blob: 19eea94b19fb33d215db64c3f74c46cbdf9d32a5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
Inductive equivalent P Q := Equivalent (P_to_Q : P -> Q) (Q_to_P : Q -> P).
Inductive equal T (x : T) : T -> Type := Equal : equal T x x.
(* Arithmetic *)
Inductive natural := Zero | Add_1_to (n : natural).
Fixpoint add (m n : natural) : natural :=
match m with Zero => n | Add_1_to m_minus_1 => add m_minus_1 (Add_1_to n) end.
Definition double (n : natural) : natural := add n n.
Inductive odd (n : natural) :=
Odd (half : natural)
(n_odd : equal natural n (Add_1_to (double half))).
Inductive less_than (m n : natural) :=
LessThan (diff : natural)
(m_lt_n : equal natural n (Add_1_to (add m diff))).
(* Finite subsets *)
Definition injective_in T R (D : T -> Type) (f : T -> R) :=
forall x y, D x -> D y -> equal R (f x) (f y) -> equal T x y.
Inductive in_image T R (D : T -> Type) (f : T -> R) (a : R) :=
InImage (x : T) (x_in_D : D x) (a_is_fx : equal R a (f x)).
Inductive finite_of_order T (D : T -> Type) (n : natural) :=
FiniteOfOrder (rank : T -> natural)
(rank_injective : injective_in T natural D rank)
(rank_onto :
forall i, equivalent (less_than i n) (in_image T natural D rank i)).
(* Constraints *)
Universes i j.
Inductive constraint1 : (Type -> Type) -> Type := mk_constraint1 : constraint1 (fun x : Type@{i} => (x : Type@{j})).
Constraint i < j.
Inductive constraint2 : Type@{j} := mkc2 (_ : Type@{i}).
Universes i' j'.
Constraint i' = j'.
Inductive constraint3 : (Type -> Type) -> Type := mk_constraint3 : constraint3 (fun x : Type@{i'} => (x : Type@{j'})).
Inductive constraint4 : (Type -> Type) -> Type
:= mk_constraint4 : let U1 := Type in
let U2 := Type in
constraint4 (fun x : U1 => (x : U2)).
|