(* -*- mode: coq; mode: visual-line -*- *)
(** * Theorems about path spaces *)

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

Local Open Scope path_scope.

Generalizable Variables A B f x y z.

(** ** Path spaces *)

(** The path spaces of a path space are not, of course, determined; they are just the
    higher-dimensional structure of the original space. *)

(** ** Transporting in path spaces.

   There are potentially a lot of these lemmas, so we adopt a uniform naming scheme:

   - `l` means the left endpoint varies
   - `r` means the right endpoint varies
   - `F` means application of a function to that (varying) endpoint.
*)

Definition transport_paths_l {A : Type} {x1 x2 y : A} (p : x1 = x2) (q : x1 = y)
  : transport (fun x => x = y) p q = p^ @ q.
A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
transport (fun x : A => x = y) p q = p^ @ q
Proof.
A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
transport (fun x : A => x = y) p q = p^ @ q
  destruct p, q; reflexivity.
Defined.

Definition transport_paths_r {A : Type} {x y1 y2 : A} (p : y1 = y2) (q : x = y1)
  : transport (fun y => x = y) p q = q @ p.
A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
transport (fun y : A => x = y) p q = q @ p
Proof.
A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
transport (fun y : A => x = y) p q = q @ p
  destruct p, q; reflexivity.
Defined.

Definition transport_paths_lr {A : Type} {x1 x2 : A} (p : x1 = x2) (q : x1 = x1)
  : transport (fun x => x = x) p q = p^ @ q @ p.
A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
transport (fun x : A => x = x) p q = (p^ @ q) @ p
Proof.
A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
transport (fun x : A => x = x) p q = (p^ @ q) @ p
  destruct p; simpl.
A: Type
x1: A
q: x1 = x1
q = (1 @ q) @ 1
  exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.

Definition transport_paths_Fl {A B : Type} {f : A -> B} {x1 x2 : A} {y : B}
  (p : x1 = x2) (q : f x1 = y)
  : transport (fun x => f x = y) p q = (ap f p)^ @ q.
A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
transport (fun x : A => f x = y) p q = (ap f p)^ @ q
Proof.
A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
transport (fun x : A => f x = y) p q = (ap f p)^ @ q
  destruct p, q; reflexivity.
Defined.

Definition transport_paths_Fr {A B : Type} {g : A -> B} {y1 y2 : A} {x : B}
  (p : y1 = y2) (q : x = g y1)
  : transport (fun y => x = g y) p q = q @ (ap g p).
A, B: Type
g: A -> B
y1, y2: A
x: B
p: y1 = y2
q: x = g y1
transport (fun y : A => x = g y) p q = q @ ap g p
Proof.
A, B: Type
g: A -> B
y1, y2: A
x: B
p: y1 = y2
q: x = g y1
transport (fun y : A => x = g y) p q = q @ ap g p
  destruct p.
A, B: Type
g: A -> B
y1: A
x: B
q: x = g y1
transport (fun y : A => x = g y) 1 q = q @ ap g 1 symmetry; apply concat_p1.
Defined.

Definition transport_paths_FlFr {A B : Type} {f g : A -> B} {x1 x2 : A}
  (p : x1 = x2) (q : f x1 = g x1)
  : transport (fun x => f x = g x) p q = (ap f p)^ @ q @ (ap g p).
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
transport (fun x : A => f x = g x) p q =
((ap f p)^ @ q) @ ap g p
Proof.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
transport (fun x : A => f x = g x) p q =
((ap f p)^ @ q) @ ap g p
  destruct p; simpl.
A, B: Type
f, g: A -> B
x1: A
q: f x1 = g x1
q = (1 @ q) @ 1
  exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.

Definition transport_paths_FlFr_D {A : Type} {B : A -> Type}
  {f g : forall a, B a} {x1 x2 : A} (p : x1 = x2) (q : f x1 = g x1)
: transport (fun x => f x = g x) p q
  = (apD f p)^ @ ap (transport B p) q @ (apD g p).
A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q: f x1 = g x1
transport (fun x : A => f x = g x) p q =
((apD f p)^ @ ap (transport B p) q) @ apD g p
Proof.
A: Type
B: A -> Type
f, g: forall a : A, B a
x1, x2: A
p: x1 = x2
q: f x1 = g x1
transport (fun x : A => f x = g x) p q =
((apD f p)^ @ ap (transport B p) q) @ apD g p
  destruct p; simpl.
A: Type
B: A -> Type
f, g: forall a : A, B a
x1: A
q: f x1 = g x1
q = (1 @ ap (transport B 1) q) @ 1
  exact ((ap_idmap _)^ @ (concat_1p _)^ @ (concat_p1 _)^).
Defined.

Definition transport_paths_FFlr {A B : Type} {f : A -> B} {g : B -> A} {x1 x2 : A}
  (p : x1 = x2) (q : g (f x1) = x1)
  : transport (fun x => g (f x) = x) p q = (ap g (ap f p))^ @ q @ p.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
transport (fun x : A => g (f x) = x) p q =
((ap g (ap f p))^ @ q) @ p
Proof.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
transport (fun x : A => g (f x) = x) p q =
((ap g (ap f p))^ @ q) @ p
  destruct p; simpl.
A, B: Type
f: A -> B
g: B -> A
x1: A
q: g (f x1) = x1
q = (1 @ q) @ 1
  exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.

Definition transport_paths_lFFr {A B : Type} {f : A -> B} {g : B -> A} {x1 x2 : A}
  (p : x1 = x2) (q : x1 = g (f x1))
  : transport (fun x => x = g (f x)) p q = p^ @ q @ (ap g (ap f p)).
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
transport (fun x : A => x = g (f x)) p q =
(p^ @ q) @ ap g (ap f p)
Proof.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
transport (fun x : A => x = g (f x)) p q =
(p^ @ q) @ ap g (ap f p)
  destruct p; simpl.
A, B: Type
f: A -> B
g: B -> A
x1: A
q: x1 = g (f x1)
q = (1 @ q) @ 1
  exact ((concat_1p q)^ @ (concat_p1 (1 @ q))^).
Defined.

(** Variants of the above that do the most common rearranging. We could add similar variants for the others as needed. *)
Definition transport_paths_FlFr' {A B : Type} {f g : A -> B} {x1 x2 : A}
  (p : x1 = x2) (q : f x1 = g x1) (r : (f x2) = (g x2))
  (h : (ap f p) @ r = q @ (ap g p))
  : transport (fun x => f x = g x) p q = r.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
h: ap f p @ r = q @ ap g p
transport (fun x : A => f x = g x) p q = r
Proof.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
h: ap f p @ r = q @ ap g p
transport (fun x : A => f x = g x) p q = r
  refine (transport_paths_FlFr _ _ @ _).
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
h: ap f p @ r = q @ ap g p
((ap f p)^ @ q) @ ap g p = r
  refine (concat_pp_p _ _ _ @ _).
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
h: ap f p @ r = q @ ap g p
(ap f p)^ @ (q @ ap g p) = r
  apply moveR_Vp.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
