Require Import HoTT.Basics Types.Prod Types.Equiv Types.Sigma Types.Universe.Require Import HoTT.Basics Types.Prod Types.Equiv Types.Sigma Types.Universe.

Local Open Scope path_scope.
Generalizable Variables A B f.

(** * Bi-invertible maps *)

(** A map is "bi-invertible" if it has both a section and a retraction, not necessarily the same.  This definition of equivalence was proposed by Andre Joyal. *)

Class IsBiInv {A B : Type} (e : A -> B) := {
  sect_biinv : B -> A ;
  retr_biinv : B -> A ;
  eisretr_biinv : e o sect_biinv == idmap ;
  eissect_biinv : retr_biinv o e == idmap ;
}.

Arguments sect_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments retr_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments eisretr_biinv {A B}%_type_scope e%_function_scope {_} _.
Arguments eissect_biinv {A B}%_type_scope e%_function_scope {_} _.

Record BiInv A B := {
  biinv_fun : A -> B ;
  biinv_isbiinv :: IsBiInv biinv_fun
}.

Coercion biinv_fun : BiInv >-> Funclass.

Arguments biinv_fun {A B} _ _.
Arguments biinv_isbiinv {A B} _.

(** If [e] is bi-invertible, then the retraction and the section of [e] are equal. *)
Definition sect_retr_homotopic_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : sect_biinv f == retr_biinv f.
A, B: Type
f: A -> B
bi: IsBiInv f
sect_biinv f == retr_biinv f
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
sect_biinv f == retr_biinv f
  revert bi.
A, B: Type
f: A -> B
forall bi : IsBiInv f, sect_biinv f == retr_biinv f
  intros [h g r s].
A, B: Type
f: A -> B
h, g: B -> A
r: (fun x : B => f (h x)) == idmap
s: (fun x : A => g (f x)) == idmap
sect_biinv f == retr_biinv f
  exact (fun y => (s (h y))^ @ ap g (r y)).
Defined.

Definition retr_is_sect_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : f o retr_biinv f == idmap.
A, B: Type
f: A -> B
bi: IsBiInv f
f o retr_biinv f == idmap
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
f o retr_biinv f == idmap
  intro z.
A, B: Type
f: A -> B
bi: IsBiInv f
z: B
f (retr_biinv f z) = z
  lhs_V napply (ap f (sect_retr_homotopic_isbiinv f z)).
A, B: Type
f: A -> B
bi: IsBiInv f
z: B
f (sect_biinv f z) = z
  apply eisretr_biinv.
Defined.

Definition sect_is_retr_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : sect_biinv f o f == idmap.
A, B: Type
f: A -> B
bi: IsBiInv f
sect_biinv f o f == idmap
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
sect_biinv f o f == idmap
  intro z.
A, B: Type
f: A -> B
bi: IsBiInv f
z: A
sect_biinv f (f z) = z
  lhs napply sect_retr_homotopic_isbiinv.
A, B: Type
f: A -> B
bi: IsBiInv f
z: A
retr_biinv f (f z) = z
  apply eissect_biinv.
Defined.

