Home

準逆

module foundations.quasi-inverse where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.function
open import foundations.homotopy
open import foundations.sigma-type

private variable
  ℓ ℓ′ : Level

record QuasiInv {A : Type ℓ} {B : Type ℓ′} (f : A → B) : Type (ℓ ⊔ ℓ′) where
  field
    g : B → A
    linv : g ∘ f ~ idFunction A
    rinv : f ∘ g ~ idFunction B

_≅_ : Type ℓ → Type ℓ′ → Type (ℓ ⊔ ℓ′)
A ≅ B = Σ (A → B) QuasiInv