h: ap f p @ r = q @ ap g p
q @ ap g p = ap f p @ r
  exact h^.
Defined.

Definition transport_paths_FFlr' {A B : Type} {f : A -> B} {g : B -> A} {x1 x2 : A}
  (p : x1 = x2) (q : g (f x1) = x1) (r : g (f x2) = x2)
  (h : (ap g (ap f p)) @ r = q @ p)
  : transport (fun x => g (f x) = x) p q = r.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
h: ap g (ap f p) @ r = q @ p
transport (fun x : A => g (f x) = x) p q = r
Proof.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
h: ap g (ap f p) @ r = q @ p
transport (fun x : A => g (f x) = x) p q = r
  refine (transport_paths_FFlr _ _ @ _).
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
h: ap g (ap f p) @ r = q @ p
((ap g (ap f p))^ @ q) @ p = r
  refine (concat_pp_p _ _ _ @ _).
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
h: ap g (ap f p) @ r = q @ p
(ap g (ap f p))^ @ (q @ p) = r
  apply moveR_Vp.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
h: ap g (ap f p) @ r = q @ p
q @ p = ap g (ap f p) @ r
  exact h^.
Defined.

Definition transport011_paths {A B X} (f : A -> X) (g : B -> X)
  {a1 a2 : A} {b1 b2 : B} (p : a1 = a2) (q : b1 = b2)
  (r : f a1 = g b1)
  : transport011 (fun a b => f a = g b) p q r = (ap f p)^ @ r @ ap g q.
A, B, X: Type
f: A -> X
g: B -> X
a1, a2: A
b1, b2: B
p: a1 = a2
q: b1 = b2
r: f a1 = g b1
transport011 (fun (a : A) (b : B) => f a = g b) p q r =
((ap f p)^ @ r) @ ap g q
Proof.
A, B, X: Type
f: A -> X
g: B -> X
a1, a2: A
b1, b2: B
p: a1 = a2
q: b1 = b2
r: f a1 = g b1
transport011 (fun (a : A) (b : B) => f a = g b) p q r =
((ap f p)^ @ r) @ ap g q
  destruct p, q; cbn.
A, B, X: Type
f: A -> X
g: B -> X
a1: A
b1: B
r: f a1 = g b1
r = (1 @ r) @ 1
  symmetry.
A, B, X: Type
f: A -> X
g: B -> X
a1: A
b1: B
r: f a1 = g b1
(1 @ r) @ 1 = r
  lhs nrapply concat_p1.
A, B, X: Type
f: A -> X
g: B -> X
a1: A
b1: B
r: f a1 = g b1
1 @ r = r
  apply concat_1p.
Defined.

(** ** Transporting in 2-path types *)

Definition transport_paths2 {A : Type} {x y : A}
           (p : x = y) (q : idpath x = idpath x)
: transport (fun a => idpath a = idpath a) p q
  =  (concat_Vp p)^
    @ whiskerL p^ ((concat_1p p)^ @ whiskerR q p @ concat_1p p)
    @ concat_Vp p.
A: Type
x, y: A
p: x = y
q: 1 = 1
transport (fun a : A => 1 = 1) p q =
((concat_Vp p)^ @
 whiskerL p^
   (((concat_1p p)^ @ whiskerR q p) @ concat_1p p)) @
concat_Vp p
Proof.
A: Type
x, y: A
p: x = y
q: 1 = 1
transport (fun a : A => 1 = 1) p q =
((concat_Vp p)^ @
 whiskerL p^
   (((concat_1p p)^ @ whiskerR q p) @ concat_1p p)) @
concat_Vp p
  destruct p.
A: Type
x: A
q: 1 = 1
transport (fun a : A => 1 = 1) 1 q =
((concat_Vp 1)^ @
 whiskerL 1^
   (((concat_1p 1)^ @ whiskerR q 1) @ concat_1p 1)) @
concat_Vp 1 simpl.
A: Type
x: A
q: 1 = 1
q = (1 @ whiskerL 1 ((1 @ whiskerR q 1) @ 1)) @ 1
  refine (_ @ (concat_p1 _)^).
