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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter" "-w" "-notation-overridden,-deprecated-option") -*- *)
(*
The Coq Proof Assistant, version 8.7.1 (January 2018)
compiled on Jan 21 2018 15:02:24 with OCaml 4.06.0
from commit 391bb5e196901a3a9426295125b8d1c700ab6992
*)
Require Export Coq.Init.Notations.
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Reserved Notation "p @ q" (at level 60, right associativity).
Reserved Notation "! p " (at level 50).
Monomorphic Universe uu.
Monomorphic Universe uu0.
Monomorphic Universe uu1.
Constraint uu0 < uu1.
Global Set Universe Polymorphism.
Global Set Polymorphic Inductive Cumulativity.
Global Unset Universe Minimization ToSet.
Notation UU := Type (only parsing).
Notation UU0 := Type@{uu0} (only parsing).
Global Set Printing Universes.
Inductive unit : UU0 := tt : unit.
Inductive paths@{i} {A:Type@{i}} (a:A) : A -> Type@{i} := idpath : paths a a.
Hint Resolve idpath : core .
Notation "a = b" := (paths a b) (at level 70, no associativity) : type_scope.
Set Primitive Projections.
Set Nonrecursive Elimination Schemes.
Record total2@{i} { T: Type@{i} } ( P: T -> Type@{i} ) : Type@{i}
:= tpair { pr1 : T; pr2 : P pr1 }.
Arguments tpair {_} _ _ _.
Arguments pr1 {_ _} _.
Arguments pr2 {_ _} _.
Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Definition foo (X:Type) (xy : @total2 X (λ _, X)) : X.
induction xy as [x y].
exact x.
Defined.
Unset Automatic Introduction.
Definition idfun (T : UU) := λ t:T, t.
Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
Proof.
intros. induction e1. exact e2.
Defined.
Hint Resolve @pathscomp0 : pathshints.
Notation "p @ q" := (pathscomp0 p q).
Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
Proof.
intros. induction e. exact (idpath _).
Defined.
Notation "! p " := (pathsinv0 p).
Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
(e: t1 = t2) : f t1 = f t2.
Proof.
intros. induction e. exact (idpath _).
Defined.
Definition map_on_two_paths {X Y Z : UU} (f : X -> Y -> Z) {x x' y y'} (ex : x = x') (ey: y = y') :
f x y = f x' y'.
Proof.
intros. induction ex. induction ey. exact (idpath _).
Defined.
Definition maponpathscomp0 {X Y : UU} {x1 x2 x3 : X}
(f : X -> Y) (e1 : x1 = x2) (e2 : x2 = x3) :
maponpaths f (e1 @ e2) = maponpaths f e1 @ maponpaths f e2.
Proof.
intros. induction e1. induction e2. exact (idpath _).
Defined.
Definition maponpathsinv0 {X Y : UU} (f : X -> Y)
{x1 x2 : X} (e : x1 = x2) : maponpaths f (! e) = ! (maponpaths f e).
Proof.
intros. induction e. exact (idpath _).
Defined.
Definition constr1 {X : UU} (P : X -> UU) {x x' : X} (e : x = x') :
∑ (f : P x -> P x'),
∑ (ee : ∏ p : P x, tpair _ x p = tpair _ x' (f p)),
∏ (pp : P x), maponpaths pr1 (ee pp) = e.
Proof.
intros. induction e.
split with (idfun (P x)).
split with (λ p, idpath _).
unfold maponpaths. simpl.
intro. exact (idpath _).
Defined.
Definition transportf@{i} {X : Type@{i}} (P : X -> Type@{i}) {x x' : X}
(e : x = x') : P x -> P x' := pr1 (constr1 P e).
Lemma two_arg_paths_f@{i} {A : Type@{i}} {B : A -> Type@{i}} {C:Type@{i}} {f : ∏ a, B a -> C} {a1 b1 a2 b2}
(p : a1 = a2) (q : transportf B p b1 = b2) : f a1 b1 = f a2 b2.
Proof.
intros. induction p. induction q. exact (idpath _).
Defined.
Definition iscontr@{i} (T:Type@{i}) : Type@{i} := ∑ cntr:T, ∏ t:T, t=cntr.
Lemma proofirrelevancecontr {X : UU} (is : iscontr X) (x x' : X) : x = x'.
Proof.
intros.
induction is as [y fe].
exact (fe x @ !(fe x')).
Defined.
Definition hfiber@{i} {X Y : Type@{i}} (f : X -> Y) (y : Y) : Type@{i} := total2 (λ x, f x = y).
Definition hfiberpair {X Y : UU} (f : X -> Y) {y : Y}
(x : X) (e : f x = y) : hfiber f y :=
tpair _ x e.
Definition coconustot (T : UU) (t : T) := ∑ t' : T, t' = t.
Definition coconustotpair (T : UU) {t t' : T} (e: t' = t) : coconustot T t
:= tpair _ t' e.
Lemma connectedcoconustot {T : UU} {t : T} (c1 c2 : coconustot T t) : c1 = c2.
Proof.
intros.
induction c1 as [x0 x].
induction x.
induction c2 as [x1 y].
induction y.
exact (idpath _).
Defined.
Definition isweq@{i} {X Y : Type@{i}} (f : X -> Y) : Type@{i} :=
∏ y : Y, iscontr (hfiber f y).
Lemma isProofIrrelevantUnit : ∏ x x' : unit, x = x'.
Proof.
intros. induction x. induction x'. exact (idpath _).
Defined.
Lemma unitl0 : tt = tt -> coconustot _ tt.
Proof.
intros e. exact (coconustotpair unit e).
Defined.
Lemma unitl1: coconustot _ tt -> tt = tt.
Proof.
intro cp. induction cp as [x t]. induction x. exact t.
Defined.
Lemma unitl2: ∏ e : tt = tt, unitl1 (unitl0 e) = e.
Proof.
intros. unfold unitl0. simpl. exact (idpath _).
Defined.
Lemma unitl3: ∏ e : tt = tt, e = idpath tt.
Proof.
intros.
assert (e0 : unitl0 (idpath tt) = unitl0 e).
{ simple refine (connectedcoconustot _ _). }
set (e1 := maponpaths unitl1 e0).
exact (! (unitl2 e) @ (! e1) @ (unitl2 (idpath _))).
Defined.
Theorem iscontrpathsinunit (x x' : unit) : iscontr (x = x').
Proof.
intros.
split with (isProofIrrelevantUnit x x').
intros e'.
induction x.
induction x'.
simpl.
apply unitl3.
Qed.
Lemma ifcontrthenunitl0 (e1 e2 : tt = tt) : e1 = e2.
Proof.
intros.
simple refine (proofirrelevancecontr _ _ _).
exact (iscontrpathsinunit tt tt).
Qed.
Section isweqcontrtounit.
Universe i.
(* To see the bug, run it both with and without this constraint: *)
(* Constraint uu0 < i. *)
(* Without this constraint, we get i = uu0 in the next definition *)
Lemma isweqcontrtounit@{} {T : Type@{i}} (is : iscontr@{i} T) : isweq@{i} (λ _:T, tt).
Proof.
intros. intro y. induction y.
induction is as [c h].
split with (hfiberpair@{i i i} _ c (idpath tt)).
intros ha.
induction ha as [x e].
simple refine (two_arg_paths_f (h x) _).
simple refine (ifcontrthenunitl0 _ _).
Defined.
(*
Explanation of the bug:
With the constraint uu0 < i above we get:
|= uu0 <= bug.3
uu0 <= i
uu1 <= i
i <= bug.3
from this print statement: *)
Print isweqcontrtounit.
(*
Without the constraint uu0 < i above we get:
|= i <= bug.3
uu0 = i
Since uu0 = i is not inferred when we impose the constraint uu0 < i,
it is invalid to infer it when we don't.
*)
Context (X : Type@{uu1}).
Check (@isweqcontrtounit X). (* detect a universe inconsistency *)
End isweqcontrtounit.
|
