CommutativeSquares.v

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

(** * Commutative squares *)

(** Commutative squares compose vertically.

      A --f--> B
      |    //  |
      h  comm  g
      |  //    |
      V //     V
      C --f'-> D
      |    //  |
      h' comm' g'
      |  //    |
      V //     V
      E --f''> F
*)
Lemma comm_square_comp {A B C D E F}
  {f : A -> B} {f': C -> D} {h : A -> C} {g : B -> D} (comm : f' o h == g o f)
  {f'': E -> F} {h' : C -> E} {g' : D -> F} (comm' : f'' o h' == g' o f')
  : f'' o (h' o h) == (g' o g) o f.A, B, C, D, E, F: Type
f: A -> B
f': C -> D
h: A -> C
g: B -> D
comm: f' o h == g o f
f'': E -> F
h': C -> E
g': D -> F
comm': f'' o h' == g' o f'
f'' o (h' o h) == g' o g o f
Proof.A, B, C, D, E, F: Type
f: A -> B
f': C -> D
h: A -> C
g: B -> D
comm: f' o h == g o f
f'': E -> F
h': C -> E
g': D -> F
comm': f'' o h' == g' o f'
f'' o (h' o h) == g' o g o f
  intros x.A, B, C, D, E, F: Type
f: A -> B
f': C -> D
h: A -> C
g: B -> D
comm: f' o h == g o f
f'': E -> F
h': C -> E
g': D -> F
comm': f'' o h' == g' o f'
x: A
f'' (h' (h x)) = g' (g (f x))
  path_via (g' (f' (h x))).A, B, C, D, E, F: Type
f: A -> B
f': C -> D
h: A -> C
g: B -> D
comm: f' o h == g o f
f'': E -> F
h': C -> E
g': D -> F
comm': f'' o h' == g' o f'
x: A
g' (f' (h x)) = g' (g (f x))
  apply ap, comm.
Defined.

(** Commutative squares compose horizontally.

      A --k--> B --l--> C
      |    //  |    //  |
      f  comm  g  comm  h
      |  //    |  //    |
      V //     V //     V
      X --i--> Y --j--> Z
*)

Lemma comm_square_comp' {A B C X Y Z : Type}
    {k : A -> B} {l : B -> C}
    {f : A -> X} {g : B -> Y} {h : C -> Z}
    {i : X -> Y} {j : Y -> Z}
    (H : i o f == g o k) (K : j o g == h o l)
  : (j o i) o f == h o (l o k).A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
j o i o f == h o (l o k)
Proof.A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
j o i o f == h o (l o k)
  intros x.A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
x: A
j (i (f x)) = h (l (k x))
  path_via (j (g (k x))).A, B, C, X, Y, Z: Type
k: A -> B
l: B -> C
f: A -> X
g: B -> Y
h: C -> Z
i: X -> Y
j: Y -> Z
H: i o f == g o k
K: j o g == h o l
x: A
j (i (f x)) = j (g (k x))
  apply ap, H.
Defined.

(** Given any commutative square from [f] to [f'] whose verticals
[wA, wB] are equivalences, the [equiv_inv] square from [f'] to [f] with verticals [wA ^-1, wB ^-1] also commutes. *)
Lemma comm_square_inverse
  {A B : Type} {f : A -> B}
  {A' B' : Type} {f' : A' -> B'}
  {wA : A <~> A'} {wB : B <~> B'}
  (wf : f' o wA == wB o f)
: f o (wA ^-1) == (wB ^-1) o f'.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
f o wA^-1 == wB^-1 o f'
Proof.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
f o wA^-1 == wB^-1 o f'
  intros a'.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
f (wA^-1 a') = wB^-1 (f' a')
  path_via (wB ^-1 (wB (f (wA ^-1 a')))).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
f (wA^-1 a') = wB^-1 (wB (f (wA^-1 a')))
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
wB^-1 (wB (f (wA^-1 a'))) = wB^-1 (f' a')
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
f (wA^-1 a') = wB^-1 (wB (f (wA^-1 a'))) apply inverse, eissect.
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
wB^-1 (wB (f (wA^-1 a'))) = wB^-1 (f' a') apply ap, (concat (wf _)^).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a': A'
f' (wA (wA^-1 a')) = f' a'
    apply ap, eisretr.
Defined.

(** Up to naturality, the result of [comm_square_inverse] really is a
retraction (aka left inverse); *)
Lemma comm_square_inverse_is_sect
  {A B : Type} {f : A -> B}
  {A' B' : Type} {f' : A' -> B'}
  (wA : A <~> A') (wB : B <~> B')
  (wf : f' o wA == wB o f) (a : A)
  : comm_square_comp wf (comm_square_inverse wf) a @ eissect wB (f a)
   = ap f (eissect wA a).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
comm_square_comp wf (comm_square_inverse wf) a @
eissect wB (f a) = ap f (eissect wA a)
Proof.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
comm_square_comp wf (comm_square_inverse wf) a @
eissect wB (f a) = ap f (eissect wA a)
  unfold comm_square_inverse, comm_square_comp; simpl.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
(((eissect wB (f (wA^-1 (wA a))))^ @
  ap wB^-1
    ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a)))) @
 ap wB^-1 (wf a)) @ eissect wB (f a) =
ap f (eissect wA a)
  repeat lhs napply concat_pp_p.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
(eissect wB (f (wA^-1 (wA a))))^ @
(ap wB^-1
   ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
 (ap wB^-1 (wf a) @ eissect wB (f a))) =
ap f (eissect wA a) apply moveR_Vp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
(ap wB^-1 (wf a) @ eissect wB (f a)) =
eissect wB (f (wA^-1 (wA a))) @ ap f (eissect wA a)
  transitivity (ap (wB ^-1 o wB) (ap f (eissect wA a)) @ eissect wB (f a)).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
(ap wB^-1 (wf a) @ eissect wB (f a)) =
ap (wB^-1 o wB) (ap f (eissect wA a)) @
eissect wB (f a)
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap (wB^-1 o wB) (ap f (eissect wA a)) @
eissect wB (f a) =
eissect wB (f (wA^-1 (wA a))) @ ap f (eissect wA a)
  2: {A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap (wB^-1 o wB) (ap f (eissect wA a)) @
eissect wB (f a) =
eissect wB (f (wA^-1 (wA a))) @ ap f (eissect wA a) lhs napply (concat_Ap (eissect wB)).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
eissect wB (f (wA^-1 (wA a))) @
ap idmap (ap f (eissect wA a)) =
eissect wB (f (wA^-1 (wA a))) @ ap f (eissect wA a)
       apply ap, ap_idmap. }A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
(ap wB^-1 (wf a) @ eissect wB (f a)) =
ap (wB^-1 o wB) (ap f (eissect wA a)) @
eissect wB (f a)
  lhs napply concat_p_pp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
(ap wB^-1
   ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
 ap wB^-1 (wf a)) @ eissect wB (f a) =
ap (fun x : B => wB^-1 (wB x)) (ap f (eissect wA a)) @
eissect wB (f a)
  apply whiskerR.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  ((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
ap wB^-1 (wf a) =
ap (fun x : B => wB^-1 (wB x)) (ap f (eissect wA a))
  lhs_V napply ap_pp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  (((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
   wf a) =
ap (fun x : B => wB^-1 (wB x)) (ap f (eissect wA a))
  rhs napply ap_compose.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap wB^-1
  (((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
   wf a) = ap wB^-1 (ap wB (ap f (eissect wA a)))
  apply ap.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
((wf (wA^-1 (wA a)))^ @ ap f' (eisretr wA (wA a))) @
wf a = ap wB (ap f (eissect wA a))
  lhs napply concat_pp_p.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
(wf (wA^-1 (wA a)))^ @
(ap f' (eisretr wA (wA a)) @ wf a) =
ap wB (ap f (eissect wA a))
  apply moveR_Vp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap f' (eisretr wA (wA a)) @ wf a =
wf (wA^-1 (wA a)) @ ap wB (ap f (eissect wA a))
  path_via (ap (f' o wA) (eissect wA a) @ wf a).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap f' (eisretr wA (wA a)) @ wf a =
ap (fun x : A => f' (wA x)) (eissect wA a) @ wf a
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap (fun x : A => f' (wA x)) (eissect wA a) @ wf a =
wf (wA^-1 (wA a)) @ ap wB (ap f (eissect wA a))
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap f' (eisretr wA (wA a)) @ wf a =
ap (fun x : A => f' (wA x)) (eissect wA a) @ wf a apply whiskerR.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap f' (eisretr wA (wA a)) =
ap (fun x : A => f' (wA x)) (eissect wA a) rhs napply ap_compose.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap f' (eisretr wA (wA a)) =
ap f' (ap wA (eissect wA a))
    apply ap, eisadj.
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
ap (fun x : A => f' (wA x)) (eissect wA a) @ wf a =
wf (wA^-1 (wA a)) @ ap wB (ap f (eissect wA a)) lhs napply (concat_Ap wf).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A
wf (wA^-1 (wA a)) @
ap (fun x : A => wB (f x)) (eissect wA a) =
wf (wA^-1 (wA a)) @ ap wB (ap f (eissect wA a))
    apply whiskerL, (ap_compose f wB).
Defined.

(** and similarly, [comm_square_inverse] is a section (aka right [equiv_inv]). *)
Lemma comm_square_inverse_is_retr
  {A B : Type} {f : A -> B}
  {A' B' : Type} {f' : A' -> B'}
  (wA : A <~> A') (wB : B <~> B')
  (wf : f' o wA == wB o f) (a : A')
  : comm_square_comp (comm_square_inverse wf) wf a @ eisretr wB (f' a)
  = ap f' (eisretr wA a).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
comm_square_comp (comm_square_inverse wf) wf a @
eisretr wB (f' a) = ap f' (eisretr wA a)
Proof.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
comm_square_comp (comm_square_inverse wf) wf a @
eisretr wB (f' a) = ap f' (eisretr wA a)
  unfold comm_square_inverse, comm_square_comp; simpl.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
(wf (wA^-1 a) @
 ap wB
   ((eissect wB (f (wA^-1 a)))^ @
    ap wB^-1 ((wf (wA^-1 a))^ @ ap f' (eisretr wA a)))) @
eisretr wB (f' a) = ap f' (eisretr wA a)
  rewrite !ap_pp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
(wf (wA^-1 a) @
 (ap wB (eissect wB (f (wA^-1 a)))^ @
  (ap wB (ap wB^-1 (wf (wA^-1 a))^) @
   ap wB (ap wB^-1 (ap f' (eisretr wA a)))))) @
eisretr wB (f' a) = ap f' (eisretr wA a)
  rewrite <- !concat_pp_p.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
(((wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
  ap wB (ap wB^-1 (wf (wA^-1 a))^)) @
 ap wB (ap wB^-1 (ap f' (eisretr wA a)))) @
eisretr wB (f' a) = ap f' (eisretr wA a)
  rewrite concat_pp_p.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
((wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
 ap wB (ap wB^-1 (wf (wA^-1 a))^)) @
(ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
 eisretr wB (f' a)) = ap f' (eisretr wA a)
  set (p := (ap wB (ap (wB ^-1) (ap f' (eisretr wA a)))
            @ eisretr wB (f' a))).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
((wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
 ap wB (ap wB^-1 (wf (wA^-1 a))^)) @ p =
ap f' (eisretr wA a)
  path_via ((eisretr wB _)^ @ p).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
((wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
 ap wB (ap wB^-1 (wf (wA^-1 a))^)) @ p =
(eisretr wB (f' (wA (wA^-1 a))))^ @ p
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
(eisretr wB (f' (wA (wA^-1 a))))^ @ p =
ap f' (eisretr wA a)
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
((wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
 ap wB (ap wB^-1 (wf (wA^-1 a))^)) @ p =
(eisretr wB (f' (wA (wA^-1 a))))^ @ p apply whiskerR.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
(wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^) @
ap wB (ap wB^-1 (wf (wA^-1 a))^) =
(eisretr wB (f' (wA (wA^-1 a))))^
    apply moveR_pM.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
(ap wB (ap wB^-1 (wf (wA^-1 a))^))^
    path_via ((eisretr wB (f' (wA (wA ^-1 a))))^ @
      ap (wB o wB ^-1) (wf ((wA ^-1) a))).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a))
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a)) =
(eisretr wB (f' (wA (wA^-1 a))))^ @
(ap wB (ap wB^-1 (wf (wA^-1 a))^))^
    +A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ ap wB (eissect wB (f (wA^-1 a)))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a)) rewrite ap_V, <- eisadj.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ (eisretr wB (wB (f (wA^-1 a))))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a))
      transitivity (ap idmap (wf ((wA ^-1) a))
                       @ (eisretr wB (wB (f ((wA ^-1) a))))^).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ (eisretr wB (wB (f (wA^-1 a))))^ =
ap idmap (wf (wA^-1 a)) @
(eisretr wB (wB (f (wA^-1 a))))^
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
ap idmap (wf (wA^-1 a)) @
(eisretr wB (wB (f (wA^-1 a))))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a))
      *A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
wf (wA^-1 a) @ (eisretr wB (wB (f (wA^-1 a))))^ =
ap idmap (wf (wA^-1 a)) @
(eisretr wB (wB (f (wA^-1 a))))^ apply whiskerR, inverse, ap_idmap.
      *A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
ap idmap (wf (wA^-1 a)) @
(eisretr wB (wB (f (wA^-1 a))))^ =
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a)) exact (concat_Ap (fun b' => (eisretr wB b')^) _).
    +A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
(eisretr wB (f' (wA (wA^-1 a))))^ @
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a)) =
(eisretr wB (f' (wA (wA^-1 a))))^ @
(ap wB (ap wB^-1 (wf (wA^-1 a))^))^ apply ap.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
ap (fun x : B' => wB (wB^-1 x)) (wf (wA^-1 a)) =
(ap wB (ap wB^-1 (wf (wA^-1 a))^))^
      rewrite ap_compose, !ap_V.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
ap wB (ap wB^-1 (wf (wA^-1 a))) =
((ap wB (ap wB^-1 (wf (wA^-1 a))))^)^
      apply inverse, inv_V.
  -A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
(eisretr wB (f' (wA (wA^-1 a))))^ @ p =
ap f' (eisretr wA a) apply moveR_Vp.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
p:= ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a): wB (wB^-1 (f' (wA (wA^-1 a)))) = f' a
p =
eisretr wB (f' (wA (wA^-1 a))) @ ap f' (eisretr wA a)
    subst p.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
ap wB (ap wB^-1 (ap f' (eisretr wA a))) @
eisretr wB (f' a) =
eisretr wB (f' (wA (wA^-1 a))) @ ap f' (eisretr wA a)
    rewrite <- ap_compose.A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
ap (fun x : B' => wB (wB^-1 x)) (ap f' (eisretr wA a)) @
eisretr wB (f' a) =
eisretr wB (f' (wA (wA^-1 a))) @ ap f' (eisretr wA a)
    path_via (eisretr wB _ @ ap idmap (ap f' (eisretr wA a))).A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
ap (fun x : B' => wB (wB^-1 x)) (ap f' (eisretr wA a)) @
eisretr wB (f' a) =
eisretr wB (f' (wA (wA^-1 a))) @
ap idmap (ap f' (eisretr wA a))
A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
eisretr wB (f' (wA (wA^-1 a))) @
ap idmap (ap f' (eisretr wA a)) =
eisretr wB (f' (wA (wA^-1 a))) @ ap f' (eisretr wA a)
    +A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
ap (fun x : B' => wB (wB^-1 x)) (ap f' (eisretr wA a)) @
eisretr wB (f' a) =
eisretr wB (f' (wA (wA^-1 a))) @
ap idmap (ap f' (eisretr wA a)) exact (concat_Ap (eisretr wB) _).
    +A, B: Type
f: A -> B
A', B': Type
f': A' -> B'
wA: A <~> A'
wB: B <~> B'
wf: f' o wA == wB o f
a: A'
eisretr wB (f' (wA (wA^-1 a))) @
ap idmap (ap f' (eisretr wA a)) =
eisretr wB (f' (wA (wA^-1 a))) @ ap f' (eisretr wA a) apply ap, ap_idmap.
Defined.