A: Type
x: A
q: 1 = 1
q = 1 @ whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  refine (_ @ (concat_1p _)^).
A: Type
x: A
q: 1 = 1
q = whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  (** The tricky thing here is getting a sufficiently general statement that we can prove it by path induction. *)
  assert (H : forall (p : x = x) (q : 1 = p),
                (q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^
                = whiskerL (idpath x) (idpath 1 @ whiskerR q 1 @ idpath (p @ 1))).
A: Type
x: A
q: 1 = 1
forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
q = whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  {
A: Type
x: A
q: 1 = 1
forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1) intros p' q'.
A: Type
x: A
q: 1 = 1
p': x = x
q': 1 = p'
(q' @ (concat_p1 p')^) @ (concat_1p (p' @ 1))^ =
whiskerL 1 ((1 @ whiskerR q' 1) @ 1) destruct q'.
A: Type
x: A
q: 1 = 1
(1 @ (concat_p1 1)^) @ (concat_1p (1 @ 1))^ =
whiskerL 1 ((1 @ whiskerR 1 1) @ 1) reflexivity. }
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
q = whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  transitivity (q @ (concat_p1 1)^ @ (concat_1p 1)^).
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
q = (q @ (concat_p1 1)^) @ (concat_1p 1)^
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
(q @ (concat_p1 1)^) @ (concat_1p 1)^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  {
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
q = (q @ (concat_p1 1)^) @ (concat_1p 1)^ simpl; exact ((concat_p1 _)^ @ (concat_p1 _)^). }
A: Type
x: A
q: 1 = 1
H: forall (p : x = x) (q : 1 = p),
(q @ (concat_p1 p)^) @ (concat_1p (p @ 1))^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
(q @ (concat_p1 1)^) @ (concat_1p 1)^ =
whiskerL 1 ((1 @ whiskerR q 1) @ 1)
  refine (H 1 q).
Defined.

(** ** Functorial action *)

(** 'functor_path' is called [ap]. *)

(** ** Equivalences between path spaces *)

(** [isequiv_ap] and [equiv_ap] are in Equivalences.v  *)

(** ** Path operations are equivalences *)

Global Instance isequiv_path_inverse {A : Type} (x y : A)
  : IsEquiv (@inverse A x y) | 0.
A: Type
x, y: A
IsEquiv inverse
Proof.
A: Type
x, y: A
IsEquiv inverse
  refine (Build_IsEquiv _ _ _ (@inverse A y x)
                       (@inv_V A y x) (@inv_V A x y) _).
A: Type
x, y: A
forall x0 : x = y, inv_V x0^ = ap inverse (inv_V x0)
  intros p; destruct p; reflexivity.
Defined.

Definition equiv_path_inverse {A : Type} (x y : A)
  : (x = y) <~> (y = x)
  := Build_Equiv _ _ (@inverse A x y) _.

Global Instance isequiv_concat_l {A : Type} `(p : x = y:>A) (z : A)
  : IsEquiv (@transitivity A _ _ x y z p) | 0.
A: Type
x, y: A
p: x = y
z: A
IsEquiv (transitivity p)
Proof.
A: Type
x, y: A
p: x = y
z: A
IsEquiv (transitivity p)
  refine (Build_IsEquiv _ _ _ (concat p^)
                       (concat_p_Vp p) (concat_V_pp p) _).
A: Type
x, y: A
p: x = y
z: A
forall x0 : y = z,
concat_p_Vp p (p @ x0) =
ap (concat p) (concat_V_pp p x0)
  intros q; destruct p; destruct q; reflexivity.
Defined.

Definition equiv_concat_l {A : Type} `(p : x = y) (z : A)
  : (y = z) <~> (x = z)
  := Build_Equiv _ _ (concat p) _.

Global Instance isequiv_concat_r {A : Type} `(p : y = z) (x : A)
  : IsEquiv (fun q:x=y => q @ p) | 0.
A: Type
y, z: A
p: y = z
x: A
IsEquiv (fun q : x = y => q @ p)
Proof.
A: Type
y, z: A
p: y = z
x: A
IsEquiv (fun q : x = y => q @ p)
  refine (Build_IsEquiv _ _ (fun q => q @ p) (fun q => q @ p^)
           (fun q => concat_pV_p q p) (fun q => concat_pp_V q p) _).
A: Type
y, z: A
p: y = z
x: A
forall x0 : x = y,
concat_pV_p (x0 @ p) p =
ap (fun q : x = y => q @ p) (concat_pp_V x0 p)
  intros q; destruct p; destruct q; reflexivity.
Defined.

Definition equiv_concat_r {A : Type} `(p : y = z) (x : A)
  : (x = y) <~> (x = z)
  := Build_Equiv _ _ (fun q => q @ p) _.

Global Instance isequiv_concat_lr {A : Type} {x x' y y' : A} (p : x' = x) (q : y = y')
  : IsEquiv (fun r:x=y => p @ r @ q) | 0
  := @isequiv_compose _ _ (fun r => p @ r) _ _ (fun r => r @ q) _.

Definition equiv_concat_lr {A : Type} {x x' y y' : A} (p : x' = x) (q : y = y')
  : (x = y) <~> (x' = y')
  := Build_Equiv _ _ (fun r:x=y => p @ r @ q) _.

Definition equiv_p1_1q {A : Type} {x y : A} {p q : x = y}
  : p = q <~> p @ 1 = 1 @ q
  := equiv_concat_lr (concat_p1 p) (concat_1p q)^.

Definition equiv_1p_q1 {A : Type} {x y : A} {p q : x = y}
  : p = q <~> 1 @ p = q @ 1
  := equiv_concat_lr (concat_1p p) (concat_p1 q)^.

Global Instance isequiv_whiskerL {A} {x y z : A} (p : x = y) {q r : y = z}
: IsEquiv (@whiskerL A x y z p q r).
A: Type
x, y, z: A
p: x = y
q, r: y = z
IsEquiv (whiskerL p)
Proof.
A: Type
x, y, z: A
p: x = y
q, r: y = z
IsEquiv (whiskerL p)
  simple refine (isequiv_adjointify _ _ _ _).
A: Type
x, y, z: A
p: x = y
q, r: y = z
p @ q = p @ r -> q = r
A: Type
x, y, z: A
p: x = y
q, r: y = z
whiskerL p o ?g == idmap
A: Type
x, y, z: A
p: x = y
q, r: y = z
?g o whiskerL p == idmap
  -
A: Type
x, y, z: A
p: x = y
q, r: y = z
p @ q = p @ r -> q = r apply cancelL.
  -
A: Type
x, y, z: A
p: x = y
q, r: y = z
whiskerL p o cancelL p q r == idmap intros k.
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p (cancelL p q r k) = k unfold cancelL.
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p
  (((concat_V_pp p q)^ @ whiskerL p^ k) @
   concat_V_pp p r) = k
    rewrite !whiskerL_pp.
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
(whiskerL p (concat_V_pp p q)^ @
 whiskerL p (whiskerL p^ k)) @
whiskerL p (concat_V_pp p r) = k
    refine ((_ @@ 1 @@ _) @ whiskerL_pVL p k).
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p (concat_V_pp p q)^ =
(concat_p_Vp p (p @ q))^
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p (concat_V_pp p r) = concat_p_Vp p (p @ r)
    +
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p (concat_V_pp p q)^ =
(concat_p_Vp p (p @ q))^ destruct p, q; reflexivity.
    +
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: p @ q = p @ r
whiskerL p (concat_V_pp p r) = concat_p_Vp p (p @ r) destruct p, r; reflexivity.
  -
A: Type
x, y, z: A
p: x = y
q, r: y = z
cancelL p q r o whiskerL p == idmap intros k.
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
cancelL p q r (whiskerL p k) = k unfold cancelL.
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
((concat_V_pp p q)^ @ whiskerL p^ (whiskerL p k)) @
concat_V_pp p r = k
    refine ((_ @@ 1 @@ _) @ whiskerL_VpL p k).
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
(concat_V_pp p q)^ = (concat_V_pp p q)^
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
concat_V_pp p r = concat_V_pp p r
    +
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
(concat_V_pp p q)^ = (concat_V_pp p q)^ destruct p, q; reflexivity.
    +
A: Type
x, y, z: A
p: x = y
q, r: y = z
k: q = r
concat_V_pp p r = concat_V_pp p r destruct p, r; reflexivity.
Defined.

Definition equiv_whiskerL {A} {x y z : A} (p : x = y) (q r : y = z)
: (q = r) <~> (p @ q = p @ r)
  := Build_Equiv _ _ (whiskerL p) _.

Definition equiv_cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
: (p @ q = p @ r) <~> (q = r)
  := equiv_inverse (equiv_whiskerL p q r).

Definition isequiv_cancelL {A} {x y z : A} (p : x = y) (q r : y = z)
  : IsEquiv (cancelL p q r).
A: Type
x, y, z: A
p: x = y
q, r: y = z
IsEquiv (cancelL p q r)
Proof.
A: Type
x, y, z: A
p: x = y
q, r: y = z
IsEquiv (cancelL p q r)
  change (IsEquiv (equiv_cancelL p q r)); exact _.
Defined.

Global Instance isequiv_whiskerR {A} {x y z : A} {p q : x = y} (r : y = z)
: IsEquiv (fun h => @whiskerR A x y z p q h r).
A: Type
x, y, z: A
p, q: x = y
r: y = z
IsEquiv (fun h : p = q => whiskerR h r)
Proof.
A: Type
x, y, z: A
p, q: x = y
r: y = z
IsEquiv (fun h : p = q => whiskerR h r)
  simple refine (isequiv_adjointify _ _ _ _).
A: Type
x, y, z: A
p, q: x = y
r: y = z
p @ r = q @ r -> p = q
A: Type
x, y, z: A
p, q: x = y
r: y = z
(fun h : p = q => whiskerR h r) o ?g == idmap
A: Type
x, y, z: A
p, q: x = y
r: y = z
?g o (fun h : p = q => whiskerR h r) == idmap
  -
A: Type
x, y, z: A
p, q: x = y
r: y = z
p @ r = q @ r -> p = q apply cancelR.
  -
A: Type
x, y, z: A
p, q: x = y
r: y = z
(fun h : p = q => whiskerR h r) o cancelR p q r ==
idmap intros k.
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR (cancelR p q r k) r = k unfold cancelR.
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR
  (((concat_pp_V p r)^ @ whiskerR k r^) @
   concat_pp_V q r) r = k
    rewrite !whiskerR_pp.
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
(whiskerR (concat_pp_V p r)^ r @
 whiskerR (whiskerR k r^) r) @
whiskerR (concat_pp_V q r) r = k
    refine ((_ @@ 1 @@ _) @ whiskerR_VpR k r).
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR (concat_pp_V p r)^ r =
(concat_pV_p (p @ r) r)^
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR (concat_pp_V q r) r = concat_pV_p (q @ r) r
    +
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR (concat_pp_V p r)^ r =
(concat_pV_p (p @ r) r)^ destruct p, r; reflexivity.
    +
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p @ r = q @ r
whiskerR (concat_pp_V q r) r = concat_pV_p (q @ r) r destruct q, r; reflexivity.
  -
A: Type
x, y, z: A
p, q: x = y
r: y = z
cancelR p q r o (fun h : p = q => whiskerR h r) ==
idmap intros k.
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
cancelR p q r (whiskerR k r) = k unfold cancelR.
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
((concat_pp_V p r)^ @ whiskerR (whiskerR k r) r^) @
concat_pp_V q r = k
    refine ((_ @@ 1 @@ _) @ whiskerR_pVR k r).
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
(concat_pp_V p r)^ = (concat_pp_V p r)^
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
concat_pp_V q r = concat_pp_V q r
    +
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
(concat_pp_V p r)^ = (concat_pp_V p r)^ destruct p, r; reflexivity.
    +
A: Type
x, y, z: A
p, q: x = y
r: y = z
k: p = q
concat_pp_V q r = concat_pp_V q r destruct q, r; reflexivity.
Defined.

Definition equiv_whiskerR {A} {x y z : A} (p q : x = y) (r : y = z)
: (p = q) <~> (p @ r = q @ r)
  := Build_Equiv _ _ (fun h => whiskerR h r) _.

Definition equiv_cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
: (p @ r = q @ r) <~> (p = q)
  := equiv_inverse (equiv_whiskerR p q r).

Definition isequiv_cancelR {A} {x y z : A} (p q : x = y) (r : y = z)
  : IsEquiv (cancelR p q r).
A: Type
x, y, z: A
p, q: x = y
r: y = z
IsEquiv (cancelR p q r)
Proof.
A: Type
x, y, z: A
p, q: x = y
r: y = z
IsEquiv (cancelR p q r)
  change (IsEquiv (equiv_cancelR p q r)); exact _.
Defined.

(** We can use these to build up more complicated equivalences.

In particular, all of the [move] family are equivalences.

(Note: currently, some but not all of these [isequiv_] lemmas have corresponding [equiv_] lemmas.  Also, they do *not* currently contain the computational content that e.g. the inverse of [moveR_Mp] is [moveL_Vp]; perhaps it would be useful if they did? *)

Global Instance isequiv_moveR_Mp
 {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: IsEquiv (moveR_Mp p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveR_Mp p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveR_Mp p q r)
  destruct r.
A: Type
y, z: A
p, q: y = z
IsEquiv (moveR_Mp p q 1)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveR_Mp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: (p = r^ @ q) <~> (r @ p = q)
:= Build_Equiv _ _ (moveR_Mp p q r) _.

Global Instance isequiv_moveR_pM
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: IsEquiv (moveR_pM p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveR_pM p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveR_pM p q r)
  destruct p.
A: Type
x, y: A
q, r: y = x
IsEquiv (moveR_pM 1 q r)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveR_pM
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: (r = q @ p^) <~> (r @ p = q)
:= Build_Equiv _ _ (moveR_pM p q r) _.

Global Instance isequiv_moveR_Vp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y)
: IsEquiv (moveR_Vp p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
IsEquiv (moveR_Vp p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
IsEquiv (moveR_Vp p q r)
  destruct r.
A: Type
x, z: A
p, q: x = z
IsEquiv (moveR_Vp p q 1)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveR_Vp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y)
: (p = r @ q) <~> (r^ @ p = q)
:= Build_Equiv _ _ (moveR_Vp p q r) _.

Global Instance isequiv_moveR_pV
  {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x)
: IsEquiv (moveR_pV p q r).
A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
IsEquiv (moveR_pV p q r)
Proof.
A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
IsEquiv (moveR_pV p q r)
  destruct p.
A: Type
y, z: A
q, r: y = z
IsEquiv (moveR_pV 1 q r)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveR_pV
  {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x)
: (r = q @ p) <~> (r @ p^ = q)
:= Build_Equiv _ _ (moveR_pV p q r) _.

Global Instance isequiv_moveL_Mp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: IsEquiv (moveL_Mp p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveL_Mp p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveL_Mp p q r)
  destruct r.
A: Type
y, z: A
p, q: y = z
IsEquiv (moveL_Mp p q 1)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveL_Mp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: (r^ @ q = p) <~> (q = r @ p)
:= Build_Equiv _ _ (moveL_Mp p q r) _.

Definition isequiv_moveL_pM
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x)
: IsEquiv (moveL_pM p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveL_pM p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: y = x
IsEquiv (moveL_pM p q r)
  destruct p.
A: Type
x, y: A
q, r: y = x
IsEquiv (moveL_pM 1 q r)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveL_pM
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : y = x) :
  q @ p^ = r <~> q = r @ p
  := Build_Equiv _ _ _ (isequiv_moveL_pM p q r).

Global Instance isequiv_moveL_Vp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y)
: IsEquiv (moveL_Vp p q r).
A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
IsEquiv (moveL_Vp p q r)
Proof.
A: Type
x, y, z: A
p: x = z
q: y = z
r: x = y
IsEquiv (moveL_Vp p q r)
  destruct r.
A: Type
x, z: A
p, q: x = z
IsEquiv (moveL_Vp p q 1)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveL_Vp
  {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y)
: r @ q = p <~> q = r^ @ p
:= Build_Equiv _ _ (moveL_Vp p q r) _.

Global Instance isequiv_moveL_pV
  {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x)
: IsEquiv (moveL_pV p q r).
A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
IsEquiv (moveL_pV p q r)
Proof.
A: Type
x, y, z: A
p: z = x
q: y = z
r: y = x
IsEquiv (moveL_pV p q r)
  destruct p.
A: Type
y, z: A
q, r: y = z
IsEquiv (moveL_pV 1 q r)
  apply (isequiv_compose' _ (isequiv_concat_l _ _) _ (isequiv_concat_r _ _)).
Defined.

Definition equiv_moveL_pV
  {A : Type} {x y z : A} (p : z = x) (q : y = z) (r : y = x)
: q @ p = r <~> q = r @ p^
:= Build_Equiv _ _ (moveL_pV p q r) _.

Definition isequiv_moveL_1M {A : Type} {x y : A} (p q : x = y)
: IsEquiv (moveL_1M p q).
A: Type
x, y: A
p, q: x = y
IsEquiv (moveL_1M p q)
Proof.
A: Type
x, y: A
p, q: x = y
IsEquiv (moveL_1M p q)
  destruct q.
A: Type
x: A
p: x = x
IsEquiv (moveL_1M p 1) apply isequiv_concat_l.
Defined.

Definition isequiv_moveL_M1 {A : Type} {x y : A} (p q : x = y)
: IsEquiv (moveL_M1 p q).
A: Type
x, y: A
p, q: x = y
IsEquiv (moveL_M1 p q)
Proof.
A: Type
x, y: A
p, q: x = y
IsEquiv (moveL_M1 p q)
  destruct q.
A: Type
x: A
p: x = x
IsEquiv (moveL_M1 p 1) apply isequiv_concat_l.
Defined.

Definition isequiv_moveL_1V {A : Type} {x y : A} (p : x = y) (q : y = x)
: IsEquiv (moveL_1V p q).
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveL_1V p q)
Proof.
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveL_1V p q)
  destruct q.
A: Type
y: A
p: y = y
IsEquiv (moveL_1V p 1) apply isequiv_concat_l.
Defined.

Definition isequiv_moveL_V1 {A : Type} {x y : A} (p : x = y) (q : y = x)
: IsEquiv (moveL_V1 p q).
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveL_V1 p q)
Proof.
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveL_V1 p q)
  destruct q.
