bi-invertible mapからquasi-inverseへ

module foundations.bi-invertible-map-to-quasi-inverse where

open import foundations.universe
open import foundations.sigma-type
open import foundations.homotopy
open import foundations.function
open import foundations.product-type
open import foundations.retraction
open import foundations.section
open import foundations.quasi-inverse
open import foundations.bi-invertible-map
open import foundations.identity-type
open import foundations.functions-are-functors
open import foundations.groupoid-laws

private variable
  ℓ : Level
  A B : Type ℓ

biinv⇒QuasiInv : ∀ {f : A → B} → biinv f → QuasiInv f
biinv⇒QuasiInv {f = f} ((r , isR) , (s , isS)) = record
  { g = r
  ; linv = isR
  ; rinv = λ x → ap f (H x) ∙ isS x
  }
  where
    H : r ~ s
    H x = ap r (sym (isS x)) ∙ isR (s x)