From HoTT.Basics Require Import Overture Equivalences Tactics Iff Trunc.From HoTT.Basics Require Import Overture Equivalences Tactics Iff Trunc.
From HoTT.Basics Require Import PathGroupoids.
From HoTT.Types Require Import Sigma Prod Equiv.

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} _.

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

(** If [e] is bi-invertible, then the retraction and the section of [e] are homotopic. *)
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.

(** From a bi-invertible map, we can construct a half-adjoint equivalence in two ways.  Here we take the inverse to be the retraction.  Note that [isequiv_adjointify] modifies the last field provided.  So in order that [eissect_biinv f] not be modified, we first use [isequiv_adjointify] to prove that [retr_biinv f] is an equivalence, and then use [isequiv_inverse] to deduce that [f] is an equivalence. *)
#[export] Instance isequiv_retr_biinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : IsEquiv (retr_biinv f).
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv (retr_biinv f)
Proof.
A, B: Type
f: A -> B
bi: IsBiInv f
IsEquiv (retr_biinv f)
  srefine (isequiv_adjointify (retr_biinv f) f (eissect_biinv f) _); intro b.
A, B: Type
f: A -> B
bi: IsBiInv f
b: B
f (retr_biinv f b) = b
  (* This inlined proof will be modified by [isequiv_adjointify]: *)
  exact (ap f (sect_retr_homotopic_isbiinv f b)^ @ eisretr_biinv f b).
Defined.

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

(** Now we extract the proof generated by [isequiv_adjointify]; it will satisfy the adjoint law [eisadj]. *)
Definition retr_is_sect_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : f o retr_biinv f == idmap
  := eisretr f.

(** [f] is an equivalence in a second way.  Here we take the inverse to be the section.  Again, the last field we provide is modified, and we extract it. *)
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
  srefine (isequiv_adjointify f (sect_biinv f) (eisretr_biinv f) _); intro a.
A, B: Type
f: A -> B
bi: IsBiInv f
a: A
sect_biinv f (f a) = a
  exact (sect_retr_homotopic_isbiinv f (f a) @ eissect_biinv f a).
Defined.

Definition sect_is_retr_isbiinv {A B : Type} (f : A -> B) `{bi : !IsBiInv f}
  : sect_biinv f o f == idmap
  := eissect f (IsEquiv:=isequiv_isbiinv' f).

#[export] Instance isequiv_sect_biinv {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 [g o e == e' o f] 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).
  Context (pe : g o e == e' o f).

  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.

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

  Definition biinv_compat_pr : 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
pe: g o e == e' o f
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
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
pe: g o e == e' o f
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
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
pe: g o e == e' o f
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
forall x : A, r' (g (e x)) = f (r (e x))
    exact (fun a => ap r' (pe a) @ (re' (f a) @ (ap f (re a))^)).
  Defined.

  Definition biinv_compat_ps : 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
pe: g o e == e' o f
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
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
pe: g o e == e' o f
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
s' o g == f o s
    intro b.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
pe: g o e == e' o f
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
b: B
s' (g b) = f (s b)
    apply (equiv_inj e').
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
pe: g o e == e' o f
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
b: B
e' (s' (g b)) = e' (f (s b))
    exact (es' (g b) @ (ap g (es b))^ @ pe (s b)).
  Defined.

  Definition biinv_compat_pre (x : A)
    : re' (f x) = (ap r' (pe x))^ @ biinv_compat_pr (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
pe: g o e == e' o f
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
x: A
re' (f x) = (ap r' (pe x))^ @ biinv_compat_pr (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
pe: g o e == e' o f
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
x: A
re' (f x) = (ap r' (pe x))^ @ biinv_compat_pr (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
pe: g o e == e' o f
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
x: A
re' (f x) =
(ap r' (pe x))^ @
equiv_ind e (fun y : B => r' (g y) = f (r y))
  (fun a : A => ap r' (pe a) @ (re' (f a) @ (ap f (re a))^)) 
  (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
pe: g o e == e' o f
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
x: A
re' (f x) =
(ap r' (pe x))^ @ (ap r' (pe x) @ (re' (f x) @ (ap f (re 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
pe: g o e == e' o f
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
x: A
re' (f x) @ (ap f (re x))^ =
(ap r' (pe x))^ @ (ap r' (pe x) @ (re' (f x) @ (ap f (re x))^))
    apply moveL_Vp.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
pe: g o e == e' o f
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
x: A
ap r' (pe x) @ (re' (f x) @ (ap f (re x))^) =
ap r' (pe x) @ (re' (f x) @ (ap f (re x))^)
    reflexivity.
  Defined.

  Definition biinv_compat_pes (y : B)
    : es' (g y) = ap e' (biinv_compat_ps 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
pe: g o e == e' o f
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
y: B
es' (g y) = ap e' (biinv_compat_ps 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
pe: g o e == e' o f
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
y: B
es' (g y) = ap e' (biinv_compat_ps 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
pe: g o e == e' o f
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
y: B
es' (g y) = es' (g y) @ (ap g (es y))^ @ pe (s 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
pe: g o e == e' o f
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
y: B
es' (g y) @ (ap g (es y))^ =
es' (g y) @ (ap g (es y))^ @ pe (s y) @ (pe (s y))^
    apply moveL_pV.
A, B, C, D: Type
e: BiInv A B
e': BiInv C D
f: A -> C
g: B -> D
pe: g o e == e' o f
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
y: B
es' (g y) @ (ap g (es y))^ @ pe (s y) = es' (g y) @ (ap g (es y))^ @ pe (s y)
    reflexivity.
  Defined.

End EquivalenceCompatibility.