Library HoTT.Equiv.BiInv


Require Import HoTT.Basics HoTT.Types.

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.

Definition BiInv `(f : A B) : Type
  := {g : B A & Sect f g} × {h : B A & Sect h f}.

It seems that the easiest way to show that bi-invertibility is equivalent to being an equivalence is also to show that both are h-props and that they are logically equivalent.

Definition isequiv_biinv `(f : A B)
  : BiInv f IsEquiv f.
Proof.
  intros [[g s] [h r]].
  exact (isequiv_adjointify f g
    (fun xap f (ap g (r x)^ @ s (h x)) @ r x)
    s).
Defined.

Global Instance isprop_biinv `{Funext} `(f : A B) : IsHProp (BiInv f) | 0.
Proof.
  apply hprop_inhabited_contr.
  intros bif; pose (fe := isequiv_biinv f bif).
  apply @contr_prod.
  - by apply contr_retr_equiv.
  - by apply contr_sect_equiv.
Defined.

Definition equiv_biinv_isequiv `{Funext} `(f : A B)
  : BiInv f <~> IsEquiv f.
Proof.
  apply equiv_iff_hprop.
  - by apply isequiv_biinv.
  - intros ?. split.
    + by (f^-1); apply eissect.
    + by (f^-1); apply eisretr.
Defined.