Home

レトラクション

module foundations.retraction where
Imports 
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のレトラクトと呼ぶ。