Timings for BiInv.v

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.

Proof.

  revert bi.

  intros [h g r s].

  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.

Proof.

  intro z.

  lhs_V napply (ap f (sect_retr_homotopic_isbiinv f 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.

Proof.

  intro z.

  lhs napply sect_retr_homotopic_isbiinv.

  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.

Proof.

  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.

Proof.

  destruct bi as [h g r s].

  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.

Proof.

  snapply isequiv_adjointify.

  -

 apply (sect_biinv f).

  -

 apply eisretr_biinv.

  (* We provide proof of eissect, but it gets modified. *)
 

-

 intro a.

    lhs napply sect_retr_homotopic_isbiinv.

    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.

Proof.

  intros [g s r adj].

  exact (Build_IsBiInv _ _ f g g s r).

Defined.

Definition iff_isbiinv_isequiv {A B : Type} (f : A -> B)
  : IsBiInv f <-> IsEquiv f.

Proof.

  split.

  -

 apply isequiv_isbiinv.

  -

 apply isbiinv_isequiv.

Defined.

#[export] Instance ishprop_isbiinv `{Funext} {A B : Type} (f : A -> B)
  : IsHProp (IsBiInv f) | 0.

Proof.

  apply hprop_inhabited_contr.

  intros bif.

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

Proof.

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

Proof.

  nrefine ((issig_equiv A B) oE _ oE (issig_biinv A B)^-1).

  napply (equiv_functor_sigma_id equiv_isbiinv_isequiv).

Defined.

Definition biinv_idmap (A : Type) : BiInv A A.

Proof.

  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.

  Proof.

    intro 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.

  Proof.

    intro 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.

  Proof.

    rapply (equiv_ind e).

    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.

  Proof.

    intro y.

    apply (equiv_inj e').

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

  Proof.

    unfold biinv_compat_pr.

    rewrite equiv_ind_comp.

    apply moveL_pM.

    apply moveL_Mp.

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

  Proof.

    rewrite ap_equiv_inj.

    apply moveL_pM.

    apply moveL_pM.

    reflexivity.

  Defined.

End EquivalenceCompatibility.