-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsmash_product.v
275 lines (223 loc) · 7.14 KB
/
smash_product.v
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
Set Implicit Arguments.
Unset Strict Implicit.
Require Import HoTT.Homotopy.
Require Import pointed_spaces.
Require Import tactics.
Require Import some_lemmas.
Import pt_map_notation.
Section smash_product.
Variables A B : pt_type.
Reserved Notation "< A , B >"
(at level 40, B at next level, left associativity).
Record smash_data : Type := {
smash_carrier :> Type ;
smash_pair : forall (a : A) (b : B), smash_carrier
where "< a , b >" := (smash_pair a b)
;
base_1 : smash_carrier ;
base_2 : smash_carrier ;
contract_1 : forall (a : A), <a, point B> = base_1 ;
contract_2 : forall (b : B), <point A, b> = base_2 ;
smash_elim : forall (P : smash_carrier -> Type)
(d_pair : forall a b, P (< a , b>) )
(d_base_1 : P base_1)
(d_base_2 : P base_2)
(d_contract_1 : forall a : A,
transport (contract_1 a) (d_pair a (point B)) =
d_base_1)
(d_contract_2 : forall b : B,
transport (contract_2 b) (d_pair (point A) b) =
d_base_2)
, forall x : smash_carrier, P x
;
smash_comp_pair : forall (P : smash_carrier -> Type)
(d_pair : forall a b, P (< a , b>) )
(d_base_1 : P base_1)
(d_base_2 : P base_2)
(d_contract_1 : forall a : A,
transport (contract_1 a) (d_pair a (point B)) =
d_base_1)
(d_contract_2 : forall b : B,
transport (contract_2 b) (d_pair (point A) b) =
d_base_2),
forall a b,
smash_elim (*d_pair*) (*d_base_1*) (*d_base_2*)
d_contract_1 d_contract_2
(<a, b>) = d_pair a b
;
smash_comp_base_1 : forall (P : smash_carrier -> Type)
(d_pair : forall a b, P (< a , b>) )
(d_base_1 : P base_1)
(d_base_2 : P base_2)
(d_contract_1 : forall a : A,
transport (contract_1 a) (d_pair a (point B)) =
d_base_1)
(d_contract_2 : forall b : B,
transport (contract_2 b) (d_pair (point A) b) =
d_base_2),
smash_elim (*d_pair*) (*d_base_1*) (*d_base_2*)
d_contract_1 d_contract_2
base_1 = d_base_1
;
smash_comp_base_2 : forall (P : smash_carrier -> Type)
(d_pair : forall a b, P (< a , b>) )
(d_base_1 : P base_1)
(d_base_2 : P base_2)
(d_contract_1 : forall a : A,
transport (contract_1 a) (d_pair a (point B)) =
d_base_1)
(d_contract_2 : forall b : B,
transport (contract_2 b) (d_pair (point A) b) =
d_base_2),
smash_elim (*d_pair*) (*d_base_1*) (*d_base_2*)
d_contract_1 d_contract_2
base_2 = d_base_2
;
smash_comp_contract_1 : forall (P : smash_carrier -> Type)
(d_pair : forall a b, P (< a , b>) )
(d_base_1 : P base_1)
(d_base_2 : P base_2)
(d_contract_1 : forall a : A,
transport (contract_1 a) (d_pair a (point B)) =
d_base_1)
(d_contract_2 : forall b : B,
transport (contract_2 b) (d_pair (point A) b) =
d_base_2),
forall a : A,
map_dep (smash_elim d_contract_1 d_contract_2) (contract_1 a) =
(map (transport (contract_1 a)) ((smash_comp_pair
d_contract_1 d_contract_2) a (point B)))
@ (d_contract_1 a) @
! (smash_comp_base_1
d_contract_1 d_contract_2)
(* thanks PLL *)
}.
Definition smash_elim_simp (X : smash_data)
(Y : pt_type)
(f : forall (a : A) (b : B), Y)
(Ya Yb : Y)
(Ha : forall a : A, f a (point B) = Ya)
(Hb : forall b : B, f (point A) b = Yb) : X -> Y.
Proof.
apply
(smash_elim (P := (fun _ => Y))
(d_pair := f)
(d_base_1 := Ya)
(d_base_2 := Yb)
).
intro a.
pathvia (transport (P:=fun _ : X => Y)(contract_1 X a) Ya).
apply (map _ (Ha a)).
apply trans_trivial.
intro b.
pathvia (transport (P:=fun _ : X => Y)(contract_2 X b) Yb).
apply (map _ (Hb b)).
apply trans_trivial.
Defined.
Section smash_elim_simp_rules.
Variable X : smash_data.
Variables (Y : pt_type)
(f : forall (a : A) (b : B), Y)
(Ya Yb : Y)
(Ha : forall a : A, f a (point B) = Ya)
(Hb : forall b : B, f (point A) b = Yb).
Lemma smash_elim_simp_pair : forall a b,
@smash_elim_simp X _ f _ _ Ha Hb (smash_pair X a b) = f a b.
Proof.
intros a b.
apply (@smash_comp_pair X (fun _ => Y) f Ya Yb).
Defined.
Lemma smash_elim_simp_base_1 :
@smash_elim_simp X _ f _ _ Ha Hb (base_1 X) = Ya.
Proof.
apply (@smash_comp_base_1 X (fun _ => Y) f Ya Yb).
Defined.
Lemma smash_elim_simp_base_2 :
@smash_elim_simp X _ f _ _ Ha Hb (base_2 X) = Yb.
Proof.
apply (@smash_comp_base_2 X (fun _ => Y) f Ya Yb).
Defined.
(*
Lemma smash_elim_simp_contract_1 :
forall a : A,
map (@smash_elim_simp X _ f _ _ Ha Hb) (contract_1 a) =
*)
End smash_elim_simp_rules.
Definition smash (X : smash_data) : pt_type := {|
carrier := (* smash_carrier *) X ;
point := smash_pair X (point A) (point B)
|}.
(** a path from (a, b0) to (a0,b0) *)
Definition edge_connected_1 (X : smash_data) (a : A) :
smash_pair _ a (point B) = smash_pair X (point A)(point B).
pathvia (base_1 X).
(*apply (concat (y:=base_1 X)).*)
apply (contract_1 X a).
apply (! contract_1 X _).
Defined.
Lemma edge_connected_1_refl (X : smash_data) :
edge_connected_1 X (point A) = idpath.
Proof.
(* unfold edge_connected_1. *)
apply opposite_right_inverse.
Qed.
Definition edge_connected_2 (X : smash_data) (b : B) :
smash_pair _ (point A) b = smash_pair X (point A)(point B).
pathvia (base_2 X).
apply (contract_2 X _ ).
apply (! contract_2 _ _ ).
Defined.
Lemma edge_connected_2_refl (X : smash_data) :
edge_connected_2 X (point B) = idpath.
Proof.
(* unfold edge_connected_2. *)
apply opposite_right_inverse.
Qed.
End smash_product.
Module Import smash_notation.
Notation "< a , b >" := (smash_pair _ a b)
(at level 40, B at next level, left associativity).
End smash_notation.
Section smash_product_functorial.
Variables A B C D : pt_type.
Variable f : A .-> C.
Variable g : B .-> D.
Variable AB : smash_data A B.
Variable CD : smash_data C D.
Definition smashf_carrier : smash AB -> smash CD.
apply (@smash_elim_simp _ _ AB (smash CD)
(fun a b => smash_pair _ (pr1 f a) (pr1 g b) )
(base_1 CD)
(base_2 CD)
).
- intro a.
(* rewrite (pr2 g). *)
pathvia (smash_pair CD (pr1 f a)(point D)).
apply (map _ (pr2 g)).
apply (contract_1).
- intro b.
pathvia (smash_pair CD (point C)(pr1 g b)).
+ apply map_twovar_2eq_nondep.
apply (pr2 f).
+ apply contract_2.
Defined.
Definition smashf : smash AB .-> smash CD.
exists smashf_carrier.
unfold smashf_carrier.
change (point (smash AB)) with
(smash_pair AB (point A) (point B)).
(*rewrite smash_elim_simp_pair.*)
pathvia (smash_pair CD (pr1 f (point A))(pr1 g (point B))).
About smash_elim_simp_pair.
- simpl. apply ( smash_elim_simp_pair AB (Y:=smash CD)
(f:=fun a b => smash_pair CD (pr1 f a) (pr1 g b))).
- change (point (smash CD)) with
(smash_pair CD (point C) (point D)).
Check @map_twovar.
pathvia (smash_pair CD (pr1 f (point A)) (point D)).
+ apply (map _ (pr2 g)).
+ apply map_twovar_2eq_nondep.
apply (pr2 f).
Defined.
(* need functorial properties *)
End smash_product_functorial.