module foundations.retraction where
open import foundations.universe open import foundations.sigma-type open import foundations.homotopy open import foundations.function
private variable ℓ ℓ′ : Level HasRetraction : ∀ {A : Type ℓ} {B : Type ℓ′} (f : A → B) → Type (ℓ ⊔ ℓ′) HasRetraction {A = A} {B} f = Σ[ g ∈ (B → A) ] (g ∘ f ~ idFunction A)
_◅_ : Type ℓ → Type ℓ′ → Type (ℓ ⊔ ℓ′) A ◅ B = Σ (A → B) HasRetraction
A ◅ B
であるとき、A
をB
のレトラクトと呼ぶ。