Home

quasi-inverseからbi-invertible mapへ

module foundations.quasi-inverse-to-bi-invertible-map where
Imports 
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

private variable
  ℓ : Level
  A B : Type ℓ

QuasiInv⇒biinv : ∀ {f : A → B} → QuasiInv f → biinv f
QuasiInv⇒biinv qinv = (g , linv) , (g , rinv)
  where open QuasiInv qinv