PathGroupoids.v

(* -*- mode: coq; mode: visual-line -*-  *)

(** * The groupid structure of paths *)

Require Import Basics.Overture Basics.Tactics.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Open Scope path_scope.

(** ** Naming conventions

   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:

   - we are not afraid of long names
   - we are not afraid of short names when they are used frequently
   - we use underscores
   - name of theorems and lemmas are lower-case
   - records and other types may be upper or lower case

   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]:

   - [1] means the identity path
   - [p] means 'the path'
   - [V] means 'the inverse path'
   - [A] means '[ap]'
   - [M] means the thing we are moving across equality
   - [x] means 'the point' which is not a path, e.g. in [transport p x]
   - [2] means relating to 2-dimensional paths
   - [3] means relating to 3-dimensional paths, and so on

   Associativity is indicated with an underscore. Here are some examples of how the name gives hints about the left-hand side of the equation.

   - [concat_1p] means [1 * p]
   - [concat_Vp] means [p^ * p]
   - [concat_p_pp] means [p * (q * r)]
   - [concat_pp_p] means [(p * q) * r]
   - [concat_V_pp] means [p^ * (p * q)]
   - [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].

   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:

   - [inv_pp] is about [(p @ q)^]
   - [inv_V] is about [(p^)^]
   - [inv_A] is about [(ap f p)^]
   - [ap_V] is about [ap f (p^)]
   - [ap_pp] is about [ap f (p @ q)]
   - [ap_idmap] is about [ap idmap p]
   - [ap_1] is about [ap f 1]
   - [ap02_p2p] is about [ap02 f (p @@ q)]

   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:

   - [moveL_pM] means that we transform [p = q @ r] to [p @ r^ = q]
     because we are moving something to the left-hand side, and we are
     moving the right argument of concat.

   - [moveR_Mp] means that we transform [p @ q = r] to [q = p^ @ r]
     because we move to the right-hand side, and we are moving the left
     argument of concat.

   - [moveR_1M] means that we transform [p = q] (rather than [p = 1 @ q]) to [p * q^ = 1].

   There are also cancellation laws called [cancelR] and [cancelL], which are inverse to the 2-dimensional 'whiskering' operations [whiskerR] and [whiskerL].

   We may now proceed with the groupoid structure proper.
*)

(** ** The 1-dimensional groupoid structure. *)

(** The identity path is a right unit. *)
Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
  p @ 1 = p
  :=
  match p with idpath => 1 end.

(** The identity is a left unit. *)
Definition concat_1p {A : Type} {x y : A} (p : x = y) :
  1 @ p = p
  :=
  match p with idpath => 1 end.

