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 *)