blob: 059462fac3bf6483da9283657d8b5eedf3aef707 (
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
(* Inductive paths {A} (x : A) : A -> Type := idpath : paths x x where "x = y" := (@paths _ x y) : type_scope. *)
(* Goal forall A B : Set, @paths Type A B -> @paths Set A B. *)
(* intros A B H. *)
(* Fail exact H. *)
(* Section . *)
Section lift_strict.
Polymorphic Definition liftlt :=
let t := Type@{i} : Type@{k} in
fun A : Type@{i} => A : Type@{k}.
Polymorphic Definition liftle :=
fun A : Type@{i} => A : Type@{k}.
End lift_strict.
Set Universe Polymorphism.
(* Inductive option (A : Type) : Type := *)
(* | None : option A *)
(* | Some : A -> option A. *)
Inductive option (A : Type@{i}) : Type@{i} :=
| None : option A
| Some : A -> option A.
Definition foo' {A : Type@{i}} (o : option@{i} A) : option@{i} A :=
o.
Definition foo'' {A : Type@{i}} (o : option@{j} A) : option@{k} A :=
o.
Definition testm (A : Type@{i}) : Type@{max(i,j)} := A.
(* Inductive prod (A : Type@{i}) (B : Type@{j}) := *)
(* | pair : A -> B -> prod A B. *)
(* Definition snd {A : Type@{i}} (B : Type@{j}) (p : prod A B) : B := *)
(* match p with *)
(* | pair _ _ a b => b *)
(* end. *)
(* Definition snd' {A : Type@{i}} (B : Type@{i}) (p : prod A B) : B := *)
(* match p with *)
(* | pair _ _ a b => b *)
(* end. *)
(* Inductive paths {A : Type} : A -> A -> Type := *)
(* | idpath (a : A) : paths a a. *)
Inductive paths {A : Type@{i}} : A -> A -> Type@{i} :=
| idpath (a : A) : paths a a.
Definition Funext :=
forall (A : Type) (B : A -> Type),
forall f g : (forall a, B a), (forall x : A, paths (f x) (g x)) -> paths f g.
Definition paths_lift_closed (A : Type@{i}) (x y : A) :
paths x y -> @paths (liftle@{j Type} A) x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition paths_lift (A : Type@{i}) (x y : A) :
paths x y -> paths@{j} x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition paths_lift_closed_strict (A : Type@{i}) (x y : A) :
paths x y -> @paths (liftlt@{j Type} A) x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition paths_downward_closed_le (A : Type@{i}) (x y : A) :
paths@{j} (A:=liftle@{i j} A) x y -> paths@{i} x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition paths_downward_closed_lt (A : Type@{i}) (x y : A) :
@paths (liftlt@{j i} A) x y -> paths x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition paths_downward_closed_lt_nolift (A : Type@{i}) (x y : A) :
paths@{j} x y -> paths x y.
Proof.
intros. destruct X. exact (idpath _).
Defined.
Definition funext_downward_closed (F : Funext@{i' j' k'}) :
Funext@{i j k}.
Proof.
intros A B f g H. red in F.
pose (F A B f g (fun x => paths_lift _ _ _ (H x))).
apply paths_downward_closed_lt_nolift. apply p.
Defined.
|