A: Type
y: A
p: y = y
IsEquiv (moveL_V1 p 1) apply isequiv_concat_l.
Defined.

Definition isequiv_moveR_M1 {A : Type} {x y : A} (p q : x = y)
: IsEquiv (moveR_M1 p q).
A: Type
x, y: A
p, q: x = y
IsEquiv (moveR_M1 p q)
Proof.
A: Type
x, y: A
p, q: x = y
IsEquiv (moveR_M1 p q)
  destruct p.
A: Type
x: A
q: x = x
IsEquiv (moveR_M1 1 q) apply isequiv_concat_r.
Defined.

Global Instance isequiv_moveR_1M {A : Type} {x y : A} (p q : x = y)
: IsEquiv (moveR_1M p q).
A: Type
x, y: A
p, q: x = y
IsEquiv (moveR_1M p q)
Proof.
A: Type
x, y: A
p, q: x = y
IsEquiv (moveR_1M p q)
  destruct p.
A: Type
x: A
q: x = x
IsEquiv (moveR_1M 1 q) apply isequiv_concat_r.
Defined.

Definition equiv_moveR_1M {A : Type} {x y : A} (p q : x = y)
  : (1 = q @ p^) <~> (p = q)
  := Build_Equiv _ _ (moveR_1M p q) _.

