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
|
Section Hurkens.
Definition Type2 := Type.
Definition Type1 := Type : Type2.
(** 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.
(* The projection prop should not be definable *)
Set Primitive Projections.
Record Box (T : Type) : Prop := wrap {prop : T}.
Definition down (x : Type) : Prop := Box x.
Definition up (x : Prop) : Type := x.
Definition back A : up (down A) -> A := @prop A.
Definition forth A : A -> up (down A) := wrap A.
Definition backforth (A:Type) (P:A->Type) (a:A) :
P (back A (forth A a)) -> P a := fun H => H.
Definition backforth_r (A:Type) (P:A->Type) (a:A) :
P a -> P (back A (forth A a)) := fun H => H.
Theorem pandora : False.
apply (paradox down up back forth backforth backforth_r).
Qed.
Print Assumptions pandora.
(* Closed under the global context *)
|
