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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
Require Import TestSuite.admit.
Set Universe Polymorphism.
Definition Lift
: ltac:(let U1 := constr:(Type) in
let U0 := constr:(Type : U1) in
exact (U0 -> U1))
:= fun T => T.
Fail Check nat:Prop. (* The command has indeed failed with message:
=> Error:
The term "nat" has type "Set" while it is expected to have type "Prop". *)
Set Printing All.
Set Printing Universes.
Fail Check Lift nat : Prop. (* Lift (* Top.8 Top.9 Top.10 *) nat:Prop
: Prop
(* Top.10
Top.9
Top.8 |= Top.10 < Top.9
Top.9 < Top.8
Top.9 <= Prop
*)
*)
Fail Eval compute in Lift nat : Prop.
(* = nat
: Prop *)
Monomorphic Definition Type2 := Type.
Monomorphic Definition Type1 := Type : Type2.
Section Hurkens.
(** Assumption of a retract from Type into Prop *)
Variable down : Type1 -> Prop.
Variable up : Prop -> Type1.
Hypothesis back : forall A, up (down A) -> A.
Hypothesis forth : forall A, A -> up (down A).
Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A),
P (back A (forth A a)) -> P a.
Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A),
P a -> P (back A (forth A a)).
(** Proof *)
Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop.
Definition U : Type1 := V -> Prop.
Definition sb (z:V) : V := fun A r a => r (z A r) a.
Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)).
Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x).
Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x).
Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))).
Definition I (x:U) : Prop :=
(forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False.
Lemma Omega : forall i:U -> Prop, induct i -> up (i WF).
Proof.
intros i y.
apply y.
unfold le, WF, induct.
apply forth.
intros x H0.
apply y.
unfold sb, le', le.
compute.
apply backforth_r.
exact H0.
Qed.
Lemma lemma1 : induct (fun u => down (I u)).
Proof.
unfold induct.
intros x p.
apply forth.
intro q.
generalize (q (fun u => down (I u)) p).
intro r.
apply back in r.
apply r.
intros i j.
unfold le, sb, le', le in j |-.
apply backforth in j.
specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))).
apply q.
exact j.
Qed.
Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False.
Proof.
intro x.
generalize (x (fun u => down (I u)) lemma1).
intro r; apply back in r.
apply r.
intros i H0.
apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))).
unfold le, WF in H0.
apply back in H0.
exact H0.
Qed.
Theorem paradox : False.
Proof.
exact (lemma2 Omega).
Qed.
End Hurkens.
Definition informative (x : bool) :=
match x with
| true => Type
| false => Prop
end.
Definition depsort (T : Type) (x : bool) : informative x :=
match x with
| true => T
| false => True
end.
(** This definition should fail *)
Fail Definition Box (T : Type1) : Prop := Lift T.
Fail Definition prop {T : Type1} (t : Box T) : T := t.
Fail Definition wrap {T : Type1} (t : T) : Box T := t.
Fail Definition down (x : Type1) : Prop := Box x.
Definition up (x : Prop) : Type1 := x.
Fail Definition back A : up (down A) -> A := @prop A.
Fail Definition forth (A : Type1) : A -> up (down A) := @wrap A.
Fail Definition backforth (A:Type1) (P:A->Type) (a:A) :
P (back A (forth A a)) -> P a := fun H => H.
Fail Definition backforth_r (A:Type1) (P:A->Type) (a:A) :
P a -> P (back A (forth A a)) := fun H => H.
Theorem pandora : False.
Fail apply (paradox down up back forth backforth backforth_r).
admit.
Qed.
Print Assumptions pandora.
|