(** The record is equivalent to a product type.  This is used below in a 'product of contractible types is contractible' argument. *)
Definition prod_isbiinv (A B : Type) `{f : A -> B}
  : {g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap} <~> IsBiInv f.
A, B: Type
f: A -> B
{g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap} <~> IsBiInv f
Proof.
A, B: Type
f: A -> B
{g : B -> A & g o f == idmap} * {h : B -> A & f o h == idmap} <~> IsBiInv f
  make_equiv.
Defined.

Definition issig_biinv (A B : Type) : {f : A -> B & IsBiInv f} <~> BiInv A B
  := ltac:(issig).

(** From a bi-invertible map, we can construct a half-adjoint equivalence in two ways.  Here we take the inverse to be the retraction. *)
#[export] Instance isequiv_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : IsEquiv f.
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv f
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv f
  destruct bi as [h g r s].
A, B: Type
f: A -> B
h, g: B -> A
r: (fun x : B => f (h x)) == idmap
s: (fun x : A => g (f x)) == idmap
IsEquiv f
  exact (isequiv_adjointify f g
    (fun x => ap f (ap g (r x)^ @ s (h x)) @ r x)
    s).
Defined.

#[export] Instance isequiv_isbiinv_retr {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : IsEquiv (retr_biinv f)
  := isequiv_inverse f.

(** Here we take the inverse to be the section. *)
Definition isequiv_isbiinv' {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : IsEquiv f.
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv f
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv f
  snapply isequiv_adjointify.
A, B: Type
f: A -> B
bi: IsBiInv f
B -> A
A, B: Type
f: A -> B
bi: IsBiInv f
f o ?g == idmap
A, B: Type
f: A -> B
bi: IsBiInv f
?g o f == idmap
  -
A, B: Type
f: A -> B
bi: IsBiInv f
B -> A apply (sect_biinv f).
  -
A, B: Type
f: A -> B
bi: IsBiInv f
f o sect_biinv f == idmap apply eisretr_biinv.  (* We provide proof of eissect, but it gets modified. *)
  -
A, B: Type
f: A -> B
bi: IsBiInv f
sect_biinv f o f == idmap intro a.
A, B: Type
f: A -> B
bi: IsBiInv f
a: A
sect_biinv f (f a) = a
    lhs napply sect_retr_homotopic_isbiinv.
A, B: Type
f: A -> B
bi: IsBiInv f
a: A
retr_biinv f (f a) = a
    apply eissect_biinv.
Defined.

#[export] Instance isequiv_isbiinv_sect {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : IsEquiv (sect_biinv f)
  := isequiv_inverse f (feq:=isequiv_isbiinv' f).

Definition isbiinv_isequiv {A B : Type} (f : A -> B)
  : IsEquiv f -> IsBiInv f.
A, B: Type
f: A -> B
IsEquiv f -> IsBiInv f
Proof.
A, B: Type
f: A -> B
IsEquiv f -> IsBiInv f
  intros [g s r adj].
A, B: Type
f: A -> B
g: B -> A
s: (fun x : B => f (g x)) == idmap
r: (fun x : A => g (f x)) == idmap
adj: forall x : A, s (f x) = ap f (r x)
IsBiInv f
  exact (Build_IsBiInv _ _ f g g s r).
Defined.

Definition iff_isbiinv_isequiv {A B : Type} (f : A -> B)
  : IsBiInv f <-> IsEquiv f.
A, B: Type
f: A -> B
IsBiInv f <-> IsEquiv f
Proof.
A, B: Type
f: A -> B
IsBiInv f <-> IsEquiv f
  split.
A, B: Type
f: A -> B
IsBiInv f -> IsEquiv f
A, B: Type
f: A -> B
IsEquiv f -> IsBiInv f
  -
A, B: Type
f: A -> B
IsBiInv f -> IsEquiv f apply isequiv_isbiinv.
  -
A, B: Type
f: A -> B
IsEquiv f -> IsBiInv f apply isbiinv_isequiv.
Defined.

#[export] Instance ishprop_isbiinv `{Funext} {A B : Type} (f : A -> B)
  : IsHProp (IsBiInv f) | 0.
H: Funext
A, B: Type
f: A -> B
IsHProp (IsBiInv f)
Proof.
H: Funext
A, B: Type
f: A -> B
IsHProp (IsBiInv f)
  apply hprop_inhabited_contr.
H: Funext
A, B: Type
f: A -> B
IsBiInv f -> Contr (IsBiInv f)
  intros bif.