Definition isequiv_moveR_1V {A : Type} {x y : A} (p : x = y) (q : y = x)
: IsEquiv (moveR_1V p q).
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveR_1V p q)
Proof.
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveR_1V p q)
  destruct p.
A: Type
x: A
q: x = x
IsEquiv (moveR_1V 1 q) apply isequiv_concat_r.
Defined.

Definition isequiv_moveR_V1 {A : Type} {x y : A} (p : x = y) (q : y = x)
: IsEquiv (moveR_V1 p q).
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveR_V1 p q)
Proof.
A: Type
x, y: A
p: x = y
q: y = x
IsEquiv (moveR_V1 p q)
  destruct p.
A: Type
x: A
q: x = x
IsEquiv (moveR_V1 1 q) apply isequiv_concat_r.
Defined.


Definition moveR_moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : transport P p u = v)
  : moveR_transport_p P p u v (moveL_transport_V P p u v q) = q.
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: transport P p u = v
moveR_transport_p P p u v
  (moveL_transport_V P p u v q) = 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
moveR_transport_p P p u v
  (moveL_transport_V P p u v q) = q
  destruct p; reflexivity.
Defined.

Definition moveL_moveR_transport_p {A : Type} (P : A -> Type) {x y : A}
           (p : x = y) (u : P x) (v : P y) (q : u = transport P p^ v)
  : moveL_transport_V P p u v (moveR_transport_p P p u v q) = q.
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
q: u = transport P p^ v
moveL_transport_V P p u v
  (moveR_transport_p P p u v q) = 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
moveL_transport_V P p u v
  (moveR_transport_p P p u v q) = q
  destruct p; reflexivity.
Defined.

