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
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
|
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
(* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
coqtop version trunk (October 2014) *)
Notation Type0 := Set.
Notation idmap := (fun x => x).
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Open Scope fibration_scope.
Notation pr1 := projT1.
Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
Definition compose {A B C : Type} (g : B -> C) (f : A -> B) :=
fun x => g (f x).
Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
Open Scope function_scope.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Arguments idpath {A a} , [A] a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x.
admit.
Defined.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
Notation "1" := idpath : path_scope.
Notation "p @ q" := (concat p q) (at level 20) : path_scope.
Notation "p ^" := (inverse p) (at level 3, format "p '^'") : path_scope.
Notation "p @' q" := (concat p q) (at level 21, left associativity,
format "'[v' p '/' '@'' q ']'") : long_path_scope.
Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y.
exact (match p with idpath => u end).
Defined.
Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y.
exact (match p with idpath => idpath end).
Defined.
Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
:= forall x:A, f x = g x.
Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
forall x : A, r (s x) = x.
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : Sect equiv_inv f;
eissect : Sect f equiv_inv;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
Arguments eisretr {A B} f {_} _.
Record Equiv A B := BuildEquiv {
equiv_fun : A -> B ;
equiv_isequiv : IsEquiv equiv_fun
}.
Coercion equiv_fun : Equiv >-> Funclass.
Global Existing Instance equiv_isequiv.
Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
Class Contr_internal (A : Type) := BuildContr {
center : A ;
contr : (forall y : A, center = y)
}.
Inductive trunc_index : Type :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.
Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
Local Open Scope trunc_scope.
Notation "-2" := minus_two (at level 0) : trunc_scope.
Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
match n with
| -2 => Contr_internal A
| n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
end.
Class IsTrunc (n : trunc_index) (A : Type) : Type :=
Trunc_is_trunc : IsTrunc_internal n A.
Notation IsHProp := (IsTrunc -1).
Monomorphic Axiom dummy_funext_type : Type0.
Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
Local Open Scope path_scope.
Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
p @ 1 = p
:=
match p with idpath => 1 end.
Definition concat_1p {A : Type} {x y : A} (p : x = y) :
1 @ p = p
:=
match p with idpath => 1 end.
Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
p @ (q @ r) = (p @ q) @ r :=
match r with idpath =>
match q with idpath =>
match p with idpath => 1
end end end.
Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
(p @ q) @ r = p @ (q @ r) :=
match r with idpath =>
match q with idpath =>
match p with idpath => 1
end end end.
Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
r^ @ q = p -> q = r @ p.
admit.
Defined.
Ltac with_rassoc tac :=
repeat rewrite concat_pp_p;
tac;
repeat rewrite concat_p_pp.
Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp).
Definition ap_p_pp {A B : Type} (f : A -> B) {w : B} {x y z : A}
(r : w = f x) (p : x = y) (q : y = z) :
r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q).
admit.
Defined.
Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
ap (g o f) p = ap g (ap f p)
:=
match p with idpath => 1 end.
Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
(ap f q) @ (p y) = (p x) @ (ap g q)
:=
match q with
| idpath => concat_1p _ @ ((concat_p1 _) ^)
end.
Definition transportD2 {A : Type} (B C : A -> Type) (D : forall a:A, B a -> C a -> Type)
{x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D x1 y z)
: D x2 (p # y) (p # z)
:=
match p with idpath => w end.
Local Open Scope equiv_scope.
Definition transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
{x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) (y : B x2)
: (transport (fun x => B x -> C) p f) y = f (p^ # y).
admit.
Defined.
Definition transport_arrow_fromconst {A B : Type} {C : A -> Type}
{x1 x2 : A} (p : x1 = x2) (f : B -> C x1) (y : B)
: (transport (fun x => B -> C x) p f) y = p # (f y).
admit.
Defined.
Definition ap_transport_arrow_toconst {A : Type} {B : A -> Type} {C : Type}
{x1 x2 : A} (p : x1 = x2) (f : B x1 -> C) {y1 y2 : B x2} (q : y1 = y2)
: ap (transport (fun x => B x -> C) p f) q
@ transport_arrow_toconst p f y2
= transport_arrow_toconst p f y1
@ ap (fun y => f (p^ # y)) q.
admit.
Defined.
Class Univalence.
Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B).
admit.
Defined.
Definition transport_path_universe
{A B : Type} (f : A -> B) {feq : IsEquiv f} (z : A)
: transport (fun X:Type => X) (path_universe f) z = f z.
admit.
Defined.
Definition transport_path_universe_V `{Funext}
{A B : Type} (f : A -> B) {feq : IsEquiv f} (z : B)
: transport (fun X:Type => X) (path_universe f)^ z = f^-1 z.
admit.
Defined.
Ltac simpl_do_clear tac term :=
let H := fresh in
assert (H := term);
simpl in H |- *;
tac H;
clear H.
Tactic Notation "simpl" "rewrite" constr(term) := simpl_do_clear ltac:(fun H => rewrite H) term.
Global Instance Univalence_implies_Funext `{Univalence} : Funext.
Admitted.
Section Factorization.
Context {class1 class2 : forall (X Y : Type@{i}), (X -> Y) -> Type@{i}}
`{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class1 _ _ g)}
`{forall (X Y : Type@{i}) (g:X->Y), IsHProp (class2 _ _ g)}
{A B : Type@{i}} {f : A -> B}.
Record Factorization :=
{ intermediate : Type ;
factor1 : A -> intermediate ;
factor2 : intermediate -> B ;
fact_factors : factor2 o factor1 == f ;
inclass1 : class1 _ _ factor1 ;
inclass2 : class2 _ _ factor2
}.
Record PathFactorization {fact fact' : Factorization} :=
{ path_intermediate : intermediate fact <~> intermediate fact' ;
path_factor1 : path_intermediate o factor1 fact == factor1 fact' ;
path_factor2 : factor2 fact == factor2 fact' o path_intermediate ;
path_fact_factors : forall a, path_factor2 (factor1 fact a)
@ ap (factor2 fact') (path_factor1 a)
@ fact_factors fact' a
= fact_factors fact a
}.
Context `{Univalence} {fact fact' : Factorization}
(pf : @PathFactorization fact fact').
Let II := path_intermediate pf.
Let ff1 := path_factor1 pf.
Let ff2 := path_factor2 pf.
Local Definition II' : intermediate fact = intermediate fact'.
admit.
Defined.
Local Definition fff' (a : A)
: (transportD2 (fun X => A -> X) (fun X => X -> B)
(fun X g h => {_ : forall a : A, h (g a) = f a &
{_ : class1 A X g & class2 X B h}})
II' (factor1 fact) (factor2 fact)
(fact_factors fact; (inclass1 fact; inclass2 fact))).1 a =
ap (transport (fun X => X -> B) II' (factor2 fact))
(transport_arrow_fromconst II' (factor1 fact) a
@ transport_path_universe II (factor1 fact a)
@ ff1 a)
@ transport_arrow_toconst II' (factor2 fact) (factor1 fact' a)
@ ap (factor2 fact) (transport_path_universe_V II (factor1 fact' a))
@ ff2 (II^-1 (factor1 fact' a))
@ ap (factor2 fact') (eisretr II (factor1 fact' a))
@ fact_factors fact' a.
Proof.
Open Scope long_path_scope.
rewrite (ap_transport_arrow_toconst (B := idmap) (C := B)).
simpl rewrite (@ap_compose _ _ _ (transport idmap (path_universe II)^)
(factor2 fact)).
rewrite <- ap_p_pp; rewrite_moveL_Mp_p.
Set Debug Tactic Unification.
Fail rewrite (concat_Ap ff2).
|
