Home

両側可逆写像

module foundations.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

private variable ℓ ℓ′ : Level

biinv : ∀ {A : Type ℓ} {B : Type ℓ′} → (A → B) → Type (ℓ ⊔ ℓ′)
biinv f = HasRetraction f × HasSection f

_≃_ : Type ℓ → Type ℓ′ → Type (ℓ ⊔ ℓ′)
A ≃ B = Σ (A → B) biinv