H: Funext
A, B: Type
f: A -> B
bif: IsBiInv f
Contr (IsBiInv f)
  (* This uses implicitly that the product of contractible types is contractible: *)
  srapply (contr_equiv' _ (prod_isbiinv A B)).
Defined.

Definition equiv_isbiinv_isequiv `{Funext} {A B : Type} (f : A -> B)
  : IsBiInv f <~> IsEquiv f.
H: Funext
A, B: Type
f: A -> B
IsBiInv f <~> IsEquiv f
Proof.
H: Funext
A, B: Type
f: A -> B
IsBiInv f <~> IsEquiv f
  apply equiv_iff_hprop_uncurried, iff_isbiinv_isequiv.
Defined.

(** Some lemmas to send equivalences and biinvertible maps back and forth. *)

Definition equiv_biinv A B (f : BiInv A B) : A <~> B
  := Build_Equiv A B f _.

Definition biinv_equiv A B (e : A <~> B) : BiInv A B
  := Build_BiInv A B e (isbiinv_isequiv e (equiv_isequiv e)).

Definition equiv_biinv_equiv `{Funext} A B
  : BiInv A B <~> (A <~> B).
H: Funext
A, B: Type
BiInv A B <~> (A <~> B)
Proof.
H: Funext
A, B: Type
BiInv A B <~> (A <~> B)
  nrefine ((issig_equiv A B) oE _ oE (issig_biinv A B)^-1).
H: Funext
A, B: Type
{f : A -> B & IsBiInv f} <~> {f : A -> B & IsEquiv f}
  napply (equiv_functor_sigma_id equiv_isbiinv_isequiv).
Defined.

Definition biinv_idmap (A : Type) : BiInv A A.
A: Type
BiInv A A
Proof.
A: Type
BiInv A A
  by nrefine (Build_BiInv A A idmap (Build_IsBiInv A A idmap idmap idmap _ _)).
Defined.

(** Assume we have a commutative square [e' o f == g o e] in which [e] and [e'] are bi-invertible.  Then [f] and [g] also commute with the retractions and sections, and the homotopies in these new squares each satisfy a coherence condition. *)

Section EquivalenceCompatibility.

  Context {A B C D : Type}.
  Context (e : BiInv A B) (e' : BiInv C D) (f : A -> C) (g : B -> D).

  Let s := sect_biinv e.
  Let r := retr_biinv e.
  Let re := eissect_biinv e : r o e == idmap.
  Let es := eisretr_biinv e : e o s == idmap.
  Let s' := sect_biinv e'.
  Let r' := retr_biinv e'.
  Let re' := eissect_biinv e' : r' o e' == idmap.
  Let es' := eisretr_biinv e' : e' o s' == idmap.

  Definition helper_r (pe : e' o f == g o e) : r' o g o e == f o r o e.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
r' o g o e == f o r o e
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
r' o g o e == f o r o e
    intro x.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
x: A
r' (g (e x)) = f (r (e x))
    exact ((ap r' (pe x))^ @ (re' (f x) @ (ap f (re x))^)).
  Defined.

  Definition helper_s (pe : e' o f == g o e) : e' o s' o g == e' o f o s.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
e' o s' o g == e' o f o s
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
e' o s' o g == e' o f o s
    intro y.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: e' o f == g o e
y: B
e' (s' (g y)) = e' (f (s y))
    exact (es' (g y) @ (ap g (es y))^ @ (pe (s y))^).
  Defined.

  (** The following lemmas express the coherence conditions mentioned above. *)

  Definition biinv_compat_pr (pe : forall (x : A), e' (f x) = g (e x))
    : r' o g == f o r.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
r' o g == f o r
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
r' o g == f o r
    rapply (equiv_ind e).
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
forall x : A, r' (g (e x)) = f (r (e x))
    apply (helper_r pe).
  Defined.

  Definition biinv_compat_ps (pe : forall (x : A), e' (f x) = g (e x))
    : s' o g == f o s.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
s' o g == f o s
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
s' o g == f o s
    intro y.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
s' (g y) = f (s y)
    apply (equiv_inj e').
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
e' (s' (g y)) = e' (f (s y))
    apply (helper_s pe).
  Defined.

  Definition biinv_compat_pre (pe : forall (x : A), e' (f x) = g (e x)) (x : A)
    : re' (f x) = ap r' (pe x) @ (biinv_compat_pr pe) (e x) @ ap f (re x).
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
re' (f x) = (ap r' (pe x) @ biinv_compat_pr pe (e x)) @ ap f (re x)
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
re' (f x) = (ap r' (pe x) @ biinv_compat_pr pe (e x)) @ ap f (re x)
    unfold biinv_compat_pr.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
re' (f x) =
(ap r' (pe x) @
 equiv_ind e (fun y : B => r' (g y) = f (r y)) (helper_r pe) (e x)) @
ap f (re x)
    rewrite equiv_ind_comp.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
re' (f x) = (ap r' (pe x) @ helper_r pe x) @ ap f (re x)
    apply moveL_pM.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
re' (f x) @ (ap f (re x))^ = ap r' (pe x) @ helper_r pe x
    apply moveL_Mp.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x0 : A, e' (f x0) = g (e x0)
x: A
(ap r' (pe x))^ @ (re' (f x) @ (ap f (re x))^) = helper_r pe x
    reflexivity.
  Defined.

  Definition biinv_compat_pes (pe : forall (x : A), e' (f x) = g (e x)) (y : B)
    : es' (g y) = ap e' ((biinv_compat_ps pe) y) @ pe (s y) @ ap g (es y).
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
es' (g y) = (ap e' (biinv_compat_ps pe y) @ pe (s y)) @ ap g (es y)
  Proof.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
es' (g y) = (ap e' (biinv_compat_ps pe y) @ pe (s y)) @ ap g (es y)
    rewrite ap_equiv_inj.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
es' (g y) = (helper_s pe y @ pe (s y)) @ ap g (es y)
    apply moveL_pM.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
es' (g y) @ (ap g (es y))^ = helper_s pe y @ pe (s y)
    apply moveL_pM.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
s:= sect_biinv e: B -> A
r:= retr_biinv e: B -> A
re:= eissect_biinv e: r o e == idmap
es:= eisretr_biinv e: e o s == idmap
s':= sect_biinv e': D -> C
r':= retr_biinv e': D -> C
re':= eissect_biinv e': r' o e' == idmap
es':= eisretr_biinv e': e' o s' == idmap
pe: forall x : A, e' (f x) = g (e x)
y: B
(es' (g y) @ (ap g (es y))^) @ (pe (s y))^ = helper_s pe y
    reflexivity.
  Defined.

End EquivalenceCompatibility.