# Library HoTT.Equiv.BiInv

# Bi-invertible maps

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 x ⇒ ap 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.