]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/hott/PathGroupoids.ma
- cprs and cnx on the way
[helm.git] / matita / matita / lib / hott / PathGroupoids.ma
1 (*
2 (** * The groupid structure of paths *)
3
4 Require Import Overture.
5
6 Local Open Scope path_scope.
7
8 (** ** Naming conventions
9
10    We need good naming conventions that allow us to name theorems without looking them up. The names should indicate the structure of the theorem, but they may sometimes be ambiguous, in which case you just have to know what is going on.    We shall adopt the following principles:
11
12    - we are not afraid of long names
13    - we are not afraid of short names when they are used frequently
14    - we use underscores
15    - name of theorems and lemmas are lower-case
16    - records and other types may be upper or lower case
17
18    Theorems about concatenation of paths are called [concat_XXX] where [XXX] tells us what is on the left-hand side of the equation. You have to guess the right-hand side. We use the following symbols in [XXX]:
19
20    - [1] means the identity path
21    - [p] means 'the path'
22    - [V] means 'the inverse path'
23    - [A] means '[ap]'
24    - [M] means the thing we are moving across equality
25    - [x] means 'the point' which is not a path, e.g. in [transport p x]
26    - [2] means relating to 2-dimensional paths
27    - [3] means relating to 3-dimensional paths, and so on
28
29    Associativity is indicated with an underscore. Here are some examples of how the name gives hints about the left-hand side of the equation.
30
31    - [concat_1p] means [1 * p]
32    - [concat_Vp] means [p^ * p]
33    - [concat_p_pp] means [p * (q * r)]
34    - [concat_pp_p] means [(p * q) * r]
35    - [concat_V_pp] means [p^ * (p * q)]
36    - [concat_pV_p] means [(q * p^) * p] or [(p * p^) * q], but probably the former because for the latter you could just use [concat_pV].
37
38    Laws about inverse of something are of the form [inv_XXX], and those about [ap] are of the form [ap_XXX], and so on. For example:
39
40    - [inv_pp] is about [(p @ q)^]
41    - [inv_V] is about [(p^)^]
42    - [inv_A] is about [(ap f p)^]
43    - [ap_V] is about [ap f (p^)]
44    - [ap_pp] is about [ap f (p @ q)]
45    - [ap_idmap] is about [ap idmap p]
46    - [ap_1] is about [ap f 1]
47    - [ap02_p2p] is about [ap02 f (p @@ q)]
48
49    Then we have laws which move things around in an equation. The naming scheme here is [moveD_XXX]. The direction [D] indicates where to move to: [L] means that we move something to the left-hand side, whereas [R] means we are moving something to the right-hand side. The part [XXX] describes the shape of the side _from_ which we are moving where the thing that is getting moves is called [M].  The presence of 1 next to an [M] generally indicates an *implied* identity path which is inserted automatically after the movement.  Examples:
50
51    - [moveL_pM] means that we transform [p = q @ r] to [p @ r^ = q]
52      because we are moving something to the left-hand side, and we are
53      moving the right argument of concat.
54
55    - [moveR_Mp] means that we transform [p @ q = r] to [q = p^ @ r]
56      because we move to the right-hand side, and we are moving the left
57      argument of concat.
58
59    - [moveR_1M] means that we transform [p = q] (rather than [p = 1 @ q]) to [p * q^ = 1].
60
61    There are also cancellation laws called [cancelR] and [cancelL], which are inverse to the 2-dimensional 'whiskering' operations [whiskerR] and [whiskerL].
62
63    We may now proceed with the groupoid structure proper.
64 *)
65
66 (** ** The 1-dimensional groupoid structure. *)
67
68 (** The identity path is a right unit. *)
69 Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
70   p @ 1 = p
71   :=
72   match p with idpath => 1 end.
73
74 (** The identity is a left unit. *)
75 Definition concat_1p {A : Type} {x y : A} (p : x = y) :
76   1 @ p = p
77   :=
78   match p with idpath => 1 end.
79
80 (** Concatenation is associative. *)
81 Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
82   p @ (q @ r) = (p @ q) @ r :=
83   match r with idpath =>
84     match q with idpath =>
85       match p with idpath => 1
86       end end end.
87
88 Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
89   (p @ q) @ r = p @ (q @ r) :=
90   match r with idpath =>
91     match q with idpath =>
92       match p with idpath => 1
93       end end end.
94
95 (** The left inverse law. *)
96 Definition concat_pV {A : Type} {x y : A} (p : x = y) :
97   p @ p^ = 1
98   :=
99   match p with idpath => 1 end.
100
101 (** The right inverse law. *)
102 Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
103   p^ @ p = 1
104   :=
105   match p with idpath => 1 end.
106
107 (** Several auxiliary theorems about canceling inverses across associativity.  These are somewhat redundant, following from earlier theorems.  *)
108
109 Definition concat_V_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
110   p^ @ (p @ q) = q
111   :=
112   match q with idpath =>
113     match p with idpath => 1 end
114   end.
115
116 Definition concat_p_Vp {A : Type} {x y z : A} (p : x = y) (q : x = z) :
117   p @ (p^ @ q) = q
118   :=
119   match q with idpath =>
120     match p with idpath => 1 end
121   end.
122
123 Definition concat_pp_V {A : Type} {x y z : A} (p : x = y) (q : y = z) :
124   (p @ q) @ q^ = p
125   :=
126   match q with idpath =>
127     match p with idpath => 1 end
128   end.
129
130 Definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) :
131   (p @ q^) @ q = p
132   :=
133   (match q as i return forall p, (p @ i^) @ i = p with
134     idpath =>
135     fun p =>
136       match p with idpath => 1 end
137   end) p.
138
139 (** Inverse distributes over concatenation *)
140 Definition inv_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
141   (p @ q)^ = q^ @ p^
142   :=
143   match q with idpath =>
144     match p with idpath => 1 end
145   end.
146
147 Definition inv_Vp {A : Type} {x y z : A} (p : y = x) (q : y = z) :
148   (p^ @ q)^ = q^ @ p
149   :=
150   match q with idpath =>
151     match p with idpath => 1 end
152   end.
153
154 Definition inv_pV {A : Type} {x y z : A} (p : x = y) (q : z = y) :
155   (p @ q^)^ = q @ p^.
156 Proof.
157   destruct p. destruct q. reflexivity.
158 Defined.
159
160 Definition inv_VV {A : Type} {x y z : A} (p : y = x) (q : z = y) :
161   (p^ @ q^)^ = q @ p.
162 Proof.
163   destruct p. destruct q. reflexivity.
164 Defined.
165
166 (** Inverse is an involution. *)
167 Definition inv_V {A : Type} {x y : A} (p : x = y) :
168   p^^ = p
169   :=
170   match p with idpath => 1 end.
171
172
173 (* *** Theorems for moving things around in equations. *)
174
175 Definition moveR_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
176   p = r^ @ q -> r @ p = q.
177 Proof.
178   destruct r.
179   intro h. exact (concat_1p _ @ h @ concat_1p _).
180 Defined.
181
182 Definition moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
183   r = q @ p^ -> r @ p = q.
184 Proof.
185   destruct p.
186   intro h. exact (concat_p1 _ @ h @ concat_p1 _).
187 Defined.
188
189 Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
190   p = r @ q -> r^ @ p = q.
191 Proof.
192   destruct r.
193   intro h. exact (concat_1p _ @ h @ concat_1p _).
194 Defined.
195
196 Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
197   r = q @ p -> r @ p^ = q.
198 Proof.
199   destruct p.
200   intro h. exact (concat_p1 _ @ h @ concat_p1 _).
201 Defined.
202
203 Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
204   r^ @ q = p -> q = r @ p.
205 Proof.
206   destruct r.
207   intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
208 Defined.
209
210 Definition moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
211   q @ p^ = r -> q = r @ p.
212 Proof.
213   destruct p.
214   intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
215 Defined.
216
217 Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
218   r @ q = p -> q = r^ @ p.
219 Proof.
220   destruct r.
221   intro h. exact ((concat_1p _)^ @ h @ (concat_1p _)^).
222 Defined.
223
224 Definition moveL_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
225   q @ p = r -> q = r @ p^.
226 Proof.
227   destruct p.
228   intro h. exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
229 Defined.
230
231 Definition moveL_1M {A : Type} {x y : A} (p q : x = y) :
232   p @ q^ = 1 -> p = q.
233 Proof.
234   destruct q.
235   intro h. exact ((concat_p1 _)^ @ h).
236 Defined.
237
238 Definition moveL_M1 {A : Type} {x y : A} (p q : x = y) :
239   q^ @ p = 1 -> p = q.
240 Proof.
241   destruct q.
242   intro h. exact ((concat_1p _)^ @ h).
243 Defined.
244
245 Definition moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
246   p @ q = 1 -> p = q^.
247 Proof.
248   destruct q.
249   intro h. exact ((concat_p1 _)^ @ h).
250 Defined.
251
252 Definition moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
253   q @ p = 1 -> p = q^.
254 Proof.
255   destruct q.
256   intro h. exact ((concat_1p _)^ @ h).
257 Defined.
258
259 Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
260   1 = p^ @ q -> p = q.
261 Proof.
262   destruct p.
263   intro h. exact (h @ (concat_1p _)).
264 Defined.
265
266 Definition moveR_1M {A : Type} {x y : A} (p q : x = y) :
267   1 = q @ p^ -> p = q.
268 Proof.
269   destruct p.
270   intro h. exact (h @ (concat_p1 _)).
271 Defined.
272
273 Definition moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
274   1 = q @ p -> p^ = q.
275 Proof.
276   destruct p.
277   intro h. exact (h @ (concat_p1 _)).
278 Defined.
279
280 Definition moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
281   1 = p @ q -> p^ = q.
282 Proof.
283   destruct p.
284   intro h. exact (h @ (concat_1p _)).
285 Defined.
286
287 Definition moveR_transport_p {A : Type} (P : A -> Type) {x y : A}
288   (p : x = y) (u : P x) (v : P y)
289   : u = p^ # v -> p # u = v.
290 Proof.
291   destruct p.
292   exact idmap.
293 Defined.
294
295 Definition moveR_transport_V {A : Type} (P : A -> Type) {x y : A}
296   (p : y = x) (u : P x) (v : P y)
297   : u = p # v -> p^ # u = v.
298 Proof.
299   destruct p.
300   exact idmap.
301 Defined.
302
303 Definition moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
304   (p : x = y) (u : P x) (v : P y)
305   : p # u = v -> u = p^ # v.
306 Proof.
307   destruct p.
308   exact idmap.
309 Defined.
310
311 Definition moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
312   (p : y = x) (u : P x) (v : P y)
313   : p^ # u = v -> u = p # v.
314 Proof.
315   destruct p.
316   exact idmap.
317 Defined.
318
319 (** *** Functoriality of functions *)
320
321 (** Here we prove that functions behave like functors between groupoids, and that [ap] itself is functorial. *)
322
323 (** Functions take identity paths to identity paths. *)
324 Definition ap_1 {A B : Type} (x : A) (f : A -> B) :
325   ap f 1 = 1 :> (f x = f x)
326   :=
327   1.
328
329 (** Functions commute with concatenation. *)
330 Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
331   ap f (p @ q) = (ap f p) @ (ap f q)
332   :=
333   match q with
334     idpath =>
335     match p with idpath => 1 end
336   end.
337
338 Definition ap_p_pp {A B : Type} (f : A -> B) {w x y z : A}
339   (r : f w = f x) (p : x = y) (q : y = z) :
340   r @ (ap f (p @ q)) = (r @ ap f p) @ (ap f q).
341 Proof.
342   destruct p, q. simpl. exact (concat_p_pp r 1 1).
343 Defined.
344
345 Definition ap_pp_p {A B : Type} (f : A -> B) {w x y z : A}
346   (p : x = y) (q : y = z) (r : f z = f w) :
347   (ap f (p @ q)) @ r = (ap f p) @ (ap f q @ r).
348 Proof.
349   destruct p, q. simpl. exact (concat_pp_p 1 1 r).
350 Defined.
351
352 (** Functions commute with path inverses. *)
353 Definition inverse_ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
354   (ap f p)^ = ap f (p^)
355   :=
356   match p with idpath => 1 end.
357
358 Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
359   ap f (p^) = (ap f p)^
360   :=
361   match p with idpath => 1 end.
362
363 (** [ap] itself is functorial in the first argument. *)
364
365 Definition ap_idmap {A : Type} {x y : A} (p : x = y) :
366   ap idmap p = p
367   :=
368   match p with idpath => 1 end.
369
370 Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
371   ap (g o f) p = ap g (ap f p)
372   :=
373   match p with idpath => 1 end.
374
375 (* Sometimes we don't have the actual function [compose]. *)
376 Definition ap_compose' {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
377   ap (fun a => g (f a)) p = ap g (ap f p)
378   :=
379   match p with idpath => 1 end.
380
381 (** The action of constant maps. *)
382 Definition ap_const {A B : Type} {x y : A} (p : x = y) (z : B) :
383   ap (fun _ => z) p = 1
384   :=
385   match p with idpath => idpath end.
386
387 (** Naturality of [ap]. *)
388 Definition concat_Ap {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y) :
389   (ap f q) @ (p y) = (p x) @ (ap g q)
390   :=
391   match q with
392     | idpath => concat_1p _ @ ((concat_p1 _) ^)
393   end.
394
395 (** Naturality of [ap] at identity. *)
396 Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
397   (ap f q) @ (p y) = (p x) @ q
398   :=
399   match q with
400     | idpath => concat_1p _ @ ((concat_p1 _) ^)
401   end.
402
403 Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) :
404   (p x) @ (ap f q) =  q @ (p y)
405   :=
406   match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
407     | idpath => concat_p1 _ @ (concat_1p _)^
408   end.
409
410 (** Naturality with other paths hanging around. *)
411 Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
412   {x y : A} (q : x = y)
413   {w z : B} (r : w = f x) (s : g y = z)
414   :
415   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s).
416 Proof.
417   destruct q, s; simpl.
418   repeat rewrite concat_p1.
419   reflexivity.
420 Defined.
421
422 Definition concat_pA_p {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
423   {x y : A} (q : x = y)
424   {w : B} (r : w = f x)
425   :
426   (r @ ap f q) @ p y = (r @ p x) @ ap g q.
427 Proof.
428   destruct q; simpl.
429   repeat rewrite concat_p1.
430   reflexivity.
431 Defined.
432
433 Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
434   {x y : A} (q : x = y)
435   {z : B} (s : g y = z)
436   :
437   (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
438 Proof.
439   destruct q, s; simpl.
440   repeat rewrite concat_p1, concat_1p.
441   reflexivity.
442 Defined.
443
444 Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
445   {x y : A} (q : x = y)
446   {w z : A} (r : w = f x) (s : y = z)
447   :
448   (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).
449 Proof.
450   destruct q, s; simpl.
451   repeat rewrite concat_p1.
452   reflexivity.
453 Defined.
454
455 Definition concat_pp_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
456   {x y : A} (q : x = y)
457   {w z : A} (r : w = x) (s : g y = z)
458   :
459   (r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s).
460 Proof.
461   destruct q, s; simpl.
462   repeat rewrite concat_p1.
463   reflexivity.
464 Defined.
465
466 Definition concat_pA1_p {A : Type} {f : A -> A} (p : forall x, f x = x)
467   {x y : A} (q : x = y)
468   {w : A} (r : w = f x)
469   :
470   (r @ ap f q) @ p y = (r @ p x) @ q.
471 Proof.
472   destruct q; simpl.
473   repeat rewrite concat_p1.
474   reflexivity.
475 Defined.
476
477 Definition concat_A1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
478   {x y : A} (q : x = y)
479   {z : A} (s : y = z)
480   :
481   (ap f q) @ (p y @ s) = (p x) @ (q @ s).
482 Proof.
483   destruct q, s; simpl.
484   repeat rewrite concat_p1, concat_1p.
485   reflexivity.
486 Defined.
487
488 Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
489   {x y : A} (q : x = y)
490   {w : A} (r : w = x)
491   :
492   (r @ p x) @ ap g q = (r @ q) @ p y.
493 Proof.
494   destruct q; simpl.
495   repeat rewrite concat_p1.
496   reflexivity.
497 Defined.
498
499 Definition concat_p_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
500   {x y : A} (q : x = y)
501   {z : A} (s : g y = z)
502   :
503   p x @ (ap g q @ s) = q @ (p y @ s).
504 Proof.
505   destruct q, s; simpl.
506   repeat rewrite concat_p1, concat_1p.
507   reflexivity.
508 Defined.
509
510 (** *** Action of [apD10] and [ap10] on paths. *)
511
512 (** Application of paths between functions preserves the groupoid structure *)
513
514 Definition apD10_1 {A} {B:A->Type} (f : forall x, B x) (x:A)
515   : apD10 (idpath f) x = 1
516 := 1.
517
518 Definition apD10_pp {A} {B:A->Type} {f f' f'' : forall x, B x}
519   (h:f=f') (h':f'=f'') (x:A)
520 : apD10 (h @ h') x = apD10 h x @ apD10 h' x.
521 Proof.
522   case h, h'; reflexivity.
523 Defined.
524
525 Definition apD10_V {A} {B:A->Type} {f g : forall x, B x} (h:f=g) (x:A)
526   : apD10 (h^) x = (apD10 h x)^
527 := match h with idpath => 1 end.
528
529 Definition ap10_1 {A B} {f:A->B} (x:A) : ap10 (idpath f) x = 1
530   := 1.
531
532 Definition ap10_pp {A B} {f f' f'':A->B} (h:f=f') (h':f'=f'') (x:A)
533   : ap10 (h @ h') x = ap10 h x @ ap10 h' x
534 := apD10_pp h h' x.
535
536 Definition ap10_V {A B} {f g : A->B} (h : f = g) (x:A)
537   : ap10 (h^) x = (ap10 h x)^
538 := apD10_V h x.
539
540 (** [ap10] also behaves nicely on paths produced by [ap] *)
541 Lemma ap_ap10 {A B C} (f g : A -> B) (h : B -> C)
542   (p : f = g) (a : A) :
543   ap h (ap10 p a) = ap10 (ap (fun f' => h o f') p) a.
544 Proof.
545   destruct p. exact 1.
546 Defined.
547
548 (** *** Transport and the groupoid structure of paths *)
549
550 Definition transport_1 {A : Type} (P : A -> Type) {x : A} (u : P x)
551   : 1 # u = u
552 := 1.
553
554 Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
555   p @ q # u = q # p # u :=
556   match q with idpath =>
557     match p with idpath => 1 end
558   end.
559
560 Definition transport_pV {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P y)
561   : p # p^ # z = z
562   := (transport_pp P p^ p z)^
563   @ ap (fun r => transport P r z) (concat_Vp p).
564
565 Definition transport_Vp {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P x)
566   : p^ # p # z = z
567   := (transport_pp P p p^ z)^
568   @ ap (fun r => transport P r z) (concat_pV p).
569
570 (** In the future, we may expect to need some higher coherence for transport:
571   for instance, that transport acting on the associator is trivial. *)
572 Definition transport_p_pp {A : Type} (P : A -> Type)
573   {x y z w : A} (p : x = y) (q : y = z) (r : z = w)
574   (u : P x)
575   : ap (fun e => e # u) (concat_p_pp p q r)
576     @ (transport_pp P (p@q) r u) @ ap (transport P r) (transport_pp P p q u)
577   = (transport_pp P p (q@r) u) @ (transport_pp P q r (p#u))
578   :> ((p @ (q @ r)) # u = r # q # p # u) .
579 Proof.
580   destruct p, q, r.  simpl.  exact 1.
581 Defined.
582
583 (* Here is another coherence lemma for transport. *)
584 Definition transport_pVp {A} (P : A -> Type) {x y:A} (p:x=y) (z:P x)
585   : transport_pV P p (transport P p z)
586   = ap (transport P p) (transport_Vp P p z).
587 Proof.
588   destruct p; reflexivity.
589 Defined.
590
591 (** Dependent transport in a doubly dependent type. *)
592
593 Definition transportD {A : Type} (B : A -> Type) (C : forall a:A, B a -> Type)
594   {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1 y)
595   : C x2 (p # y)
596   :=
597   match p with idpath => z end.
598
599 (** Transporting along higher-dimensional paths *)
600
601 Definition transport2 {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
602   (r : p = q) (z : P x)
603   : p # z = q # z
604   := ap (fun p' => p' # z) r.
605
606 (** An alternative definition. *)
607 Definition transport2_is_ap10 {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
608   (r : p = q) (z : Q x)
609   : transport2 Q r z = ap10 (ap (transport Q) r) z
610   := match r with idpath => 1 end.
611
612 Definition transport2_p2p {A : Type} (P : A -> Type) {x y : A} {p1 p2 p3 : x = y}
613   (r1 : p1 = p2) (r2 : p2 = p3) (z : P x)
614   : transport2 P (r1 @ r2) z = transport2 P r1 z @ transport2 P r2 z.
615 Proof.
616   destruct r1, r2; reflexivity.
617 Defined.
618
619 Definition transport2_V {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
620   (r : p = q) (z : Q x)
621   : transport2 Q (r^) z = (transport2 Q r z)^
622   := match r with idpath => 1 end.
623
624 Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
625   {z w : P x} (r : p = q) (s : z = w)
626   : ap (transport P p) s  @  transport2 P r w
627     = transport2 P r z  @  ap (transport P q) s
628   := match r with idpath => (concat_p1 _ @ (concat_1p _)^) end.
629
630 (* TODO: What should this be called? *)
631 Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
632   f y (p # z) = (p # (f x z)).
633 Proof.
634   by induction p.
635 Defined.
636
637
638 (** *** Transporting in particular fibrations. *)
639
640 (** One frequently needs lemmas showing that transport in a certain dependent type is equal to some more explicitly defined operation, defined according to the structure of that dependent type.  For most dependent types, we prove these lemmas in the appropriate file in the types/ subdirectory.  Here we consider only the most basic cases. *)
641
642 (** Transporting in a constant fibration. *)
643 Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
644   : transport (fun x => B) p y = y.
645 Proof.
646   destruct p.  exact 1.
647 Defined.
648
649 Definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 = x2}
650   (r : p = q) (y : B)
651   : transport_const p y = transport2 (fun _ => B) r y @ transport_const q y
652   := match r with idpath => (concat_1p _)^ end.
653
654 (** Transporting in a pulled back fibration. *)
655 Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
656   (p : x = y) (z : P (f x))
657   : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.
658 Proof.
659   destruct p; reflexivity.
660 Defined.
661
662 (** A special case of [transport_compose] which seems to come up a lot. *)
663 Definition transport_idmap_ap A (P : A -> Type) x y (p : x = y) (u : P x)
664 : transport P p u = transport idmap (ap P p) u
665   := match p with idpath => idpath end.
666
667 (** *** The behavior of [ap] and [apD]. *)
668
669 (** In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. *)
670 Lemma apD_const {A B} {x y : A} (f : A -> B) (p: x = y) :
671   apD f p = transport_const p (f x) @ ap f p.
672 Proof.
673   destruct p; reflexivity.
674 Defined.
675
676 (** ** The 2-dimensional groupoid structure *)
677
678 (** Horizontal composition of 2-dimensional paths. *)
679 Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
680   : p @ q = p' @ q'
681 := match h, h' with idpath, idpath => 1 end.
682
683 Notation "p @@ q" := (concat2 p q)%path (at level 20) : path_scope.
684
685 (** 2-dimensional path inversion *)
686 Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
687   : p^ = q^
688 := match h with idpath => 1 end.
689
690 (** *** Whiskering *)
691
692 Definition whiskerL {A : Type} {x y z : A} (p : x = y)
693   {q r : y = z} (h : q = r) : p @ q = p @ r
694 := 1 @@ h.
695
696 Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
697   (h : p = q) (r : y = z) : p @ r = q @ r
698 := h @@ 1.
699
700 (** *** Unwhiskering, a.k.a. cancelling. *)
701
702 Lemma cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
703   : (p @ q = p @ r) -> (q = r).
704 Proof.
705   destruct p, r.
706   intro a.
707   exact ((concat_1p q)^ @ a).
708 Defined.
709
710 Lemma cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
711   : (p @ r = q @ r) -> (p = q).
712 Proof.
713   destruct r, p.
714   intro a.
715   exact (a @ concat_p1 q).
716 Defined.
717
718 (** Whiskering and identity paths. *)
719
720 Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
721   (concat_p1 p) ^ @ whiskerR h 1 @ concat_p1 q = h
722   :=
723   match h with idpath =>
724     match p with idpath =>
725       1
726     end end.
727
728 Definition whiskerR_1p {A : Type} {x y z : A} (p : x = y) (q : y = z) :
729   whiskerR 1 q = 1 :> (p @ q = p @ q)
730   :=
731   match q with idpath => 1 end.
732
733 Definition whiskerL_p1 {A : Type} {x y z : A} (p : x = y) (q : y = z) :
734   whiskerL p 1 = 1 :> (p @ q = p @ q)
735   :=
736   match q with idpath => 1 end.
737
738 Definition whiskerL_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
739   (concat_1p p) ^ @ whiskerL 1 h @ concat_1p q = h
740   :=
741   match h with idpath =>
742     match p with idpath =>
743       1
744     end end.
745
746 Definition concat2_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
747   h @@ 1 = whiskerR h 1 :> (p @ 1 = q @ 1)
748   :=
749   match h with idpath => 1 end.
750
751 Definition concat2_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
752   1 @@ h = whiskerL 1 h :> (1 @ p = 1 @ q)
753   :=
754   match h with idpath => 1 end.
755
756
757 (** The interchange law for concatenation. *)
758 Definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x = y} {q q' q'' : y = z}
759   (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') :
760   (a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d).
761 Proof.
762   case d.
763   case c.
764   case b.
765   case a.
766   reflexivity.
767 Defined.
768
769 (** The interchange law for whiskering.  Special case of [concat_concat2]. *)
770 Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
771   (whiskerR a q) @ (whiskerL p' b) = (whiskerL p b) @ (whiskerR a q')
772   :=
773   match b with
774     idpath =>
775     match a with idpath =>
776       (concat_1p _)^
777     end
778   end.
779
780 (** Structure corresponding to the coherence equations of a bicategory. *)
781
782 (** The "pentagonator": the 3-cell witnessing the associativity pentagon. *)
783 Definition pentagon {A : Type} {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z)
784   : whiskerL p (concat_p_pp q r s)
785       @ concat_p_pp p (q@r) s
786       @ whiskerR (concat_p_pp p q r) s
787   = concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s.
788 Proof.
789   case p, q, r, s.  reflexivity.
790 Defined.
791
792 (** The 3-cell witnessing the left unit triangle. *)
793 Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
794   : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q
795   = whiskerL p (concat_1p q).
796 Proof.
797   case p, q.  reflexivity.
798 Defined.
799
800 (** The Eckmann-Hilton argument *)
801 Definition eckmann_hilton {A : Type} {x:A} (p q : 1 = 1 :> (x = x)) : p @ q = q @ p :=
802   (whiskerR_p1 p @@ whiskerL_1p q)^
803   @ (concat_p1 _ @@ concat_p1 _)
804   @ (concat_1p _ @@ concat_1p _)
805   @ (concat_whisker _ _ _ _ p q)
806   @ (concat_1p _ @@ concat_1p _)^
807   @ (concat_p1 _ @@ concat_p1 _)^
808   @ (whiskerL_1p q @@ whiskerR_p1 p).
809
810 (** The action of functions on 2-dimensional paths *)
811
812 Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
813   := match r with idpath => 1 end.
814
815 Definition ap02_pp {A B} (f:A->B) {x y:A} {p p' p'':x=y} (r:p=p') (r':p'=p'')
816   : ap02 f (r @ r') = ap02 f r @ ap02 f r'.
817 Proof.
818   case r, r'; reflexivity.
819 Defined.
820
821 Definition ap02_p2p {A B} (f:A->B) {x y z:A} {p p':x=y} {q q':y=z} (r:p=p') (s:q=q')
822   : ap02 f (r @@ s) =   ap_pp f p q
823                       @ (ap02 f r  @@  ap02 f s)
824                       @ (ap_pp f p' q')^.
825 Proof.
826   case r, s, p, q. reflexivity.
827 Defined.
828
829 Definition apD02 {A : Type} {B : A -> Type} {x y : A} {p q : x = y}
830   (f : forall x, B x) (r : p = q)
831   : apD f p = transport2 B r (f x) @ apD f q
832   := match r with idpath => (concat_1p _)^ end.
833
834 (* And now for a lemma whose statement is much longer than its proof. *)
835 Definition apD02_pp {A} (B : A -> Type) (f : forall x:A, B x) {x y : A}
836   {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3)
837   : apD02 f (r1 @ r2)
838   = apD02 f r1
839   @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
840   @ concat_p_pp _ _ _
841   @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)).
842 Proof.
843   destruct r1, r2. destruct p1. reflexivity.
844 Defined.
845
846 (** ** Tactics, hints, and aliases *)
847
848 (** [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required. *)
849 Notation concatR := (fun p q => concat q p).
850
851 Hint Resolve
852   concat_1p concat_p1 concat_p_pp
853   inv_pp inv_V
854  : path_hints.
855
856 (* First try at a paths db
857 We want the RHS of the equation to become strictly simpler *)
858 Hint Rewrite
859 @concat_p1
860 @concat_1p
861 @concat_p_pp (* there is a choice here !*)
862 @concat_pV
863 @concat_Vp
864 @concat_V_pp
865 @concat_p_Vp
866 @concat_pp_V
867 @concat_pV_p
868 (*@inv_pp*) (* I am not sure about this one *)
869 @inv_V
870 @moveR_Mp
871 @moveR_pM
872 @moveL_Mp
873 @moveL_pM
874 @moveL_1M
875 @moveL_M1
876 @moveR_M1
877 @moveR_1M
878 @ap_1
879 (* @ap_pp
880 @ap_p_pp ?*)
881 @inverse_ap
882 @ap_idmap
883 (* @ap_compose
884 @ap_compose'*)
885 @ap_const
886 (* Unsure about naturality of [ap], was absent in the old implementation*)
887 @apD10_1
888 :paths.
889
890 Ltac hott_simpl :=
891   autorewrite with paths in * |- * ; auto with path_hints.
892 *)