Global Instance isequiv_moveR_transport_p {A : Type} (P : A -> Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
: IsEquiv (moveR_transport_p P p u v).
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
IsEquiv (moveR_transport_p P p u v)
Proof.
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
IsEquiv (moveR_transport_p P p u v)
  srapply isequiv_adjointify.
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
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveR_transport_p P p u v o ?g == idmap
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
?g o moveR_transport_p P p u v == idmap
  -
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 apply moveL_transport_V.
  -
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveR_transport_p P p u v o moveL_transport_V P p u v ==
idmap intro q; apply moveR_moveL_transport_V.
  -
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveL_transport_V P p u v o moveR_transport_p P p u v ==
idmap intro q; apply moveL_moveR_transport_p.
Defined.

Definition equiv_moveR_transport_p {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
:= Build_Equiv _ _ (moveR_transport_p P p u v) _.


Definition moveR_moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : transport P p^ u = v)
  : moveR_transport_V P p u v (moveL_transport_p P p u v q) = q.
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: transport P p^ u = v
moveR_transport_V P p u v
  (moveL_transport_p P p u v q) = 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
moveR_transport_V P p u v
  (moveL_transport_p P p u v q) = q
  destruct p; reflexivity.
Defined.

Definition moveL_moveR_transport_V {A : Type} (P : A -> Type) {x y : A}
           (p : y = x) (u : P x) (v : P y) (q : u = transport P p v)
  : moveL_transport_p P p u v (moveR_transport_V P p u v q) = q.
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
q: u = transport P p v
moveL_transport_p P p u v
  (moveR_transport_V P p u v q) = 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
moveL_transport_p P p u v
  (moveR_transport_V P p u v q) = q
  destruct p; reflexivity.
Defined.

Global Instance isequiv_moveR_transport_V {A : Type} (P : A -> Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
: IsEquiv (moveR_transport_V P p u v).
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
IsEquiv (moveR_transport_V P p u v)
Proof.
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
IsEquiv (moveR_transport_V P p u v)
  srapply isequiv_adjointify.
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
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveR_transport_V P p u v o ?g == idmap
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
?g o moveR_transport_V P p u v == idmap
  -
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 apply moveL_transport_p.
  -
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveR_transport_V P p u v o moveL_transport_p P p u v ==
idmap intro q; apply moveR_moveL_transport_p.
  -
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveL_transport_p P p u v o moveR_transport_V P p u v ==
idmap intro q; apply moveL_moveR_transport_V.
Defined.

Definition equiv_moveR_transport_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
:= Build_Equiv _ _ (moveR_transport_V P p u v) _.

Global Instance isequiv_moveL_transport_V {A : Type} (P : A -> Type) {x y : A}
  (p : x = y) (u : P x) (v : P y)
: IsEquiv (moveL_transport_V P p u v).
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
IsEquiv (moveL_transport_V P p u v)
Proof.
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
IsEquiv (moveL_transport_V P p u v)
  srapply isequiv_adjointify.
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
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveL_transport_V P p u v o ?g == idmap
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
?g o moveL_transport_V P p u v == idmap
  -
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 apply moveR_transport_p.
  -
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveL_transport_V P p u v o moveR_transport_p P p u v ==
idmap intro q; apply moveL_moveR_transport_p.
  -
A: Type
P: A -> Type
x, y: A
p: x = y
u: P x
v: P y
moveR_transport_p P p u v o moveL_transport_V P p u v ==
idmap intro q; apply moveR_moveL_transport_V.
Defined.

Definition equiv_moveL_transport_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
:= Build_Equiv _ _ (moveL_transport_V P p u v) _.

Global Instance isequiv_moveL_transport_p {A : Type} (P : A -> Type) {x y : A}
  (p : y = x) (u : P x) (v : P y)
: IsEquiv (moveL_transport_p P p u v).
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
IsEquiv (moveL_transport_p P p u v)
Proof.
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
IsEquiv (moveL_transport_p P p u v)
  srapply isequiv_adjointify.
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
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveL_transport_p P p u v o ?g == idmap
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
?g o moveL_transport_p P p u v == idmap
  -
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 apply moveR_transport_V.
  -
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveL_transport_p P p u v o moveR_transport_V P p u v ==
idmap intro q; apply moveL_moveR_transport_V.
  -
A: Type
P: A -> Type
x, y: A
p: y = x
u: P x
v: P y
moveR_transport_V P p u v o moveL_transport_p P p u v ==
idmap intro q; apply moveR_moveL_transport_p.
Defined.

Definition equiv_moveL_transport_p {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
:= Build_Equiv _ _ (moveL_transport_p P p u v) _.

Global Instance isequiv_moveR_equiv_M `{IsEquiv A B f} (x : A) (y : B)
: IsEquiv (@moveR_equiv_M A B f _ x y).
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv (moveR_equiv_M x y)
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv (moveR_equiv_M x y)
  unfold moveR_equiv_M.
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv (fun p : x = f^-1 y => ap f p @ eisretr f y)
  refine (@isequiv_compose _ _ (ap f) _ _ (fun q => q @ eisretr f y) _).
Defined.

Definition equiv_moveR_equiv_M `{IsEquiv A B f} (x : A) (y : B)
  : (x = f^-1 y) <~> (f x = y)
  := Build_Equiv _ _ (@moveR_equiv_M A B f _ x y) _.

Global Instance isequiv_moveR_equiv_V `{IsEquiv A B f} (x : B) (y : A)
: IsEquiv (@moveR_equiv_V A B f _ x y).
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv (moveR_equiv_V x y)
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv (moveR_equiv_V x y)
  unfold moveR_equiv_V.
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv (fun p : x = f y => ap f^-1 p @ eissect f y)
  refine (@isequiv_compose _ _ (ap f^-1) _ _ (fun q => q @ eissect f y) _).
Defined.

Definition equiv_moveR_equiv_V `{IsEquiv A B f} (x : B) (y : A)
  : (x = f y) <~> (f^-1 x = y)
  := Build_Equiv _ _ (@moveR_equiv_V A B f _ x y) _.

Global Instance isequiv_moveL_equiv_M `{IsEquiv A B f} (x : A) (y : B)
: IsEquiv (@moveL_equiv_M A B f _ x y).
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv (moveL_equiv_M x y)
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv (moveL_equiv_M x y)
  unfold moveL_equiv_M.
A, B: Type
f: A -> B
H: IsEquiv f
x: A
y: B
IsEquiv
  (fun p : f^-1 y = x => (eisretr f y)^ @ ap f p)
  refine (@isequiv_compose _ _ (ap f) _ _ (fun q => (eisretr f y)^ @ q) _).
Defined.

Definition equiv_moveL_equiv_M `{IsEquiv A B f} (x : A) (y : B)
  : (f^-1 y = x) <~> (y = f x)
  := Build_Equiv _ _ (@moveL_equiv_M A B f _ x y) _.

Global Instance isequiv_moveL_equiv_V `{IsEquiv A B f} (x : B) (y : A)
: IsEquiv (@moveL_equiv_V A B f _ x y).
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv (moveL_equiv_V x y)
Proof.
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv (moveL_equiv_V x y)
  unfold moveL_equiv_V.
A, B: Type
f: A -> B
H: IsEquiv f
x: B
y: A
IsEquiv
  (fun p : f y = x => (eissect f y)^ @ ap f^-1 p)
  refine (@isequiv_compose _ _ (ap f^-1) _ _ (fun q => (eissect f y)^ @ q) _).
Defined.

Definition equiv_moveL_equiv_V `{IsEquiv A B f} (x : B) (y : A)
  : (f y = x) <~> (y = f^-1 x)
  := Build_Equiv _ _ (@moveL_equiv_V A B f _ x y) _.

(** *** Dependent paths *)

(** Usually, a dependent path over [p:x1=x2] in [P:A->Type] between [y1:P x1] and [y2:P x2] is a path [transport P p y1 = y2] in [P x2].  However, when [P] is a path space, these dependent paths have a more convenient description: rather than transporting the left side both forwards and backwards, we transport both sides of the equation forwards, forming a sort of "naturality square".

   We use the same naming scheme as for the transport lemmas. *)

Definition dpath_path_l {A : Type} {x1 x2 y : A}
  (p : x1 = x2) (q : x1 = y) (r : x2 = y)
  : q = p @ r
  <~>
  transport (fun x => x = y) p q = r.
A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
r: x2 = y
q = p @ r <~> transport (fun x : A => x = y) p q = r
Proof.
A: Type
x1, x2, y: A
p: x1 = x2
q: x1 = y
r: x2 = y
q = p @ r <~> transport (fun x : A => x = y) p q = r
  destruct p; simpl.
A: Type
x1, y: A
q, r: x1 = y
q = 1 @ r <~> q = r
  exact (equiv_concat_r (concat_1p r) q).
Defined.

Definition dpath_path_r {A : Type} {x y1 y2 : A}
  (p : y1 = y2) (q : x = y1) (r : x = y2)
  : q @ p = r
  <~>
  transport (fun y => x = y) p q = r.
A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
r: x = y2
q @ p = r <~> transport (fun y : A => x = y) p q = r
Proof.
A: Type
x, y1, y2: A
p: y1 = y2
q: x = y1
r: x = y2
q @ p = r <~> transport (fun y : A => x = y) p q = r
  destruct p; simpl.
A: Type
x, y1: A
q, r: x = y1
q @ 1 = r <~> q = r
  exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_path_lr {A : Type} {x1 x2 : A}
  (p : x1 = x2) (q : x1 = x1) (r : x2 = x2)
  : q @ p = p @ r
  <~>
  transport (fun x => x = x) p q = r.
A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
r: x2 = x2
q @ p = p @ r <~>
transport (fun x : A => x = x) p q = r
Proof.
A: Type
x1, x2: A
p: x1 = x2
q: x1 = x1
r: x2 = x2
q @ p = p @ r <~>
transport (fun x : A => x = x) p q = r
  destruct p; simpl.
A: Type
x1: A
q, r: x1 = x1
q @ 1 = 1 @ r <~> q = r
  transitivity (q @ 1 = r).
A: Type
x1: A
q, r: x1 = x1
q @ 1 = 1 @ r <~> q @ 1 = r
A: Type
x1: A
q, r: x1 = x1
q @ 1 = r <~> q = r
  -
A: Type
x1: A
q, r: x1 = x1
q @ 1 = 1 @ r <~> q @ 1 = r exact (equiv_concat_r (concat_1p r) (q @ 1)).
  -
A: Type
x1: A
q, r: x1 = x1
q @ 1 = r <~> q = r exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_path_Fl {A B : Type} {f : A -> B} {x1 x2 : A} {y : B}
  (p : x1 = x2) (q : f x1 = y) (r : f x2 = y)
  : q = ap f p @ r
  <~>
  transport (fun x => f x = y) p q = r.
A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
r: f x2 = y
q = ap f p @ r <~>
transport (fun x : A => f x = y) p q = r
Proof.
A, B: Type
f: A -> B
x1, x2: A
y: B
p: x1 = x2
q: f x1 = y
r: f x2 = y
q = ap f p @ r <~>
transport (fun x : A => f x = y) p q = r
  destruct p; simpl.
A, B: Type
f: A -> B
x1: A
y: B
q, r: f x1 = y
q = 1 @ r <~> q = r
  exact (equiv_concat_r (concat_1p r) q).
Defined.

Definition dpath_path_Fr {A B : Type} {g : A -> B} {x : B} {y1 y2 : A}
  (p : y1 = y2) (q : x = g y1) (r : x = g y2)
  : q @ ap g p = r
  <~>
  transport (fun y => x = g y) p q = r.
A, B: Type
g: A -> B
x: B
y1, y2: A
p: y1 = y2
q: x = g y1
r: x = g y2
q @ ap g p = r <~>
transport (fun y : A => x = g y) p q = r
Proof.
A, B: Type
g: A -> B
x: B
y1, y2: A
p: y1 = y2
q: x = g y1
r: x = g y2
q @ ap g p = r <~>
transport (fun y : A => x = g y) p q = r
  destruct p; simpl.
A, B: Type
g: A -> B
x: B
y1: A
q, r: x = g y1
q @ 1 = r <~> q = r
  exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_path_FlFr {A B : Type} {f g : A -> B} {x1 x2 : A}
  (p : x1 = x2) (q : f x1 = g x1) (r : f x2 = g x2)
  : q @ ap g p = ap f p @ r
  <~>
  transport (fun x => f x = g x) p q = r.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
q @ ap g p = ap f p @ r <~>
transport (fun x : A => f x = g x) p q = r
Proof.
A, B: Type
f, g: A -> B
x1, x2: A
p: x1 = x2
q: f x1 = g x1
r: f x2 = g x2
q @ ap g p = ap f p @ r <~>
transport (fun x : A => f x = g x) p q = r
  destruct p; simpl.
A, B: Type
f, g: A -> B
x1: A
q, r: f x1 = g x1
q @ 1 = 1 @ r <~> q = r
  transitivity (q @ 1 = r).
A, B: Type
f, g: A -> B
x1: A
q, r: f x1 = g x1
q @ 1 = 1 @ r <~> q @ 1 = r
A, B: Type
f, g: A -> B
x1: A
q, r: f x1 = g x1
q @ 1 = r <~> q = r
  -
A, B: Type
f, g: A -> B
x1: A
q, r: f x1 = g x1
q @ 1 = 1 @ r <~> q @ 1 = r exact (equiv_concat_r (concat_1p r) (q @ 1)).
  -
A, B: Type
f, g: A -> B
x1: A
q, r: f x1 = g x1
q @ 1 = r <~> q = r exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_path_FFlr {A B : Type} {f : A -> B} {g : B -> A}
  {x1 x2 : A} (p : x1 = x2) (q : g (f x1) = x1) (r : g (f x2) = x2)
  : q @ p = ap g (ap f p) @ r
  <~>
  transport (fun x => g (f x) = x) p q = r.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
q @ p = ap g (ap f p) @ r <~>
transport (fun x : A => g (f x) = x) p q = r
Proof.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: g (f x1) = x1
r: g (f x2) = x2
q @ p = ap g (ap f p) @ r <~>
transport (fun x : A => g (f x) = x) p q = r
  destruct p; simpl.
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: g (f x1) = x1
q @ 1 = 1 @ r <~> q = r
  transitivity (q @ 1 = r).
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: g (f x1) = x1
q @ 1 = 1 @ r <~> q @ 1 = r
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: g (f x1) = x1
q @ 1 = r <~> q = r
  -
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: g (f x1) = x1
q @ 1 = 1 @ r <~> q @ 1 = r exact (equiv_concat_r (concat_1p r) (q @ 1)).
  -
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: g (f x1) = x1
q @ 1 = r <~> q = r exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_path_lFFr {A B : Type} {f : A -> B} {g : B -> A}
  {x1 x2 : A} (p : x1 = x2) (q : x1 = g (f x1)) (r : x2 = g (f x2))
  : q @ ap g (ap f p) = p @ r
  <~>
  transport (fun x => x = g (f x)) p q = r.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
r: x2 = g (f x2)
q @ ap g (ap f p) = p @ r <~>
transport (fun x : A => x = g (f x)) p q = r
Proof.
A, B: Type
f: A -> B
g: B -> A
x1, x2: A
p: x1 = x2
q: x1 = g (f x1)
r: x2 = g (f x2)
q @ ap g (ap f p) = p @ r <~>
transport (fun x : A => x = g (f x)) p q = r
  destruct p; simpl.
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: x1 = g (f x1)
q @ 1 = 1 @ r <~> q = r
  transitivity (q @ 1 = r).
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: x1 = g (f x1)
q @ 1 = 1 @ r <~> q @ 1 = r
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: x1 = g (f x1)
q @ 1 = r <~> q = r
  -
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: x1 = g (f x1)
q @ 1 = 1 @ r <~> q @ 1 = r exact (equiv_concat_r (concat_1p r) (q @ 1)).
  -
A, B: Type
f: A -> B
g: B -> A
x1: A
q, r: x1 = g (f x1)
q @ 1 = r <~> q = r exact (equiv_concat_l (concat_p1 q)^ r).
Defined.

Definition dpath_paths2 {A : Type} {x y : A}
           (p : x = y) (q : idpath x = idpath x)
           (r : idpath y = idpath y)
: (concat_1p p)^ @ whiskerR q p @ concat_1p p
  = (concat_p1 p)^ @ whiskerL p r @ concat_p1 p
  <~>
  transport (fun a => idpath a = idpath a) p q = r.
A: Type
x, y: A
p: x = y
q, r: 1 = 1
((concat_1p p)^ @ whiskerR q p) @ concat_1p p =
((concat_p1 p)^ @ whiskerL p r) @ concat_p1 p <~>
transport (fun a : A => 1 = 1) p q = r
Proof.
A: Type
x, y: A
p: x = y
q, r: 1 = 1
((concat_1p p)^ @ whiskerR q p) @ concat_1p p =
((concat_p1 p)^ @ whiskerL p r) @ concat_p1 p <~>
transport (fun a : A => 1 = 1) p q = r
  destruct p.
A: Type
x: A
q, r: 1 = 1
((concat_1p 1)^ @ whiskerR q 1) @ concat_1p 1 =
((concat_p1 1)^ @ whiskerL 1 r) @ concat_p1 1 <~>
transport (fun a : A => 1 = 1) 1 q = r simpl.
A: Type
x: A
q, r: 1 = 1
(1 @ whiskerR q 1) @ 1 = (1 @ whiskerL 1 r) @ 1 <~>
q = r
  refine (_ oE (equiv_whiskerR _ _ 1)^-1).
A: Type
x: A
q, r: 1 = 1
1 @ whiskerR q 1 = 1 @ whiskerL 1 r <~> q = r
  refine (_ oE (equiv_whiskerL 1 _ _)^-1).
A: Type
x: A
q, r: 1 = 1
whiskerR q 1 = whiskerL 1 r <~> q = r
  refine (equiv_concat_lr _ _).
A: Type
x: A
q, r: 1 = 1
q = whiskerR q 1
A: Type
x: A
q, r: 1 = 1
whiskerL 1 r = r
  -
A: Type
x: A
q, r: 1 = 1
q = whiskerR q 1 symmetry; apply whiskerR_p1_1.
  -
A: Type
x: A
q, r: 1 = 1
whiskerL 1 r = r apply whiskerL_1p_1.
Defined.

(** ** Universal mapping property *)

Global Instance isequiv_paths_ind `{Funext} {A : Type} (a : A)
  (P : forall x, (a = x) -> Type)
  : IsEquiv (paths_ind a P) | 0.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
IsEquiv (paths_ind a P)
Proof.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
IsEquiv (paths_ind a P)
  refine (isequiv_adjointify (paths_ind a P) (fun f => f a 1) _ _).
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
(fun x : forall (y : A) (p : a = y), P y p =>
 paths_ind a P (x a 1)) == idmap
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
(fun x : P a 1 => paths_ind a P x a 1) == idmap
  -
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
(fun x : forall (y : A) (p : a = y), P y p =>
 paths_ind a P (x a 1)) == idmap intros f.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
f: forall (y : A) (p : a = y), P y p
paths_ind a P (f a 1) = f
    apply path_forall; intros x.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
f: forall (y : A) (p : a = y), P y p
x: A
paths_ind a P (f a 1) x = f x
    apply path_forall; intros p.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
f: forall (y : A) (p : a = y), P y p
x: A
p: a = x
paths_ind a P (f a 1) x p = f x p
    destruct p; reflexivity.
  -
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
(fun x : P a 1 => paths_ind a P x a 1) == idmap intros u.
H: Funext
A: Type
a: A
P: forall x : A, a = x -> Type
u: P a 1
paths_ind a P u a 1 = u reflexivity.
Defined.

Definition equiv_paths_ind `{Funext} {A : Type} (a : A)
  (P : forall x, (a = x) -> Type)
  : P a 1 <~> forall x p, P x p
  := Build_Equiv _ _ (paths_ind a P) _.

Global Instance isequiv_paths_ind_r `{Funext} {A : Type} (a : A)
  (P : forall x, (x = a) -> Type)
  : IsEquiv (paths_ind_r a P) | 0.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
IsEquiv (paths_ind_r a P)
Proof.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
IsEquiv (paths_ind_r a P)
  refine (isequiv_adjointify (paths_ind_r a P) (fun f => f a 1) _ _).
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
(fun x : forall (y : A) (p : y = a), P y p =>
 paths_ind_r a P (x a 1)) == idmap
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
(fun x : P a 1 => paths_ind_r a P x a 1) == idmap
  -
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
(fun x : forall (y : A) (p : y = a), P y p =>
 paths_ind_r a P (x a 1)) == idmap intros f.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
f: forall (y : A) (p : y = a), P y p
paths_ind_r a P (f a 1) = f
    apply path_forall; intros x.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
f: forall (y : A) (p : y = a), P y p
x: A
paths_ind_r a P (f a 1) x = f x
    apply path_forall; intros p.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
f: forall (y : A) (p : y = a), P y p
x: A
p: x = a
paths_ind_r a P (f a 1) x p = f x p
    destruct p; reflexivity.
  -
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
(fun x : P a 1 => paths_ind_r a P x a 1) == idmap intros u.
H: Funext
A: Type
a: A
P: forall x : A, x = a -> Type
u: P a 1
paths_ind_r a P u a 1 = u reflexivity.
Defined.

Definition equiv_paths_ind_r `{Funext} {A : Type} (a : A)
  (P : forall x, (x = a) -> Type)
  : P a 1 <~> forall x p, P x p
  := Build_Equiv _ _ (paths_ind_r a P) _.

(** ** Truncation *)

(** Paths reduce truncation level by one.  This is essentially the definition of [IsTrunc_internal]. *)