(** It's common to need to use both. *)
Definition concat_p1_1p {A : Type} {x y : A} (p : x = y)
  : p @ 1 = 1 @ p
  := concat_p1 p @ (concat_1p p)^.

Definition concat_1p_p1 {A : Type} {x y : A} (p : x = y)
  : 1 @ p = p @ 1
  := concat_1p p @ (concat_p1 p)^.

(** Concatenation is associative. *)
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.

(** The left inverse law. *)
Definition concat_pV {A : Type} {x y : A} (p : x = y) :
  p @ p^ = 1
  :=
  match p with idpath => 1 end.

(** The right inverse law. *)
Definition concat_Vp {A : Type} {x y : A} (p : x = y) :
  p^ @ p = 1
  :=
  match p with idpath => 1 end.

(** Several auxiliary theorems about canceling inverses across associativity.  These are somewhat redundant, following from earlier theorems.  *)

Definition concat_V_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  p^ @ (p @ q) = q
  :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition concat_p_Vp {A : Type} {x y z : A} (p : x = y) (q : x = z) :
  p @ (p^ @ q) = q
  :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition concat_pp_V {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  (p @ q) @ q^ = p
  :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) :
  (p @ q^) @ q = p
  :=
  (match q as i return forall p, (p @ i^) @ i = p with
    idpath =>
    fun p =>
      match p with idpath => 1 end
  end) p.

(** Inverse distributes over concatenation *)
Definition inv_pp {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  (p @ q)^ = q^ @ p^
  :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition inv_Vp {A : Type} {x y z : A} (p : y = x) (q : y = z) :
  (p^ @ q)^ = q^ @ p
  :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition inv_pV {A : Type} {x y z : A} (p : x = y) (q : z = y) :
  (p @ q^)^ = q @ p^.A: Type
x, y, z: A
p: x = y
q: z = y
(p @ q^)^ = q @ p^
Proof.A: Type
x, y, z: A
p: x = y
q: z = y
(p @ q^)^ = q @ p^
  destruct p.A: Type
x, z: A
q: z = x
(1 @ q^)^ = q @ 1^ destruct q.A: Type
z: A
(1 @ 1^)^ = 1 @ 1^ reflexivity.
Defined.

Definition inv_VV {A : Type} {x y z : A} (p : y = x) (q : z = y) :
  (p^ @ q^)^ = q @ p.A: Type
x, y, z: A
p: y = x
q: z = y
(p^ @ q^)^ = q @ p
Proof.A: Type
x, y, z: A
p: y = x
q: z = y
(p^ @ q^)^ = q @ p
  destruct p.A: Type
y, z: A
q: z = y
(1^ @ q^)^ = q @ 1 destruct q.A: Type
z: A
(1^ @ 1^)^ = 1 @ 1 reflexivity.
Defined.

(** Inverse is an involution. *)
Definition inv_V {A : Type} {x y : A} (p : x = y) :
  p^^ = p
  :=
  match p with idpath => 1 end.


(** *** Theorems for moving things around in equations. *)

Definition moveR_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  p = r^ @ q -> r @ p = q.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
p = r^ @ q -> r @ p = q
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
p = r^ @ q -> r @ p = q
  destruct r.A: Type
y, z: A
p, q: y = z
p = 1^ @ q -> 1 @ p = q
  intro h.A: Type
y, z: A
p, q: y = z
h: p = 1^ @ q
1 @ p = q exact (concat_1p _ @ h @ concat_1p _).
Defined.

Definition moveR_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r = q @ p^ -> r @ p = q.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
r = q @ p^ -> r @ p = q
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
r = q @ p^ -> r @ p = q
  destruct p.A: Type
x, y: A
q, r: y = x
r = q @ 1^ -> r @ 1 = q
  intro h.A: Type
x, y: A
q, r: y = x
h: r = q @ 1^
r @ 1 = q exact (concat_p1 _ @ h @ concat_p1 _).
Defined.

Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  p = r @ q -> r^ @ p = q.A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
p = r @ q -> r^ @ p = q
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
p = r @ q -> r^ @ p = q
  destruct r.A: Type
x, z: A
p, q: x = z
p = 1 @ q -> 1^ @ p = q
  intro h.A: Type
x, z: A
p, q: x = z
h: p = 1 @ q
1^ @ p = q exact (concat_1p _ @ h @ concat_1p _).
Defined.

Definition moveR_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  r = q @ p -> r @ p^ = q.A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
r = q @ p -> r @ p^ = q
Proof.A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
r = q @ p -> r @ p^ = q
  destruct p.A: Type
y, z: A
q, r: y = z
r = q @ 1 -> r @ 1^ = q
  intro h.A: Type
y, z: A
q, r: y = z
h: r = q @ 1
r @ 1^ = q exact (concat_p1 _ @ h @ concat_p1 _).
Defined.

Definition moveL_Mp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  r^ @ q = p -> q = r @ p.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
r^ @ q = p -> q = r @ p
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
r^ @ q = p -> q = r @ p
  destruct r.A: Type
y, z: A
p, q: y = z
1^ @ q = p -> q = 1 @ p
  intro h.A: Type
y, z: A
p, q: y = z
h: 1^ @ q = p
q = 1 @ p exact ((concat_1p _)^ @ h @ (concat_1p _)^).
Defined.

Definition moveL_pM {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  q @ p^ = r -> q = r @ p.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
q @ p^ = r -> q = r @ p
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
q @ p^ = r -> q = r @ p
  destruct p.A: Type
x, y: A
q, r: y = x
q @ 1^ = r -> q = r @ 1
  intro h.A: Type
x, y: A
q, r: y = x
h: q @ 1^ = r
q = r @ 1 exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
Defined.

Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
  r @ q = p -> q = r^ @ p.A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
r @ q = p -> q = r^ @ p
Proof.A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
r @ q = p -> q = r^ @ p
  destruct r.A: Type
x, z: A
p, q: x = z
1 @ q = p -> q = 1^ @ p
  intro h.A: Type
x, z: A
p, q: x = z
h: 1 @ q = p
q = 1^ @ p exact ((concat_1p _)^ @ h @ (concat_1p _)^).
Defined.

Definition moveL_pV {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x) :
  q @ p = r -> q = r @ p^.A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
q @ p = r -> q = r @ p^
Proof.A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
q @ p = r -> q = r @ p^
  destruct p.A: Type
y, z: A
q, r: y = z
q @ 1 = r -> q = r @ 1^
  intro h.A: Type
y, z: A
q, r: y = z
h: q @ 1 = r
q = r @ 1^ exact ((concat_p1 _)^ @ h @ (concat_p1 _)^).
Defined.

Definition moveL_1M {A : Type} {x y : A} (p q : x = y) :
  p @ q^ = 1 -> p = q.A: Type
x, y: A
p, q: x = y
p @ q^ = 1 -> p = q
Proof.A: Type
x, y: A
p, q: x = y
p @ q^ = 1 -> p = q
  destruct q.A: Type
x: A
p: x = x
p @ 1^ = 1 -> p = 1
  intro h.A: Type
x: A
p: x = x
h: p @ 1^ = 1
p = 1 exact ((concat_p1 _)^ @ h).
Defined.

Definition moveL_M1 {A : Type} {x y : A} (p q : x = y) :
  q^ @ p = 1 -> p = q.A: Type
x, y: A
p, q: x = y
q^ @ p = 1 -> p = q
Proof.A: Type
x, y: A
p, q: x = y
q^ @ p = 1 -> p = q
  destruct q.A: Type
x: A
p: x = x
1^ @ p = 1 -> p = 1
  intro h.A: Type
x: A
p: x = x
h: 1^ @ p = 1
p = 1 exact ((concat_1p _)^ @ h).
Defined.

Definition moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  p @ q = 1 -> p = q^.A: Type
x, y: A
p: x = y
q: y = x
p @ q = 1 -> p = q^
Proof.A: Type
x, y: A
p: x = y
q: y = x
p @ q = 1 -> p = q^
  destruct q.A: Type
y: A
p: y = y
p @ 1 = 1 -> p = 1^
  intro h.A: Type
y: A
p: y = y
h: p @ 1 = 1
p = 1^ exact ((concat_p1 _)^ @ h).
Defined.

Definition moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  q @ p = 1 -> p = q^.A: Type
x, y: A
p: x = y
q: y = x
q @ p = 1 -> p = q^
Proof.A: Type
x, y: A
p: x = y
q: y = x
q @ p = 1 -> p = q^
  destruct q.A: Type
y: A
p: y = y
1 @ p = 1 -> p = 1^
  intro h.A: Type
y: A
p: y = y
h: 1 @ p = 1
p = 1^ exact ((concat_1p _)^ @ h).
Defined.

Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
  1 = p^ @ q -> p = q.A: Type
x, y: A
p, q: x = y
1 = p^ @ q -> p = q
Proof.A: Type
x, y: A
p, q: x = y
1 = p^ @ q -> p = q
  destruct p.A: Type
x: A
q: x = x
1 = 1^ @ q -> 1 = q
  intro h.A: Type
x: A
q: x = x
h: 1 = 1^ @ q
1 = q exact (h @ (concat_1p _)).
Defined.

Definition moveR_1M {A : Type} {x y : A} (p q : x = y) :
  1 = q @ p^ -> p = q.A: Type
x, y: A
p, q: x = y
1 = q @ p^ -> p = q
Proof.A: Type
x, y: A
p, q: x = y
1 = q @ p^ -> p = q
  destruct p.A: Type
x: A
q: x = x
1 = q @ 1^ -> 1 = q
  intro h.A: Type
x: A
q: x = x
h: 1 = q @ 1^
1 = q exact (h @ (concat_p1 _)).
Defined.

Definition moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = q @ p -> p^ = q.A: Type
x, y: A
p: x = y
q: y = x
1 = q @ p -> p^ = q
Proof.A: Type
x, y: A
p: x = y
q: y = x
1 = q @ p -> p^ = q
  destruct p.A: Type
x: A
q: x = x
1 = q @ 1 -> 1^ = q
  intro h.A: Type
x: A
q: x = x
h: 1 = q @ 1
1^ = q exact (h @ (concat_p1 _)).
Defined.

Definition moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x) :
  1 = p @ q -> p^ = q.A: Type
x, y: A
p: x = y
q: y = x
1 = p @ q -> p^ = q
Proof.A: Type
x, y: A
p: x = y
q: y = x
1 = p @ q -> p^ = q
  destruct p.A: Type
x: A
q: x = x
1 = 1 @ q -> 1^ = q
  intro h.A: Type
x: A
q: x = x
h: 1 = 1 @ q
1^ = q exact (h @ (concat_1p _)).
Defined.

(* In general, the path we want to move might be arbitrarily deeply nested at the beginning of a long concatenation.  Thus, instead of defining functions such as [moveL_Mp_p], we define a tactical that can repeatedly rewrite with associativity to expose it. *)
Ltac with_rassoc tac :=
  repeat rewrite concat_pp_p;
  tac;
  (* After moving, we reassociate to the left (the canonical direction for paths). *)
  repeat rewrite concat_p_pp.

Ltac rewrite_moveL_Mp_p := with_rassoc ltac:(apply moveL_Mp).
Ltac rewrite_moveL_Vp_p := with_rassoc ltac:(apply moveL_Vp).
Ltac rewrite_moveR_Mp_p := with_rassoc ltac:(apply moveR_Mp).
Ltac rewrite_moveR_Vp_p := with_rassoc ltac:(apply moveR_Vp).

Definition moveR_transport_p {A : Type} (P : A -> Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
  : u = p^ # v -> p # u = v.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
u = transport P p^ v -> transport P p u = v
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
u = transport P p^ v -> transport P p u = v
  destruct p.A: Type
P: A -> Type
x: A
u, v: P x
u = transport P 1^ v -> transport P 1 u = v
  exact idmap.
Defined.

Definition moveR_transport_V {A : Type} (P : A -> Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
  : u = p # v -> p^ # u = v.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
u = transport P p v -> transport P p^ u = v
Proof.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
u = transport P p v -> transport P p^ u = v
  destruct p.A: Type
P: A -> Type
y: A
u, v: P y
u = transport P 1 v -> transport P 1^ u = v
  exact idmap.
Defined.

Definition moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
  : p # u = v -> u = p^ # v.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
transport P p u = v -> u = transport P p^ v
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
transport P p u = v -> u = transport P p^ v
  destruct p.A: Type
P: A -> Type
x: A
u, v: P x
transport P 1 u = v -> u = transport P 1^ v
  exact idmap.
Defined.

Definition moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
  : p^ # u = v -> u = p # v.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
transport P p^ u = v -> u = transport P p v
Proof.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
transport P p^ u = v -> u = transport P p v
  destruct p.A: Type
P: A -> Type
y: A
u, v: P y
transport P 1^ u = v -> u = transport P 1 v
  exact idmap.
Defined.

(* We have some coherences between those proofs. *)
Definition moveR_transport_p_V {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : u = p^ # v)
  : (moveR_transport_p P p u v q)^ = moveL_transport_p P p v u q^.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: u = transport P p^ v
(moveR_transport_p P p u v q)^ =
moveL_transport_p P p v u q^
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: u = transport P p^ v
(moveR_transport_p P p u v q)^ =
moveL_transport_p P p v u q^
  destruct p; reflexivity.
Defined.

Definition moveR_transport_V_V {A : Type} (P : A -> Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : u = p # v)
  : (moveR_transport_V P p u v q)^ = moveL_transport_V P p v u q^.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: u = transport P p v
(moveR_transport_V P p u v q)^ =
moveL_transport_V P p v u q^
Proof.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: u = transport P p v
(moveR_transport_V P p u v q)^ =
moveL_transport_V P p v u q^
  destruct p; reflexivity.
Defined.

Definition moveL_transport_V_V {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : p # u = v)
  : (moveL_transport_V P p u v q)^ = moveR_transport_V P p v u q^.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: transport P p u = v
(moveL_transport_V P p u v q)^ =
moveR_transport_V P p v u q^
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: transport P p u = v
(moveL_transport_V P p u v q)^ =
moveR_transport_V P p v u q^
  destruct p; reflexivity.
Defined.

Definition moveL_transport_p_V {A : Type} (P : A -> Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : p^ # u = v)
  : (moveL_transport_p P p u v q)^ = moveR_transport_p P p v u q^.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: transport P p^ u = v
(moveL_transport_p P p u v q)^ =
moveR_transport_p P p v u q^
Proof.A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: transport P p^ u = v
(moveL_transport_p P p u v q)^ =
moveR_transport_p P p v u q^
  destruct p; reflexivity.
Defined.


(** *** Functoriality of functions *)

(** Here we prove that functions behave like functors between groupoids, and that [ap] itself is functorial. *)

(** Functions take identity paths to identity paths. *)
Definition ap_1 {A B : Type} (x : A) (f : A -> B) :
  ap f 1 = 1 :> (f x = f x)
  :=
  1.

Definition apD_1 {A B} (x : A) (f : forall x : A, B x) :
  apD f 1 = 1 :> (f x = f x)
  :=
  1.

(** Functions commute with concatenation. *)
Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
  ap f (p @ q) = (ap f p) @ (ap f q)
  :=
  match q with
    idpath =>
    match p with idpath => 1 end
  end.

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).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
Proof.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
  destruct p, q.A, B: Type
f: A -> B
w: B
x: A
r: w = f x
r @ ap f (1 @ 1) = (r @ ap f 1) @ ap f 1 simpl.A, B: Type
f: A -> B
w: B
x: A
r: w = f x
r @ 1 = (r @ 1) @ 1 exact (concat_p_pp r 1 1).
Defined.

Definition ap_pp_p {A B : Type} (f : A -> B) {x y z : A} {w : B}
  (p : x = y) (q : y = z) (r : f z = w) :
  (ap f (p @ q)) @ r = (ap f p) @ (ap f q @ r).A, B: Type
f: A -> B
x, y, z: A
w: B
p: x = y
q: y = z
r: f z = w
ap f (p @ q) @ r = ap f p @ (ap f q @ r)
Proof.A, B: Type
f: A -> B
x, y, z: A
w: B
p: x = y
q: y = z
r: f z = w
ap f (p @ q) @ r = ap f p @ (ap f q @ r)
  destruct p, q.A, B: Type
f: A -> B
x: A
w: B
r: f x = w
ap f (1 @ 1) @ r = ap f 1 @ (ap f 1 @ r) simpl.A, B: Type
f: A -> B
x: A
w: B
r: f x = w
1 @ r = 1 @ (1 @ r) exact (concat_pp_p 1 1 r).
Defined.

(** Functions commute with path inverses. *)
Definition inverse_ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
  (ap f p)^ = ap f (p^)
  :=
  match p with idpath => 1 end.

Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
  ap f (p^) = (ap f p)^
  :=
  match p with idpath => 1 end.

(** [ap] itself is functorial in the first argument. *)

Definition ap_idmap {A : Type} {x y : A} (p : x = y) :
  ap idmap p = p
  :=
  match p with idpath => 1 end.

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.

(* Sometimes we don't have the actual function [compose]. *)
Definition ap_compose' {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
  ap (fun a => g (f a)) p = ap g (ap f p)
  :=
  match p with idpath => 1 end.

(** The action of constant maps. *)
Definition ap_const {A B : Type} {x y : A} (p : x = y) (z : B) :
  ap (fun _ => z) p = 1
  :=
  match p with idpath => idpath end.

(** Naturality of [ap]. *)
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_p1 _
  end.

(* A useful variant of concat_Ap. *)
Definition ap_homotopic {A B : Type} {f g : A -> B} (p : forall x, f x = g x) {x y : A} (q : x = y)
  : (ap f q) = (p x) @ (ap g q) @ (p y)^.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
ap f q = (p x @ ap g q) @ (p y)^
Proof.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
ap f q = (p x @ ap g q) @ (p y)^
  apply moveL_pV.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
ap f q @ p y = p x @ ap g q
  apply concat_Ap.
Defined.

(** Naturality of [ap] at identity. *)
Definition concat_A1p {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y) :
  (ap f q) @ (p y) = (p x) @ q
  :=
  match q with
    | idpath => concat_1p_p1 _
  end.

(* The corresponding variant of concat_A1p. *)
Definition ap_homotopic_id {A : Type} {f : A -> A} (p : forall x, f x = x) {x y : A} (q : x = y)
  : (ap f q) = (p x) @ q @ (p y)^.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
ap f q = (p x @ q) @ (p y)^
Proof.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
ap f q = (p x @ q) @ (p y)^
  apply moveL_pV.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
ap f q @ p y = p x @ q
  apply concat_A1p.
Defined.

Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) :
  (p x) @ (ap f q) =  q @ (p y)
  :=
  match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
    | idpath => concat_p1_1p _
  end.

Definition apD_homotopic {A : Type} {B : A -> Type} {f g : forall x, B x}
  (p : forall x, f x = g x) {x y : A} (q : x = y)
  : apD f q = ap (transport B q) (p x) @ apD g q @ (p y)^.A: Type
B: A -> Type
f, g: forall x : A, B x
p: forall x : A, f x = g x
x, y: A
q: x = y
apD f q =
(ap (transport B q) (p x) @ apD g q) @ (p y)^
Proof.A: Type
B: A -> Type
f, g: forall x : A, B x
p: forall x : A, f x = g x
x, y: A
q: x = y
apD f q =
(ap (transport B q) (p x) @ apD g q) @ (p y)^
  apply moveL_pV.A: Type
B: A -> Type
f, g: forall x : A, B x
p: forall x : A, f x = g x
x, y: A
q: x = y
apD f q @ p y = ap (transport B q) (p x) @ apD g q
  destruct q; unfold apD, transport.A: Type
B: A -> Type
f, g: forall x : A, B x
p: forall x : A, f x = g x
x: A
1 @ p x = ap idmap (p x) @ 1
  symmetry.A: Type
B: A -> Type
f, g: forall x : A, B x
p: forall x : A, f x = g x
x: A
ap idmap (p x) @ 1 = 1 @ p x
  exact (concat_p1 _ @ ap_idmap _ @ (concat_1p _)^).
Defined.

(** Naturality with other paths hanging around. *)
Definition concat_pA_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
  {x y : A} (q : x = y)
  {w z : B} (r : w = f x) (s : g y = z)
  :
  (r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s).A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
w, z: B
r: w = f x
s: g y = z
(r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s)
Proof.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
w, z: B
r: w = f x
s: g y = z
(r @ ap f q) @ (p y @ s) = (r @ p x) @ (ap g q @ s)
  destruct q, s; simpl.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x: A
w: B
r: w = f x
(r @ 1) @ (p x @ 1) = (r @ p x) @ 1
  induction (p x).A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x: A
w: B
r: w = f x
(r @ 1) @ (1 @ 1) = (r @ 1) @ 1
  reflexivity.
Defined.

Definition concat_pA_p {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
  {x y : A} (q : x = y)
  {w : B} (r : w = f x)
  :
  (r @ ap f q) @ p y = (r @ p x) @ ap g q.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
w: B
r: w = f x
(r @ ap f q) @ p y = (r @ p x) @ ap g q
Proof.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
w: B
r: w = f x
(r @ ap f q) @ p y = (r @ p x) @ ap g q
  destruct q; simpl.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x: A
w: B
r: w = f x
(r @ 1) @ p x = (r @ p x) @ 1
  induction (p x).A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x: A
w: B
r: w = f x
(r @ 1) @ 1 = (r @ 1) @ 1
  reflexivity.
Defined.

Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
  {x y : A} (q : x = y)
  {z : B} (s : g y = z)
  :
  (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
z: B
s: g y = z
ap f q @ (p y @ s) = p x @ (ap g q @ s)
Proof.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x, y: A
q: x = y
z: B
s: g y = z
ap f q @ (p y @ s) = p x @ (ap g q @ s)
  destruct q, s; cbn.A, B: Type
f, g: A -> B
p: forall x : A, f x = g x
x: A
1 @ (p x @ 1) = p x @ 1
  apply concat_1p.
Defined.

Definition concat_pA1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
  {x y : A} (q : x = y)
  {w z : A} (r : w = f x) (s : y = z)
  :
  (r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s).A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
w, z: A
r: w = f x
s: y = z
(r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s)
Proof.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
w, z: A
r: w = f x
s: y = z
(r @ ap f q) @ (p y @ s) = (r @ p x) @ (q @ s)
  destruct q, s; simpl.A: Type
f: A -> A
p: forall x : A, f x = x
x, w: A
r: w = f x
(r @ 1) @ (p x @ 1) = (r @ p x) @ 1
  induction (p x).A: Type
f: A -> A
p: forall x : A, f x = x
x, w: A
r: w = f x
(r @ 1) @ (1 @ 1) = (r @ 1) @ 1
  reflexivity.
Defined.

Definition concat_pp_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
  {x y : A} (q : x = y)
  {w z : A} (r : w = x) (s : g y = z)
  :
  (r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s).A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
w, z: A
r: w = x
s: g y = z
(r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s)
Proof.A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
w, z: A
r: w = x
s: g y = z
(r @ p x) @ (ap g q @ s) = (r @ q) @ (p y @ s)
  destruct q, s; simpl.A: Type
g: A -> A
p: forall x : A, x = g x
x, w: A
r: w = x
(r @ p x) @ 1 = (r @ 1) @ (p x @ 1)
  induction (p x).A: Type
g: A -> A
p: forall x : A, x = g x
x, w: A
r: w = x
(r @ 1) @ 1 = (r @ 1) @ (1 @ 1)
  reflexivity.
Defined.

Definition concat_pA1_p {A : Type} {f : A -> A} (p : forall x, f x = x)
  {x y : A} (q : x = y)
  {w : A} (r : w = f x)
  :
  (r @ ap f q) @ p y = (r @ p x) @ q.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
w: A
r: w = f x
(r @ ap f q) @ p y = (r @ p x) @ q
Proof.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
w: A
r: w = f x
(r @ ap f q) @ p y = (r @ p x) @ q
  destruct q; simpl.A: Type
f: A -> A
p: forall x : A, f x = x
x, w: A
r: w = f x
(r @ 1) @ p x = (r @ p x) @ 1
  induction (p x).A: Type
f: A -> A
p: forall x : A, f x = x
x, w: A
r: w = f x
(r @ 1) @ 1 = (r @ 1) @ 1
  reflexivity.
Defined.

Definition concat_A1_pp {A : Type} {f : A -> A} (p : forall x, f x = x)
  {x y : A} (q : x = y)
  {z : A} (s : y = z)
  :
  (ap f q) @ (p y @ s) = (p x) @ (q @ s).A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
z: A
s: y = z
ap f q @ (p y @ s) = p x @ (q @ s)
Proof.A: Type
f: A -> A
p: forall x : A, f x = x
x, y: A
q: x = y
z: A
s: y = z
ap f q @ (p y @ s) = p x @ (q @ s)
  destruct q, s; cbn.A: Type
f: A -> A
p: forall x : A, f x = x
x: A
1 @ (p x @ 1) = p x @ 1
  apply concat_1p.
Defined.

Definition concat_pp_A1 {A : Type} {g : A -> A} (p : forall x, x = g x)
  {x y : A} (q : x = y)
  {w : A} (r : w = x)
  :
  (r @ p x) @ ap g q = (r @ q) @ p y.A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
w: A
r: w = x
(r @ p x) @ ap g q = (r @ q) @ p y
Proof.A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
w: A
r: w = x
(r @ p x) @ ap g q = (r @ q) @ p y
  destruct q; simpl.A: Type
g: A -> A
p: forall x : A, x = g x
x, w: A
r: w = x
(r @ p x) @ 1 = (r @ 1) @ p x
  induction (p x).A: Type
g: A -> A
p: forall x : A, x = g x
x, w: A
r: w = x
(r @ 1) @ 1 = (r @ 1) @ 1
  reflexivity.
Defined.

Definition concat_p_A1p {A : Type} {g : A -> A} (p : forall x, x = g x)
  {x y : A} (q : x = y)
  {z : A} (s : g y = z)
  :
  p x @ (ap g q @ s) = q @ (p y @ s).A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
z: A
s: g y = z
p x @ (ap g q @ s) = q @ (p y @ s)
Proof.A: Type
g: A -> A
p: forall x : A, x = g x
x, y: A
q: x = y
z: A
s: g y = z
p x @ (ap g q @ s) = q @ (p y @ s)
  destruct q, s; simpl.A: Type
g: A -> A
p: forall x : A, x = g x
x: A
p x @ 1 = 1 @ (p x @ 1)
  symmetry; apply concat_1p.
Defined.

(** Some coherence lemmas for functoriality *)

Lemma concat_1p_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_1p p @ q = ap (fun p' => 1 @ p') q.A: Type
x: A
p: x = x
q: p = 1
concat_1p p @ q = ap (fun p' : x = x => 1 @ p') q
Proof.A: Type
x: A
p: x = x
q: p = 1
concat_1p p @ q = ap (fun p' : x = x => 1 @ p') q
  rewrite <- (inv_V q).A: Type
x: A
p: x = x
q: p = 1
concat_1p p @ (q^)^ =
ap (fun p' : x = x => 1 @ p') (q^)^
  set (r := q^).A: Type
x: A
p: x = x
q: p = 1
r:= q^: 1 = p
concat_1p p @ r^ = ap (fun p' : x = x => 1 @ p') r^ clearbody r; clear q; destruct r.A: Type
x: A
concat_1p 1 @ 1^ = ap (fun p' : x = x => 1 @ p') 1^
  reflexivity.
Defined.

Lemma concat_p1_1 {A} {x : A} (p : x = x) (q : p = 1)
: concat_p1 p @ q = ap (fun p' => p' @ 1) q.A: Type
x: A
p: x = x
q: p = 1
concat_p1 p @ q = ap (fun p' : x = x => p' @ 1) q
Proof.A: Type
x: A
p: x = x
q: p = 1
concat_p1 p @ q = ap (fun p' : x = x => p' @ 1) q
  rewrite <- (inv_V q).A: Type
x: A
p: x = x
q: p = 1
concat_p1 p @ (q^)^ =
ap (fun p' : x = x => p' @ 1) (q^)^
  set (r := q^).A: Type
x: A
p: x = x
q: p = 1
r:= q^: 1 = p
concat_p1 p @ r^ = ap (fun p' : x = x => p' @ 1) r^ clearbody r; clear q; destruct r.A: Type
x: A
concat_p1 1 @ 1^ = ap (fun p' : x = x => p' @ 1) 1^
  reflexivity.
Defined.

(** *** Action of [apD10] and [ap10] on paths. *)

(** Application of paths between functions preserves the groupoid structure *)

Definition apD10_1 {A} {B:A->Type} (f : forall x, B x) (x:A)
  : apD10 (idpath f) x = 1
:= 1.

Definition apD10_pp {A} {B:A->Type} {f f' f'' : forall x, B x}
  (h:f=f') (h':f'=f'') (x:A)
: apD10 (h @ h') x = apD10 h x @ apD10 h' x.A: Type
B: A -> Type
f, f', f'': forall x : A, B x
h: f = f'
h': f' = f''
x: A
apD10 (h @ h') x = apD10 h x @ apD10 h' x
Proof.A: Type
B: A -> Type
f, f', f'': forall x : A, B x
h: f = f'
h': f' = f''
x: A
apD10 (h @ h') x = apD10 h x @ apD10 h' x
  case h, h'; reflexivity.
Defined.

Definition apD10_V {A} {B:A->Type} {f g : forall x, B x} (h:f=g) (x:A)
  : apD10 (h^) x = (apD10 h x)^
:= match h with idpath => 1 end.

Definition ap10_1 {A B} {f:A->B} (x:A) : ap10 (idpath f) x = 1
  := 1.

Definition ap10_pp {A B} {f f' f'':A->B} (h:f=f') (h':f'=f'') (x:A)
  : ap10 (h @ h') x = ap10 h x @ ap10 h' x
:= apD10_pp h h' x.

Definition ap10_V {A B} {f g : A->B} (h : f = g) (x:A)
  : ap10 (h^) x = (ap10 h x)^
:= apD10_V h x.

(** [apD10] and [ap10] also behave nicely on paths produced by [ap] *)
Definition apD10_ap_precompose {A B C} (f : A -> B) {g g' : forall x:B, C x} (p : g = g') a
: apD10 (ap (fun h : forall x:B, C x => h oD f) p) a = apD10 p (f a).A, B: Type
C: B -> Type
f: A -> B
g, g': forall x : B, C x
p: g = g'
a: A
apD10 (ap (fun h : forall x : B, C x => h oD f) p) a =
apD10 p (f a)
Proof.A, B: Type
C: B -> Type
f: A -> B
g, g': forall x : B, C x
p: g = g'
a: A
apD10 (ap (fun h : forall x : B, C x => h oD f) p) a =
apD10 p (f a)
  destruct p; reflexivity.
Defined.

Definition ap10_ap_precompose {A B C} (f : A -> B) {g g' : B -> C} (p : g = g') a
: ap10 (ap (fun h : B -> C => h o f) p) a = ap10 p (f a)
:= apD10_ap_precompose f p a.

Definition apD10_ap_postcompose {A B C} (f : forall x, B x -> C) {g g' : forall x:A, B x} (p : g = g') a
: apD10 (ap (fun h : forall x:A, B x => fun x => f x (h x)) p) a = ap (f a) (apD10 p a).A: Type
B: A -> Type
C: Type
f: forall x : A, B x -> C
g, g': forall x : A, B x
p: g = g'
a: A
apD10
  (ap
     (fun (h : forall x : A, B x) (x : A) => f x (h x))
     p) a = ap (f a) (apD10 p a)
Proof.A: Type
B: A -> Type
C: Type
f: forall x : A, B x -> C
g, g': forall x : A, B x
p: g = g'
a: A
apD10
  (ap
     (fun (h : forall x : A, B x) (x : A) => f x (h x))
     p) a = ap (f a) (apD10 p a)
  destruct p; reflexivity.
Defined.

Definition ap10_ap_postcompose {A B C} (f : B -> C) {g g' : A -> B} (p : g = g') a
: ap10 (ap (fun h : A -> B => f o h) p) a = ap f (ap10 p a)
:= apD10_ap_postcompose (fun a => f) p a.

Definition ap100 {X Y Z : Type} {f g : X -> Y -> Z} (p : f = g) (x : X) (y : Y)
  : f x y = g x y := (ap10 (ap10 p x) y).

(** *** Transport and the groupoid structure of paths *)

Definition transport_1 {A : Type} (P : A -> Type) {x : A} (u : P x)
  : 1 # u = u
:= 1.

Definition transport_pp {A : Type} (P : A -> Type) {x y z : A} (p : x = y) (q : y = z) (u : P x) :
  p @ q # u = q # p # u :=
  match q with idpath =>
    match p with idpath => 1 end
  end.

Definition transport_pV {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P y)
  : p # p^ # z = z
  := (transport_pp P p^ p z)^
  @ ap (fun r => transport P r z) (concat_Vp p).

Definition transport_Vp {A : Type} (P : A -> Type) {x y : A} (p : x = y) (z : P x)
  : p^ # p # z = z
  := (transport_pp P p p^ z)^
  @ ap (fun r => transport P r z) (concat_pV p).

(** In the future, we may expect to need some higher coherence for transport:
  for instance, that transport acting on the associator is trivial. *)
Definition transport_p_pp {A : Type} (P : A -> Type)
  {x y z w : A} (p : x = y) (q : y = z) (r : z = w)
  (u : P x)
  : ap (fun e => e # u) (concat_p_pp p q r)
    @ (transport_pp P (p@q) r u) @ ap (transport P r) (transport_pp P p q u)
  = (transport_pp P p (q@r) u) @ (transport_pp P q r (p#u))
  :> ((p @ (q @ r)) # u = r # q # p # u) .A: Type
P: A -> Type
x, y, z, w: A
p: x = y
q: y = z
r: z = w
u: P x
(ap (fun e : x = w => transport P e u)
   (concat_p_pp p q r) @ transport_pp P (p @ q) r u) @
ap (transport P r) (transport_pp P p q u) =
transport_pp P p (q @ r) u @
transport_pp P q r (transport P p u)
Proof.A: Type
P: A -> Type
x, y, z, w: A
p: x = y
q: y = z
r: z = w
u: P x
(ap (fun e : x = w => transport P e u)
   (concat_p_pp p q r) @ transport_pp P (p @ q) r u) @
ap (transport P r) (transport_pp P p q u) =
transport_pp P p (q @ r) u @
transport_pp P q r (transport P p u)
  destruct p, q, r.A: Type
P: A -> Type
x: A
u: P x
(ap (fun e : x = x => transport P e u)
   (concat_p_pp 1 1 1) @ transport_pp P (1 @ 1) 1 u) @
ap (transport P 1) (transport_pp P 1 1 u) =
transport_pp P 1 (1 @ 1) u @
transport_pp P 1 1 (transport P 1 u)  simpl.A: Type
P: A -> Type
x: A
u: P x
1 = 1  exact 1.
Defined.

(* Here are other coherence lemmas for transport. *)
Definition transport_pVp {A} (P : A -> Type) {x y:A} (p:x=y) (z:P x)
  : transport_pV P p (transport P p z)
  = ap (transport P p) (transport_Vp P p z).A: Type
P: A -> Type
x, y: A
p: x = y
z: P x
transport_pV P p (transport P p z) =
ap (transport P p) (transport_Vp P p z)
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
z: P x
transport_pV P p (transport P p z) =
ap (transport P p) (transport_Vp P p z)
  destruct p; reflexivity.
Defined.

Definition transport_VpV {A} (P : A -> Type) {x y : A} (p : x = y) (z : P y)
  : transport_Vp P p (transport P p^ z)
    = ap (transport P p^) (transport_pV P p z).A: Type
P: A -> Type
x, y: A
p: x = y
z: P y
transport_Vp P p (transport P p^ z) =
ap (transport P p^) (transport_pV P p z)
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
z: P y
transport_Vp P p (transport P p^ z) =
ap (transport P p^) (transport_pV P p z)
  destruct p; reflexivity.
Defined.

Definition ap_transport_transport_pV {A} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (e : transport P p u = v)
  : ap (transport P p) (moveL_transport_V P p u v e)
       @ transport_pV P p v = e.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
e: transport P p u = v
ap (transport P p) (moveL_transport_V P p u v e) @
transport_pV P p v = e
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
e: transport P p u = v
ap (transport P p) (moveL_transport_V P p u v e) @
transport_pV P p v = e
    by destruct e, p.
Defined.

Definition moveL_transport_V_1 {A} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x)
  : moveL_transport_V P p u (p # u) 1 = (transport_Vp P p u)^.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
moveL_transport_V P p u (transport P p u) 1 =
(transport_Vp P p u)^
    (* moveL_transport_V P p (transport P p^ v) (transport P p (transport P p^ v)) 1 *)
    (* = ap (transport P p^) (transport_pV P p v)^. *)
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
moveL_transport_V P p u (transport P p u) 1 =
(transport_Vp P p u)^
  (* pose (u := p^ # v).  *)
  (* assert (moveL_transport_V P p u (p # u) 1 = (transport_Vp P p u)^). *)
  destruct p; reflexivity.
  (* subst u. rewrite X. *)
Defined.

(** Occasionally the induction principles for the identity type show up explicitly; these let us turn them into transport. *)
Definition paths_rect_transport {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x)
  : paths_rect A x (fun a _ => P a) u y p = transport P p u
  := 1.

Definition paths_ind_transport {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x)
  : paths_ind x (fun a _ => P a) u y p = transport P p u
  := 1.

Definition paths_ind_r_transport {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P y)
  : paths_ind_r y (fun b _ => P b) u x p = transport P p^ u.A: Type
P: A -> Type
x, y: A
p: x = y
u: P y
paths_ind_r y (fun (b : A) (_ : b = y) => P b) u x p =
transport P p^ u
Proof.A: Type
P: A -> Type
x, y: A
p: x = y
u: P y
paths_ind_r y (fun (b : A) (_ : b = y) => P b) u x p =
transport P p^ u
  by destruct p.
Defined.

(** ** [ap11] *)

Definition ap11_is_ap10_ap01 {A B} {f g:A->B} (h:f=g) {x y:A} (p:x=y)
: ap11 h p = ap10 h x @ ap g p.A, B: Type
f, g: A -> B
h: f = g
x, y: A
p: x = y
ap11 h p = ap10 h x @ ap g p
Proof.A, B: Type
f, g: A -> B
h: f = g
x, y: A
p: x = y
ap11 h p = ap10 h x @ ap g p
  by path_induction.
Defined.

(** Dependent transport in doubly dependent types and more. *)

Definition transportD {A : Type} (B : A -> Type) (C : forall a:A, B a -> Type)
  {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1 y)
  : C x2 (p # y)
  :=
  match p with idpath => z 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.

(** *** [ap] for curried two variable functions *)

Definition ap011 {A B C} (f : A -> B -> C) {x x' y y'} (p : x = x') (q : y = y')
  : f x y = f x' y'.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
f x y = f x' y'
Proof.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
f x y = f x' y'
  destruct p.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q: y = y'
f x y = f x y'
  apply ap.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q: y = y'
y = y'
  exact q.
Defined.

Definition ap011_V {A B C} (f : A -> B -> C) {x x' y y'} (p : x = x') (q : y = y')
  : ap011 f p^ q^ = (ap011 f p q)^.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 f p^ q^ = (ap011 f p q)^
Proof.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 f p^ q^ = (ap011 f p q)^
  destruct p.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q: y = y'
ap011 f 1^ q^ = (ap011 f 1 q)^
  apply ap_V.
Defined.

Definition ap011_pp {A B C} (f : A -> B -> C) {x x' x'' y y' y''}
  (p : x = x') (p' : x' = x'') (q : y = y') (q' : y' = y'')
  : ap011 f (p @ p') (q @ q') = ap011 f p q @ ap011 f p' q'.A, B, C: Type
f: A -> B -> C
x, x', x'': A
y, y', y'': B
p: x = x'
p': x' = x''
q: y = y'
q': y' = y''
ap011 f (p @ p') (q @ q') =
ap011 f p q @ ap011 f p' q'
Proof.A, B, C: Type
f: A -> B -> C
x, x', x'': A
y, y', y'': B
p: x = x'
p': x' = x''
q: y = y'
q': y' = y''
ap011 f (p @ p') (q @ q') =
ap011 f p q @ ap011 f p' q'
  destruct p, p'.A, B, C: Type
f: A -> B -> C
x: A
y, y', y'': B
q: y = y'
q': y' = y''
ap011 f (1 @ 1) (q @ q') = ap011 f 1 q @ ap011 f 1 q'
  apply ap_pp.
Defined.

Definition ap011_compose {A B C D} (f : A -> B -> C) (g : C -> D) {x x' y y'}
  (p : x = x') (q : y = y')
  : ap011 (fun x y => g (f x y)) p q = ap g (ap011 f p q).A, B, C, D: Type
f: A -> B -> C
g: C -> D
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 (fun (x : A) (y : B) => g (f x y)) p q =
ap g (ap011 f p q)
Proof.A, B, C, D: Type
f: A -> B -> C
g: C -> D
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 (fun (x : A) (y : B) => g (f x y)) p q =
ap g (ap011 f p q)
  destruct p; simpl.A, B, C, D: Type
f: A -> B -> C
g: C -> D
x: A
y, y': B
q: y = y'
ap (fun y : B => g (f x y)) q = ap g (ap (f x) q)
  apply ap_compose.
Defined.

Definition ap011_compose' {A B C D E} (f : A -> B -> C) (g : D -> A) (h : E -> B)
  {x x' y y'}
  (p : x = x') (q : y = y')
  : ap011 (fun x y => f (g x) (h y)) p q = ap011 f (ap g p) (ap h q).A, B, C, D, E: Type
f: A -> B -> C
g: D -> A
h: E -> B
x, x': D
y, y': E
p: x = x'
q: y = y'
ap011 (fun (x : D) (y : E) => f (g x) (h y)) p q =
ap011 f (ap g p) (ap h q)
Proof.A, B, C, D, E: Type
f: A -> B -> C
g: D -> A
h: E -> B
x, x': D
y, y': E
p: x = x'
q: y = y'
ap011 (fun (x : D) (y : E) => f (g x) (h y)) p q =
ap011 f (ap g p) (ap h q)
  destruct p; simpl.A, B, C, D, E: Type
f: A -> B -> C
g: D -> A
h: E -> B
x: D
y, y': E
q: y = y'
ap (fun y : E => f (g x) (h y)) q =
ap (f (g x)) (ap h q)
  apply ap_compose.
Defined.

Definition ap011_is_ap {A B C} (f : A -> B -> C) {x x' : A} {y y' : B} (p : x = x') (q : y = y')
  : ap011 f p q = ap (fun x => f x y) p @ ap (fun y => f x' y) q.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 f p q =
ap (fun x : A => f x y) p @ ap (fun y : B => f x' y) q
Proof.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p: x = x'
q: y = y'
ap011 f p q =
ap (fun x : A => f x y) p @ ap (fun y : B => f x' y) q
  destruct p.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q: y = y'
ap011 f 1 q =
ap (fun x : A => f x y) 1 @ ap (fun y : B => f x y) q
  symmetry.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q: y = y'
ap (fun x : A => f x y) 1 @ ap (fun y : B => f x y) q =
ap011 f 1 q
  apply concat_1p.
Defined.

(** It would be nice to have a consistent way to name the different ways in which this can be dependent.  The following are a sort of half-hearted attempt. *)

Definition ap011D {A B C} (f : forall (a:A), B a -> C)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: f x y = f x' y'.A: Type
B: A -> Type
C: Type
f: forall a : A, B a -> C
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
f x y = f x' y'
Proof.A: Type
B: A -> Type
C: Type
f: forall a : A, B a -> C
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
f x y = f x' y'
  destruct p, q; reflexivity.
Defined.

Definition ap01D1 {A B C} (f : forall (a:A), B a -> C a)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: transport C p (f x y) = f x' y'.A: Type
B, C: A -> Type
f: forall a : A, B a -> C a
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
transport C p (f x y) = f x' y'
Proof.A: Type
B, C: A -> Type
f: forall a : A, B a -> C a
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
transport C p (f x y) = f x' y'
  destruct p, q; reflexivity.
Defined.

Definition apD011 {A B C} (f : forall (a:A) (b:B a), C a b)
           {x x'} (p : x = x') {y y'} (q : p # y = y')
: transport (C x') q (transportD B C p y (f x y)) = f x' y'.A: Type
B: A -> Type
C: forall x : A, B x -> Type
f: forall (a : A) (b : B a), C a b
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
transport (C x') q (transportD B C p y (f x y)) =
f x' y'
Proof.A: Type
B: A -> Type
C: forall x : A, B x -> Type
f: forall (a : A) (b : B a), C a b
x, x': A
p: x = x'
y: B x
y': B x'
q: transport B p y = y'
transport (C x') q (transportD B C p y (f x y)) =
f x' y'
  destruct p, q; reflexivity.
Defined.

(** Transporting along two 1-dimensional paths *)
Definition transport011 {A B} (P : A -> B -> Type) {x1 x2 : A} {y1 y2 : B}
  (p : x1 = x2) (q : y1 = y2) (z : P x1 y1)
  : P x2 y2
  := transport (fun x => P x y2) p (transport (fun y => P x1 y) q z).

Definition transport011_pp {A B} (P : A -> B -> Type) {x1 x2 x3 : A} {y1 y2 y3 : B}
  (p1 : x1 = x2) (p2 : x2 = x3) (q1 : y1 = y2) (q2 : y2 = y3) (z : P x1 y1)
  : transport011 P (p1 @ p2) (q1 @ q2) z
    = transport011 P p2 q2 (transport011 P p1 q1 z).A, B: Type
P: A -> B -> Type
x1, x2, x3: A
y1, y2, y3: B
p1: x1 = x2
p2: x2 = x3
q1: y1 = y2
q2: y2 = y3
z: P x1 y1
transport011 P (p1 @ p2) (q1 @ q2) z =
transport011 P p2 q2 (transport011 P p1 q1 z)
Proof.A, B: Type
P: A -> B -> Type
x1, x2, x3: A
y1, y2, y3: B
p1: x1 = x2
p2: x2 = x3
q1: y1 = y2
q2: y2 = y3
z: P x1 y1
transport011 P (p1 @ p2) (q1 @ q2) z =
transport011 P p2 q2 (transport011 P p1 q1 z)
  destruct p1, p2, q1, q2; reflexivity.
Defined.

Definition transport011_compose {A B A' B'} (P : A -> B -> Type) (f : A' -> A) (g : B' -> B)
  {x1 x2 : A'} {y1 y2 : B'} (p : x1 = x2) (q : y1 = y2) (z : P (f x1) (g y1))
  : transport011 (fun x y => P (f x) (g y)) p q z
   = transport011 P (ap f p) (ap g q) z.A, B, A', B': Type
P: A -> B -> Type
f: A' -> A
g: B' -> B
x1, x2: A'
y1, y2: B'
p: x1 = x2
q: y1 = y2
z: P (f x1) (g y1)
transport011 (fun (x : A') (y : B') => P (f x) (g y))
  p q z = transport011 P (ap f p) (ap g q) z
Proof.A, B, A', B': Type
P: A -> B -> Type
f: A' -> A
g: B' -> B
x1, x2: A'
y1, y2: B'
p: x1 = x2
q: y1 = y2
z: P (f x1) (g y1)
transport011 (fun (x : A') (y : B') => P (f x) (g y))
  p q z = transport011 P (ap f p) (ap g q) z
  destruct p, q; reflexivity.
Defined.

(** Naturality of [transport011]. *)
Definition ap_transport011{A B} {P Q : A -> B -> Type}
  {a1 a2 : A} {b1 b2 : B} (p : a1 = a2) (q : b1 = b2)  
  (f : forall {a b}, P a b -> Q a b) (x : P a1 b1)
  : f (transport011 P p q x) = transport011 Q p q (f x).A, B: Type
P, Q: A -> B -> Type
a1, a2: A
b1, b2: B
p: a1 = a2
q: b1 = b2
f: forall (a : A) (b : B), P a b -> Q a b
x: P a1 b1
f a2 b2 (transport011 P p q x) =
transport011 Q p q (f a1 b1 x)
Proof.A, B: Type
P, Q: A -> B -> Type
a1, a2: A
b1, b2: B
p: a1 = a2
q: b1 = b2
f: forall (a : A) (b : B), P a b -> Q a b
x: P a1 b1
f a2 b2 (transport011 P p q x) =
transport011 Q p q (f a1 b1 x)
  destruct p, q; reflexivity.
Defined.

(** Transporting along higher-dimensional paths *)

Definition transport2 {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
  (r : p = q) (z : P x)
  : p # z = q # z
  := ap (fun p' => p' # z) r.

(** An alternative definition. *)
Definition transport2_is_ap10 {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
  (r : p = q) (z : Q x)
  : transport2 Q r z = ap10 (ap (transport Q) r) z
  := match r with idpath => 1 end.

Definition transport2_p2p {A : Type} (P : A -> Type) {x y : A} {p1 p2 p3 : x = y}
  (r1 : p1 = p2) (r2 : p2 = p3) (z : P x)
  : transport2 P (r1 @ r2) z = transport2 P r1 z @ transport2 P r2 z.A: Type
P: A -> Type
x, y: A
p1, p2, p3: x = y
r1: p1 = p2
r2: p2 = p3
z: P x
transport2 P (r1 @ r2) z =
transport2 P r1 z @ transport2 P r2 z
Proof.A: Type
P: A -> Type
x, y: A
p1, p2, p3: x = y
r1: p1 = p2
r2: p2 = p3
z: P x
transport2 P (r1 @ r2) z =
transport2 P r1 z @ transport2 P r2 z
  destruct r1, r2; reflexivity.
Defined.

Definition transport2_V {A : Type} (Q : A -> Type) {x y : A} {p q : x = y}
  (r : p = q) (z : Q x)
  : transport2 Q (r^) z = (transport2 Q r z)^
  := match r with idpath => 1 end.

Definition concat_AT {A : Type} (P : A -> Type) {x y : A} {p q : x = y}
  {z w : P x} (r : p = q) (s : z = w)
  : ap (transport P p) s  @  transport2 P r w
    = transport2 P r z  @  ap (transport P q) s
  := match r with idpath => (concat_p1_1p _) end.

Definition transport_pp_1 {A : Type} (P : A -> Type) {a b : A} (p : a = b) (x : P a)
  : transport_pp P p 1 x = transport2 P (concat_p1 p) x.A: Type
P: A -> Type
a, b: A
p: a = b
x: P a
transport_pp P p 1 x = transport2 P (concat_p1 p) x
Proof.A: Type
P: A -> Type
a, b: A
p: a = b
x: P a
transport_pp P p 1 x = transport2 P (concat_p1 p) x
  by induction p.
Defined.

(* TODO: What should this be called? *)
Lemma ap_transport {A} {P Q : A -> Type} {x y : A} (p : x = y) (f : forall x, P x -> Q x) (z : P x) :
  f y (p # z) = (p # (f x z)).A: Type
P, Q: A -> Type
x, y: A
p: x = y
f: forall x : A, P x -> Q x
z: P x
f y (transport P p z) = transport Q p (f x z)
Proof.A: Type
P, Q: A -> Type
x, y: A
p: x = y
f: forall x : A, P x -> Q x
z: P x
f y (transport P p z) = transport Q p (f x z)
  by induction p.
Defined.

Lemma ap_transportD {A : Type}
      (B : A -> Type) (C1 C2 : forall a : A, B a -> Type)
      (f : forall a b, C1 a b -> C2 a b)
      {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C1 x1 y)
: f x2 (p # y) (transportD B C1 p y z)
  = transportD B C2 p y (f x1 y z).A: Type
B: A -> Type
C1, C2: forall a : A, B a -> Type
f: forall (a : A) (b : B a), C1 a b -> C2 a b
x1, x2: A
p: x1 = x2
y: B x1
z: C1 x1 y
f x2 (transport B p y) (transportD B C1 p y z) =
transportD B C2 p y (f x1 y z)
Proof.A: Type
B: A -> Type
C1, C2: forall a : A, B a -> Type
f: forall (a : A) (b : B a), C1 a b -> C2 a b
x1, x2: A
p: x1 = x2
y: B x1
z: C1 x1 y
f x2 (transport B p y) (transportD B C1 p y z) =
transportD B C2 p y (f x1 y z)
  by induction p.
Defined.

Lemma ap_transportD2 {A : Type}
      (B C : A -> Type) (D1 D2 : forall a, B a -> C a -> Type)
      (f : forall a b c, D1 a b c -> D2 a b c)
      {x1 x2 : A} (p : x1 = x2) (y : B x1) (z : C x1) (w : D1 x1 y z)
: f x2 (p # y) (p # z) (transportD2 B C D1 p y z w)
  = transportD2 B C D2 p y z (f x1 y z w).A: Type
B, C: A -> Type
D1, D2: forall a : A, B a -> C a -> Type
f: forall (a : A) (b : B a) (c : C a),
D1 a b c -> D2 a b c
x1, x2: A
p: x1 = x2
y: B x1
z: C x1
w: D1 x1 y z
f x2 (transport B p y) (transport C p z)
  (transportD2 B C D1 p y z w) =
transportD2 B C D2 p y z (f x1 y z w)
Proof.A: Type
B, C: A -> Type
D1, D2: forall a : A, B a -> C a -> Type
f: forall (a : A) (b : B a) (c : C a),
D1 a b c -> D2 a b c
x1, x2: A
p: x1 = x2
y: B x1
z: C x1
w: D1 x1 y z
f x2 (transport B p y) (transport C p z)
  (transportD2 B C D1 p y z w) =
transportD2 B C D2 p y z (f x1 y z w)
  by induction p.
Defined.

(* TODO: What should this be called? *)
Lemma ap_transport_pV {X} (Y : X -> Type) {x1 x2 : X} (p : x1 = x2)
      {y1 y2 : Y x2} (q : y1 = y2)
: ap (transport Y p) (ap (transport Y p^) q) =
  transport_pV Y p y1 @ q @ (transport_pV Y p y2)^.X: Type
Y: X -> Type
x1, x2: X
p: x1 = x2
y1, y2: Y x2
q: y1 = y2
ap (transport Y p) (ap (transport Y p^) q) =
(transport_pV Y p y1 @ q) @ (transport_pV Y p y2)^
Proof.X: Type
Y: X -> Type
x1, x2: X
p: x1 = x2
y1, y2: Y x2
q: y1 = y2
ap (transport Y p) (ap (transport Y p^) q) =
(transport_pV Y p y1 @ q) @ (transport_pV Y p y2)^
  destruct p, q; reflexivity.
Defined.

(* TODO: And this? *)
Definition transport_pV_ap {X} (P : X -> Type) (f : forall x, P x)
      {x1 x2 : X} (p : x1 = x2)
: ap (transport P p) (apD f p^) @ apD f p = transport_pV P p (f x2).X: Type
P: X -> Type
f: forall x : X, P x
x1, x2: X
p: x1 = x2
ap (transport P p) (apD f p^) @ apD f p =
transport_pV P p (f x2)
Proof.X: Type
P: X -> Type
f: forall x : X, P x
x1, x2: X
p: x1 = x2
ap (transport P p) (apD f p^) @ apD f p =
transport_pV P p (f x2)
  destruct p; reflexivity.
Defined.

Definition apD_pp {A} {P : A -> Type} (f : forall x, P x)
           {x y z : A} (p : x = y) (q : y = z)
  : apD f (p @ q)
    = transport_pp P p q (f x) @ ap (transport P q) (apD f p) @ apD f q.A: Type
P: A -> Type
f: forall x : A, P x
x, y, z: A
p: x = y
q: y = z
apD f (p @ q) =
(transport_pp P p q (f x) @
 ap (transport P q) (apD f p)) @ apD f q
Proof.A: Type
P: A -> Type
f: forall x : A, P x
x, y, z: A
p: x = y
q: y = z
apD f (p @ q) =
(transport_pp P p q (f x) @
 ap (transport P q) (apD f p)) @ apD f q
  destruct p, q; reflexivity.
Defined.

Definition apD_V {A} {P : A -> Type} (f : forall x, P x)
           {x y : A} (p : x = y)
  : apD f p^ = moveR_transport_V _ _ _ _ (apD f p)^.A: Type
P: A -> Type
f: forall x : A, P x
x, y: A
p: x = y
apD f p^ =
moveR_transport_V P p (f y) (f x) (apD f p)^
Proof.A: Type
P: A -> Type
f: forall x : A, P x
x, y: A
p: x = y
apD f p^ =
moveR_transport_V P p (f y) (f x) (apD f p)^
  destruct p; reflexivity.
Defined.


(** *** Transporting in particular fibrations. *)

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

(** Transporting in a constant fibration. *)
Definition transport_const {A B : Type} {x1 x2 : A} (p : x1 = x2) (y : B)
  : transport (fun x => B) p y = y.A, B: Type
x1, x2: A
p: x1 = x2
y: B
transport (fun _ : A => B) p y = y
Proof.A, B: Type
x1, x2: A
p: x1 = x2
y: B
transport (fun _ : A => B) p y = y
  destruct p.A, B: Type
x1: A
y: B
transport (fun _ : A => B) 1 y = y  exact 1.
Defined.

Definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 = x2}
  (r : p = q) (y : B)
  : transport_const p y = transport2 (fun _ => B) r y @ transport_const q y
  := match r with idpath => (concat_1p _)^ end.

(** Transporting in a pulled back fibration. *)
Lemma transport_compose {A B} {x y : A} (P : B -> Type) (f : A -> B)
  (p : x = y) (z : P (f x))
  : transport (fun x => P (f x)) p z  =  transport P (ap f p) z.A, B: Type
x, y: A
P: B -> Type
f: A -> B
p: x = y
z: P (f x)
transport (fun x : A => P (f x)) p z =
transport P (ap f p) z
Proof.A, B: Type
x, y: A
P: B -> Type
f: A -> B
p: x = y
z: P (f x)
transport (fun x : A => P (f x)) p z =
transport P (ap f p) z
  destruct p; reflexivity.
Defined.

Lemma transportD_compose {A A'} B {x x' : A} (C : forall x : A', B x -> Type) (f : A -> A')
      (p : x = x') y (z : C (f x) y)
: transportD (B o f) (C oD f) p y z
  = transport (C (f x')) (transport_compose B f p y)^ (transportD B C (ap f p) y z).A, A': Type
B: A' -> Type
x, x': A
C: forall x : A', B x -> Type
f: A -> A'
p: x = x'
y: B (f x)
z: C (f x) y
transportD (B o f) (C oD f) p y z =
transport (C (f x')) (transport_compose B f p y)^
  (transportD B C (ap f p) y z)
Proof.A, A': Type
B: A' -> Type
x, x': A
C: forall x : A', B x -> Type
f: A -> A'
p: x = x'
y: B (f x)
z: C (f x) y
transportD (B o f) (C oD f) p y z =
transport (C (f x')) (transport_compose B f p y)^
  (transportD B C (ap f p) y z)
  destruct p; reflexivity.
Defined.

(* TODO: Is there a lemma like [transportD_compose], but for [apD], which subsumes this? *)
Lemma transport_apD_transportD {A} B (f : forall x : A, B x) (C : forall x, B x -> Type)
      {x1 x2 : A} (p : x1 = x2) (z : C x1 (f x1))
: apD f p # transportD B C p _ z
  = transport (fun x => C x (f x)) p z.A: Type
B: A -> Type
f: forall x : A, B x
C: forall x : A, B x -> Type
x1, x2: A
p: x1 = x2
z: C x1 (f x1)
transport (C x2) (apD f p) (transportD B C p (f x1) z) =
transport (fun x : A => C x (f x)) p z
Proof.A: Type
B: A -> Type
f: forall x : A, B x
C: forall x : A, B x -> Type
x1, x2: A
p: x1 = x2
z: C x1 (f x1)
transport (C x2) (apD f p) (transportD B C p (f x1) z) =
transport (fun x : A => C x (f x)) p z
  destruct p; reflexivity.
Defined.

Lemma transport_precompose {A B C} (f : A -> B) (g g' : B -> C) (p : g = g')
: transport (fun h : B -> C => g o f = h o f) p 1 =
  ap (fun h => h o f) p.A, B, C: Type
f: A -> B
g, g': B -> C
p: g = g'
transport (fun h : B -> C => g o f = h o f) p 1 =
ap (fun h : B -> C => h o f) p
Proof.A, B, C: Type
f: A -> B
g, g': B -> C
p: g = g'
transport (fun h : B -> C => g o f = h o f) p 1 =
ap (fun h : B -> C => h o f) p
  destruct p; reflexivity.
Defined.

(** A special case of [transport_compose] which seems to come up a lot. *)
Definition transport_idmap_ap {A} (P : A -> Type) {x y : A} (p : x = y) (u : P x)
: transport P p u = transport idmap (ap P p) u
  := match p with idpath => idpath end.

(** Sometimes, it's useful to have the goal be in terms of [ap], so we can use lemmas about [ap].  However, we can't just [rewrite !transport_idmap_ap], as that's likely to loop.  So, instead, we provide a tactic [transport_to_ap], that replaces all [transport P p u] with [transport idmap (ap P p) u] for non-[idmap] [P]. *)
Ltac transport_to_ap :=
  repeat match goal with
           | [ |- context[transport ?P ?p ?u] ]
             => match P with
                  | idmap => fail 1 (* we don't want to turn [transport idmap (ap _ _)] into [transport idmap (ap idmap (ap _ _))] *)
                  | _ => idtac
                end;
               progress rewrite (transport_idmap_ap P p u)
         end.

(** Transporting in a fibration dependent on two independent types commutes. *)
Definition transport_transport {A B} (C : A -> B -> Type)
           {x1 x2 : A} (p : x1 = x2) {y1 y2 : B} (q : y1 = y2)
           (c : C x1 y1)
: transport (C x2) q (transport (fun x => C x y1) p c)
  = transport (fun x => C x y2) p (transport (C x1) q c).A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
y1, y2: B
q: y1 = y2
c: C x1 y1
transport (C x2) q
  (transport (fun x : A => C x y1) p c) =
transport (fun x : A => C x y2) p
  (transport (C x1) q c)
Proof.A, B: Type
C: A -> B -> Type
x1, x2: A
p: x1 = x2
y1, y2: B
q: y1 = y2
c: C x1 y1
transport (C x2) q
  (transport (fun x : A => C x y1) p c) =
transport (fun x : A => C x y2) p
  (transport (C x1) q c)
  destruct p, q; reflexivity.
Defined.

(** *** The behavior of [ap] and [apD]. *)

(** In a constant fibration, [apD] reduces to [ap], modulo [transport_const]. *)
Lemma apD_const {A B} {x y : A} (f : A -> B) (p: x = y) :
  apD f p = transport_const p (f x) @ ap f p.A, B: Type
x, y: A
f: A -> B
p: x = y
apD f p = transport_const p (f x) @ ap f p
Proof.A, B: Type
x, y: A
f: A -> B
p: x = y
apD f p = transport_const p (f x) @ ap f p
  destruct p; reflexivity.
Defined.

Definition apD_compose {A A' : Type} {B : A' -> Type} (g : A -> A')
  (f : forall a, B a) {x y : A} (p : x = y)
  : apD (f o g) p  = (transport_compose _ _ _ _) @ apD f (ap g p).A, A': Type
B: A' -> Type
g: A -> A'
f: forall a : A', B a
x, y: A
p: x = y
apD (f o g) p =
transport_compose B g p (f (g x)) @ apD f (ap g p)
Proof.A, A': Type
B: A' -> Type
g: A -> A'
f: forall a : A', B a
x, y: A
p: x = y
apD (f o g) p =
transport_compose B g p (f (g x)) @ apD f (ap g p)
  by destruct p.
Defined.

Definition apD_compose' {A A' : Type} {B : A' -> Type} (g : A -> A')
  (f : forall a, B a) {x y : A} (p : x = y)
  : apD f (ap g p) = (transport_compose B _ _ _)^ @ apD (f o g) p.A, A': Type
B: A' -> Type
g: A -> A'
f: forall a : A', B a
x, y: A
p: x = y
apD f (ap g p) =
(transport_compose B g p (f (g x)))^ @ apD (f o g) p
Proof.A, A': Type
B: A' -> Type
g: A -> A'
f: forall a : A', B a
x, y: A
p: x = y
apD f (ap g p) =
(transport_compose B g p (f (g x)))^ @ apD (f o g) p
  by destruct p.
Defined.

(** ** The 2-dimensional groupoid structure *)

(** Horizontal composition of 2-dimensional paths. *)
Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q')
  : p @ q = p' @ q'
:= match h, h' with idpath, idpath => 1 end.

Notation "p @@ q" := (concat2 p q)%path : path_scope.

Arguments concat2 : simpl nomatch.

Lemma concat2_ap_ap {A B : Type} {x' y' z' : B}
           (f : A -> (x' = y')) (g : A -> (y' = z'))
           {x y : A} (p : x = y)
: (ap f p) @@ (ap g p) = ap (fun u => f u @ g u) p.A, B: Type
x', y', z': B
f: A -> x' = y'
g: A -> y' = z'
x, y: A
p: x = y
ap f p @@ ap g p = ap (fun u : A => f u @ g u) p
Proof.A, B: Type
x', y', z': B
f: A -> x' = y'
g: A -> y' = z'
x, y: A
p: x = y
ap f p @@ ap g p = ap (fun u : A => f u @ g u) p
    by path_induction.
Defined.

(** 2-dimensional path inversion *)
Definition inverse2 {A : Type} {x y : A} {p q : x = y} (h : p = q)
  : p^ = q^
:= ap inverse h.

(** Some higher coherences *)

Lemma ap_pp_concat_p1 {A B} (f : A -> B) {a b : A} (p : a = b)
  : ap_pp f p 1 @ concat_p1 (ap f p) = ap (ap f) (concat_p1 p).A, B: Type
f: A -> B
a, b: A
p: a = b
ap_pp f p 1 @ concat_p1 (ap f p) =
ap (ap f) (concat_p1 p)
Proof.A, B: Type
f: A -> B
a, b: A
p: a = b
ap_pp f p 1 @ concat_p1 (ap f p) =
ap (ap f) (concat_p1 p)
  destruct p; reflexivity.
Defined.

Lemma ap_pp_concat_1p {A B} (f : A -> B) {a b : A} (p : a = b)
  : ap_pp f 1 p @ concat_1p (ap f p) = ap (ap f) (concat_1p p).A, B: Type
f: A -> B
a, b: A
p: a = b
ap_pp f 1 p @ concat_1p (ap f p) =
ap (ap f) (concat_1p p)
Proof.A, B: Type
f: A -> B
a, b: A
p: a = b
ap_pp f 1 p @ concat_1p (ap f p) =
ap (ap f) (concat_1p p)
  destruct p; reflexivity.
Defined.

Lemma ap_pp_concat_pV {A B} (f : A -> B) {x y : A} (p : x = y)
: ap_pp f p p^ @ ((1 @@ ap_V f p) @ concat_pV (ap f p))
  = ap (ap f) (concat_pV p).A, B: Type
f: A -> B
x, y: A
p: x = y
ap_pp f p p^ @ ((1 @@ ap_V f p) @ concat_pV (ap f p)) =
ap (ap f) (concat_pV p)
Proof.A, B: Type
f: A -> B
x, y: A
p: x = y
ap_pp f p p^ @ ((1 @@ ap_V f p) @ concat_pV (ap f p)) =
ap (ap f) (concat_pV p)
  destruct p; reflexivity.
Defined.

Lemma ap_pp_concat_Vp {A B} (f : A -> B) {x y : A} (p : x = y)
: ap_pp f p^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p))
  = ap (ap f) (concat_Vp p).A, B: Type
f: A -> B
x, y: A
p: x = y
ap_pp f p^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p)) =
ap (ap f) (concat_Vp p)
Proof.A, B: Type
f: A -> B
x, y: A
p: x = y
ap_pp f p^ p @ ((ap_V f p @@ 1) @ concat_Vp (ap f p)) =
ap (ap f) (concat_Vp p)
  destruct p; reflexivity.
Defined.

Lemma concat_pV_inverse2 {A} {x y : A} (p q : x = y) (r : p = q)
: (r @@ inverse2 r) @ concat_pV q = concat_pV p.A: Type
x, y: A
p, q: x = y
r: p = q
(r @@ inverse2 r) @ concat_pV q = concat_pV p
Proof.A: Type
x, y: A
p, q: x = y
r: p = q
(r @@ inverse2 r) @ concat_pV q = concat_pV p
  destruct r, p; reflexivity.
Defined.

Lemma concat_Vp_inverse2 {A} {x y : A} (p q : x = y) (r : p = q)
: (inverse2 r @@ r) @ concat_Vp q = concat_Vp p.A: Type
x, y: A
p, q: x = y
r: p = q
(inverse2 r @@ r) @ concat_Vp q = concat_Vp p
Proof.A: Type
x, y: A
p, q: x = y
r: p = q
(inverse2 r @@ r) @ concat_Vp q = concat_Vp p
  destruct r, p; reflexivity.
Defined.

(** *** Whiskering *)

Definition whiskerL {A : Type} {x y z : A} (p : x = y)
  {q r : y = z} (h : q = r) : p @ q = p @ r
:= 1 @@ h.

Definition whiskerR {A : Type} {x y z : A} {p q : x = y}
  (h : p = q) (r : y = z) : p @ r = q @ r
:= h @@ 1.

(** *** Unwhiskering, a.k.a. cancelling. *)

Definition cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
: (p @ q = p @ r) -> (q = r)
:= fun h => (concat_V_pp p q)^ @ whiskerL p^ h @ (concat_V_pp p r).

Definition cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
: (p @ r = q @ r) -> (p = q)
:= fun h => (concat_pp_V p r)^ @ whiskerR h r^ @ (concat_pp_V q r).

(** Whiskering and identity paths. *)

Definition whiskerR_p1 {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  (concat_p1 p)^ @ whiskerR h 1 @ concat_p1 q = h
  :=
  match h with idpath =>
    match p with idpath =>
      1
    end end.

Definition whiskerR_1p {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  whiskerR 1 q = 1 :> (p @ q = p @ q)
  :=
  match q with idpath => 1 end.

Definition whiskerL_p1 {A : Type} {x y z : A} (p : x = y) (q : y = z) :
  whiskerL p 1 = 1 :> (p @ q = p @ q)
  :=
  match q with idpath => 1 end.

Definition whiskerL_1p {A : Type} {x y : A} {p q : x = y} (h : p = q) :
  (concat_1p p) ^ @ whiskerL 1 h @ concat_1p q = h
  :=
  match h with idpath =>
    match p with idpath =>
      1
    end end.

Definition whiskerR_p1_1 {A} {x : A} (h : idpath x = idpath x)
: whiskerR h 1 = h.A: Type
x: A
h: 1 = 1
whiskerR h 1 = h
Proof.A: Type
x: A
h: 1 = 1
whiskerR h 1 = h
  refine (_ @ whiskerR_p1 h); simpl.A: Type
x: A
h: 1 = 1
whiskerR h 1 = (1 @ whiskerR h 1) @ 1
  symmetry; refine (concat_p1 _ @ concat_1p _).
Defined.

Definition whiskerL_1p_1 {A} {x : A} (h : idpath x = idpath x)
: whiskerL 1 h = h.A: Type
x: A
h: 1 = 1
whiskerL 1 h = h
Proof.A: Type
x: A
h: 1 = 1
whiskerL 1 h = h
  refine (_ @ whiskerL_1p h); simpl.A: Type
x: A
h: 1 = 1
whiskerL 1 h = (1 @ whiskerL 1 h) @ 1
  symmetry; refine (concat_p1 _ @ concat_1p _).
Defined.

Definition cancel2L {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
           (g : p = p') (h k : q = q')
: (g @@ h = g @@ k) -> (h = k).A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g: p = p'
h, k: q = q'
g @@ h = g @@ k -> h = k
Proof.A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g: p = p'
h, k: q = q'
g @@ h = g @@ k -> h = k
  intro r.A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g: p = p'
h, k: q = q'
r: g @@ h = g @@ k
h = k induction g, p, q.A: Type
x: A
q': x = x
h, k: 1 = q'
r: 1 @@ h = 1 @@ k
h = k
  refine ((whiskerL_1p h)^ @ _).A: Type
x: A
q': x = x
h, k: 1 = q'
r: 1 @@ h = 1 @@ k
((concat_1p 1)^ @ whiskerL 1 h) @ concat_1p q' = k refine (_ @ (whiskerL_1p k)).A: Type
x: A
q': x = x
h, k: 1 = q'
r: 1 @@ h = 1 @@ k
((concat_1p 1)^ @ whiskerL 1 h) @ concat_1p q' =
((concat_1p 1)^ @ whiskerL 1 k) @ concat_1p q'
  refine (whiskerR _ _).A: Type
x: A
q': x = x
h, k: 1 = q'
r: 1 @@ h = 1 @@ k
(concat_1p 1)^ @ whiskerL 1 h =
(concat_1p 1)^ @ whiskerL 1 k refine (whiskerL _ _).A: Type
x: A
q': x = x
h, k: 1 = q'
r: 1 @@ h = 1 @@ k
whiskerL 1 h = whiskerL 1 k
  apply r.
Defined.

Definition cancel2R {A : Type} {x y z : A} {p p' : x = y} {q q' : y = z}
           (g h : p = p') (k : q = q')
: (g @@ k = h @@ k) -> (g = h).A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g, h: p = p'
k: q = q'
g @@ k = h @@ k -> g = h
Proof.A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g, h: p = p'
k: q = q'
g @@ k = h @@ k -> g = h
  intro r.A: Type
x, y, z: A
p, p': x = y
q, q': y = z
g, h: p = p'
k: q = q'
r: g @@ k = h @@ k
g = h induction k, p, q.A: Type
x: A
p': x = x
g, h: 1 = p'
r: g @@ 1 = h @@ 1
g = h
  refine ((whiskerR_p1 g)^ @ _).A: Type
x: A
p': x = x
g, h: 1 = p'
r: g @@ 1 = h @@ 1
((concat_p1 1)^ @ whiskerR g 1) @ concat_p1 p' = h refine (_ @ (whiskerR_p1 h)).A: Type
x: A
p': x = x
g, h: 1 = p'
r: g @@ 1 = h @@ 1
((concat_p1 1)^ @ whiskerR g 1) @ concat_p1 p' =
((concat_p1 1)^ @ whiskerR h 1) @ concat_p1 p'
  refine (whiskerR _ _).A: Type
x: A
p': x = x
g, h: 1 = p'
r: g @@ 1 = h @@ 1
(concat_p1 1)^ @ whiskerR g 1 =
(concat_p1 1)^ @ whiskerR h 1 refine (whiskerL _ _).A: Type
x: A
p': x = x
g, h: 1 = p'
r: g @@ 1 = h @@ 1
whiskerR g 1 = whiskerR h 1
  apply r.
Defined.


(** Whiskering and composition *)

(* The naming scheme for these is a little unclear; should [pp] refer to concatenation of the 2-paths being whiskered or of the paths we are whiskering by? *)
Definition whiskerL_pp {A} {x y z : A} (p : x = y) {q q' q'' : y = z}
           (r : q = q') (s : q' = q'')
: whiskerL p (r @ s) = whiskerL p r @ whiskerL p s.A: Type
x, y, z: A
p: x = y
q, q', q'': y = z
r: q = q'
s: q' = q''
whiskerL p (r @ s) = whiskerL p r @ whiskerL p s
Proof.A: Type
x, y, z: A
p: x = y
q, q', q'': y = z
r: q = q'
s: q' = q''
whiskerL p (r @ s) = whiskerL p r @ whiskerL p s
  destruct p, r, s; reflexivity.
Defined.

Definition whiskerR_pp {A} {x y z : A} {p p' p'' : x = y} (q : y = z)
           (r : p = p') (s : p' = p'')
: whiskerR (r @ s) q = whiskerR r q @ whiskerR s q.A: Type
x, y, z: A
p, p', p'': x = y
q: y = z
r: p = p'
s: p' = p''
whiskerR (r @ s) q = whiskerR r q @ whiskerR s q
Proof.A: Type
x, y, z: A
p, p', p'': x = y
q: y = z
r: p = p'
s: p' = p''
whiskerR (r @ s) q = whiskerR r q @ whiskerR s q
  destruct q, r, s; reflexivity.
Defined.

(* For now, I've put an [L] or [R] to mark when we're referring to the whiskering paths. *)
Definition whiskerL_VpL {A} {x y z : A} (p : x = y)
           {q q' : y = z} (r : q = q')
: (concat_V_pp p q)^ @ whiskerL p^ (whiskerL p r) @ concat_V_pp p q'
  = r.A: Type
x, y, z: A
p: x = y
q, q': y = z
r: q = q'
((concat_V_pp p q)^ @ whiskerL p^ (whiskerL p r)) @
concat_V_pp p q' = r
Proof.A: Type
x, y, z: A
p: x = y
q, q': y = z
r: q = q'
((concat_V_pp p q)^ @ whiskerL p^ (whiskerL p r)) @
concat_V_pp p q' = r
  destruct p, r, q.A: Type
x: A
((concat_V_pp 1 1)^ @ whiskerL 1^ (whiskerL 1 1)) @
concat_V_pp 1 1 = 1 reflexivity.
Defined.

Definition whiskerL_pVL {A} {x y z : A} (p : y = x)
           {q q' : y = z} (r : q = q')
: (concat_p_Vp p q)^ @ whiskerL p (whiskerL p^ r) @ concat_p_Vp p q'
  = r.A: Type
x, y, z: A
p: y = x
q, q': y = z
r: q = q'
((concat_p_Vp p q)^ @ whiskerL p (whiskerL p^ r)) @
concat_p_Vp p q' = r
Proof.A: Type
x, y, z: A
p: y = x
q, q': y = z
r: q = q'
((concat_p_Vp p q)^ @ whiskerL p (whiskerL p^ r)) @
concat_p_Vp p q' = r
  destruct p, r, q.A: Type
y: A
((concat_p_Vp 1 1)^ @ whiskerL 1 (whiskerL 1^ 1)) @
concat_p_Vp 1 1 = 1 reflexivity.
Defined.

Definition whiskerR_pVR {A} {x y z : A} {p p' : x = y}
           (r : p = p') (q : y = z)
: (concat_pp_V p q)^ @ whiskerR (whiskerR r q) q^ @ concat_pp_V p' q
  = r.A: Type
x, y, z: A
p, p': x = y
r: p = p'
q: y = z
((concat_pp_V p q)^ @ whiskerR (whiskerR r q) q^) @
concat_pp_V p' q = r
Proof.A: Type
x, y, z: A
p, p': x = y
r: p = p'
q: y = z
((concat_pp_V p q)^ @ whiskerR (whiskerR r q) q^) @
concat_pp_V p' q = r
  destruct p, r, q.A: Type
x: A
((concat_pp_V 1 1)^ @ whiskerR (whiskerR 1 1) 1^) @
concat_pp_V 1 1 = 1 reflexivity.
Defined.

Definition whiskerR_VpR {A} {x y z : A} {p p' : x = y}
           (r : p = p') (q : z = y)
: (concat_pV_p p q)^ @ whiskerR (whiskerR r q^) q @ concat_pV_p p' q
  = r.A: Type
x, y, z: A
p, p': x = y
r: p = p'
q: z = y
((concat_pV_p p q)^ @ whiskerR (whiskerR r q^) q) @
concat_pV_p p' q = r
Proof.A: Type
x, y, z: A
p, p': x = y
r: p = p'
q: z = y
((concat_pV_p p q)^ @ whiskerR (whiskerR r q^) q) @
concat_pV_p p' q = r
  destruct p, r, q.A: Type
z: A
((concat_pV_p 1 1)^ @ whiskerR (whiskerR 1 1^) 1) @
concat_pV_p 1 1 = 1 reflexivity.
Defined.

(** Naturality of [concat_p_pp] in left-most argument. *)
Definition concat_p_pp_nat_l {A} {w x y z : A}
  {p p' : w = x} (h : p = p') (q : x = y) (r : y = z)
  : whiskerR h (q @ r) @ concat_p_pp p' q r
    = concat_p_pp p q r @ whiskerR (whiskerR h q) r.A: Type
w, x, y, z: A
p, p': w = x
h: p = p'
q: x = y
r: y = z
whiskerR h (q @ r) @ concat_p_pp p' q r =
concat_p_pp p q r @ whiskerR (whiskerR h q) r
Proof.A: Type
w, x, y, z: A
p, p': w = x
h: p = p'
q: x = y
r: y = z
whiskerR h (q @ r) @ concat_p_pp p' q r =
concat_p_pp p q r @ whiskerR (whiskerR h q) r
  by destruct h, p, q, r.
Defined.

(** Naturality of [concat_p_pp] in middle argument. *)
Definition concat_p_pp_nat_m {A} {w x y z : A}
  (p : w = x) {q q' : x = y} (h : q = q') (r : y = z)
  : whiskerL p (whiskerR h r) @ concat_p_pp p q' r
    = concat_p_pp p q r @ whiskerR (whiskerL p h) r.A: Type
w, x, y, z: A
p: w = x
q, q': x = y
h: q = q'
r: y = z
whiskerL p (whiskerR h r) @ concat_p_pp p q' r =
concat_p_pp p q r @ whiskerR (whiskerL p h) r
Proof.A: Type
w, x, y, z: A
p: w = x
q, q': x = y
h: q = q'
r: y = z
whiskerL p (whiskerR h r) @ concat_p_pp p q' r =
concat_p_pp p q r @ whiskerR (whiskerL p h) r
  by destruct h, p, q, r.
Defined.

(** Naturality of [concat_p_pp] in right-most argument. *)
Definition concat_p_pp_nat_r {A} {w x y z : A}
  (p : w = x) (q : x = y) {r r' : y = z} (h : r = r')
  : whiskerL p (whiskerL q h) @ concat_p_pp p q r'
    = concat_p_pp p q r @ whiskerL (p @ q) h.A: Type
w, x, y, z: A
p: w = x
q: x = y
r, r': y = z
h: r = r'
whiskerL p (whiskerL q h) @ concat_p_pp p q r' =
concat_p_pp p q r @ whiskerL (p @ q) h
Proof.A: Type
w, x, y, z: A
p: w = x
q: x = y
r, r': y = z
h: r = r'
whiskerL p (whiskerL q h) @ concat_p_pp p q r' =
concat_p_pp p q r @ whiskerL (p @ q) h
  by destruct h, p, q, r.
Defined.

(** The interchange law for concatenation. *)
Definition concat_concat2 {A : Type} {x y z : A} {p p' p'' : x = y} {q q' q'' : y = z}
  (a : p = p') (b : p' = p'') (c : q = q') (d : q' = q'') :
  (a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d).A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d)
Proof.A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(a @@ c) @ (b @@ d) = (a @ b) @@ (c @ d)
  case d.A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(a @@ c) @ (b @@ 1) = (a @ b) @@ (c @ 1)
  case c.A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(a @@ 1) @ (b @@ 1) = (a @ b) @@ (1 @ 1)
  case b.A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(a @@ 1) @ (1 @@ 1) = (a @ 1) @@ (1 @ 1)
  case a.A: Type
x, y, z: A
p, p', p'': x = y
q, q', q'': y = z
a: p = p'
b: p' = p''
c: q = q'
d: q' = q''
(1 @@ 1) @ (1 @@ 1) = (1 @ 1) @@ (1 @ 1)
  reflexivity.
Defined.

(** The interchange law for whiskering.  Special case of [concat_concat2]. *)
Definition concat_whisker {A} {x y z : A} (p p' : x = y) (q q' : y = z) (a : p = p') (b : q = q') :
  (whiskerR a q) @ (whiskerL p' b) = (whiskerL p b) @ (whiskerR a q')
  :=
  match b with
    idpath =>
    match a with idpath =>
      (concat_1p _)^
    end
  end.

(** Structure corresponding to the coherence equations of a bicategory. *)

(** The "pentagonator": the 3-cell witnessing the associativity pentagon. *)
Definition pentagon {A : Type} {v w x y z : A} (p : v = w) (q : w = x) (r : x = y) (s : y = z)
  : whiskerL p (concat_p_pp q r s)
      @ concat_p_pp p (q@r) s
      @ whiskerR (concat_p_pp p q r) s
  = concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s.A: Type
v, w, x, y, z: A
p: v = w
q: w = x
r: x = y
s: y = z
(whiskerL p (concat_p_pp q r s) @
 concat_p_pp p (q @ r) s) @
whiskerR (concat_p_pp p q r) s =
concat_p_pp p q (r @ s) @ concat_p_pp (p @ q) r s
Proof.A: Type
v, w, x, y, z: A
p: v = w
q: w = x
r: x = y
s: y = z
(whiskerL p (concat_p_pp q r s) @
 concat_p_pp p (q @ r) s) @
whiskerR (concat_p_pp p q r) s =
concat_p_pp p q (r @ s) @ concat_p_pp (p @ q) r s
  case p, q, r, s.A: Type
v: A
(whiskerL 1 (concat_p_pp 1 1 1) @
 concat_p_pp 1 (1 @ 1) 1) @
whiskerR (concat_p_pp 1 1 1) 1 =
concat_p_pp 1 1 (1 @ 1) @ concat_p_pp (1 @ 1) 1 1  reflexivity.
Defined.

(** The 3-cell witnessing the left unit triangle. *)
Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
  : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q
  = whiskerL p (concat_1p q).A: Type
x, y, z: A
p: x = y
q: y = z
concat_p_pp p 1 q @ whiskerR (concat_p1 p) q =
whiskerL p (concat_1p q)
Proof.A: Type
x, y, z: A
p: x = y
q: y = z
concat_p_pp p 1 q @ whiskerR (concat_p1 p) q =
whiskerL p (concat_1p q)
  case p, q.A: Type
x: A
concat_p_pp 1 1 1 @ whiskerR (concat_p1 1) 1 =
whiskerL 1 (concat_1p 1)  reflexivity.
Defined.

(** The Eckmann-Hilton argument *)
Definition eckmann_hilton {A : Type} {x:A} (p q : 1 = 1 :> (x = x)) : p @ q = q @ p :=
  (whiskerR_p1 p @@ whiskerL_1p q)^
  @ (concat_p1 _ @@ concat_p1 _)
  @ (concat_1p _ @@ concat_1p _)
  @ (concat_whisker _ _ _ _ p q)
  @ (concat_1p _ @@ concat_1p _)^
  @ (concat_p1 _ @@ concat_p1 _)^
  @ (whiskerL_1p q @@ whiskerR_p1 p).

(** The action of functions on 2-dimensional paths *)

Definition ap02 {A B : Type} (f:A->B) {x y:A} {p q:x=y} (r:p=q) : ap f p = ap f q
  := ap (ap f) r.

Definition ap02_pp {A B} (f:A->B) {x y:A} {p p' p'':x=y} (r:p=p') (r':p'=p'')
  : ap02 f (r @ r') = ap02 f r @ ap02 f r'
  := ap_pp (ap f) r r'.

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')
  : ap02 f (r @@ s) = ap_pp f p q
                      @ (ap02 f r @@ ap02 f s)
                      @ (ap_pp f p' q')^.A, B: Type
f: A -> B
x, y, z: A
p, p': x = y
q, q': y = z
r: p = p'
s: q = q'
ap02 f (r @@ s) =
(ap_pp f p q @ (ap02 f r @@ ap02 f s)) @
(ap_pp f p' q')^
Proof.A, B: Type
f: A -> B
x, y, z: A
p, p': x = y
q, q': y = z
r: p = p'
s: q = q'
ap02 f (r @@ s) =
(ap_pp f p q @ (ap02 f r @@ ap02 f s)) @
(ap_pp f p' q')^
  case r, s, p, q.A, B: Type
f: A -> B
x: A
ap02 f (1 @@ 1) =
(ap_pp f 1 1 @ (ap02 f 1 @@ ap02 f 1)) @
(ap_pp f 1 1)^ reflexivity.
Defined.

Definition apD02 {A : Type} {B : A -> Type} {x y : A} {p q : x = y}
  (f : forall x, B x) (r : p = q)
  : apD f p = transport2 B r (f x) @ apD f q
  := match r with idpath => (concat_1p _)^ end.

Definition apD02_const {A B : Type} (f : A -> B) {x y : A} {p q : x = y} (r : p = q)
  : apD02 f r = (apD_const f p)
                  @ (transport2_const r (f x) @@ ap02 f r)
                  @ (concat_p_pp _ _ _)^
                  @ (whiskerL (transport2 _ r (f x)) (apD_const f q)^)
  := match r with idpath =>
    match p with idpath => 1
    end end.

(* And now for a lemma whose statement is much longer than its proof. *)
Definition apD02_pp {A} (B : A -> Type) (f : forall x:A, B x) {x y : A}
  {p1 p2 p3 : x = y} (r1 : p1 = p2) (r2 : p2 = p3)
  : apD02 f (r1 @ r2)
  = apD02 f r1
  @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
  @ concat_p_pp _ _ _
  @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)).A: Type
B: A -> Type
f: forall x : A, B x
x, y: A
p1, p2, p3: x = y
r1: p1 = p2
r2: p2 = p3
apD02 f (r1 @ r2) =
((apD02 f r1 @
  whiskerL (transport2 B r1 (f x)) (apD02 f r2)) @
 concat_p_pp (transport2 B r1 (f x))
   (transport2 B r2 (f x)) (apD f p3)) @
whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)
Proof.A: Type
B: A -> Type
f: forall x : A, B x
x, y: A
p1, p2, p3: x = y
r1: p1 = p2
r2: p2 = p3
apD02 f (r1 @ r2) =
((apD02 f r1 @
  whiskerL (transport2 B r1 (f x)) (apD02 f r2)) @
 concat_p_pp (transport2 B r1 (f x))
   (transport2 B r2 (f x)) (apD f p3)) @
whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)
  destruct r1, r2.A: Type
B: A -> Type
f: forall x : A, B x
x, y: A
p1: x = y
apD02 f (1 @ 1) =
((apD02 f 1 @
  whiskerL (transport2 B 1 (f x)) (apD02 f 1)) @
 concat_p_pp (transport2 B 1 (f x))
   (transport2 B 1 (f x)) (apD f p1)) @
whiskerR (transport2_p2p B 1 1 (f x))^ (apD f p1) destruct p1.A: Type
B: A -> Type
f: forall x : A, B x
x: A
apD02 f (1 @ 1) =
((apD02 f 1 @
  whiskerL (transport2 B 1 (f x)) (apD02 f 1)) @
 concat_p_pp (transport2 B 1 (f x))
   (transport2 B 1 (f x)) (apD f 1)) @
whiskerR (transport2_p2p B 1 1 (f x))^ (apD f 1) reflexivity.
Defined.

Definition ap022 {A B C} (f : A -> B -> C) {x x' y y'}
  {p p' : x = x'} (r : p = p') {q q' : y = y'} (s : q = q')
  : ap011 f p q = ap011 f p' q'.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p, p': x = x'
r: p = p'
q, q': y = y'
s: q = q'
ap011 f p q = ap011 f p' q'
Proof.A, B, C: Type
f: A -> B -> C
x, x': A
y, y': B
p, p': x = x'
r: p = p'
q, q': y = y'
s: q = q'
ap011 f p q = ap011 f p' q'
  destruct r, p.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q, q': y = y'
s: q = q'
ap011 f 1 q = ap011 f 1 q'
  apply ap02.A, B, C: Type
f: A -> B -> C
x: A
y, y': B
q, q': y = y'
s: q = q'
q = q'
  exact s.
Defined.

(** These lemmas need better names. *)
Definition ap_transport_Vp_idmap {A B} (p q : A = B) (r : q = p) (z : A)
: ap (transport idmap q^) (ap (fun s => transport idmap s z) r)
  @ ap (fun s => transport idmap s (p # z)) (inverse2 r)
  @ transport_Vp idmap p z
  = transport_Vp idmap q z.A, B: Type
p, q: A = B
r: q = p
z: A
(ap (transport idmap q^)
   (ap (fun s : A = B => transport idmap s z) r) @
 ap
   (fun s : B = A =>
    transport idmap s (transport idmap p z))
   (inverse2 r)) @ transport_Vp idmap p z =
transport_Vp idmap q z
Proof.A, B: Type
p, q: A = B
r: q = p
z: A
(ap (transport idmap q^)
   (ap (fun s : A = B => transport idmap s z) r) @
 ap
   (fun s : B = A =>
    transport idmap s (transport idmap p z))
   (inverse2 r)) @ transport_Vp idmap p z =
transport_Vp idmap q z
  by path_induction.
Defined.

Definition ap_transport_pV_idmap {A B} (p q : A = B) (r : q = p) (z : B)
: ap (transport idmap q) (ap (fun s => transport idmap s^ z) r)
  @ ap (fun s => transport idmap s (p^ # z)) r
  @ transport_pV idmap p z
  = transport_pV idmap q z.A, B: Type
p, q: A = B
r: q = p
z: B
(ap (transport idmap q)
   (ap (fun s : A = B => transport idmap s^ z) r) @
 ap
   (fun s : A = B =>
    transport idmap s (transport idmap p^ z)) r) @
transport_pV idmap p z = transport_pV idmap q z
Proof.A, B: Type
p, q: A = B
r: q = p
z: B
(ap (transport idmap q)
   (ap (fun s : A = B => transport idmap s^ z) r) @
 ap
   (fun s : A = B =>
    transport idmap s (transport idmap p^ z)) r) @
transport_pV idmap p z = transport_pV idmap q z
  by path_induction.
Defined.

(** ** Tactics, hints, and aliases *)

(** [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. *)
Notation concatR := (fun p q => concat q p).

#[export]
Hint Resolve
  concat_1p concat_p1 concat_p_pp
  inv_pp inv_V
 : path_hints.

(* First try at a paths db
We want the RHS of the equation to become strictly simpler *)
#[export]
Hint Rewrite
@concat_p1
@concat_1p
@concat_p_pp (* there is a choice here !*)
@concat_pV
@concat_Vp
@concat_V_pp
@concat_p_Vp
@concat_pp_V
@concat_pV_p
(*@inv_pp*) (* I am not sure about this one *)
@inv_V
@moveR_Mp
@moveR_pM
@moveL_Mp
@moveL_pM
@moveL_1M
@moveL_M1
@moveR_M1
@moveR_1M
@ap_1
(* @ap_pp
@ap_p_pp ?*)
@inverse_ap
@ap_idmap
(* @ap_compose
@ap_compose'*)
@ap_const
(* Unsure about naturality of [ap], was absent in the old implementation*)
@apD10_1
:paths.

Ltac hott_simpl :=
  autorewrite with paths in * |- * ; auto with path_hints.