module foundations.section where
open import foundations.universe open import foundations.sigma-type open import foundations.homotopy open import foundations.function
private variable ℓ ℓ′ : Level
HasSection : ∀ {A : Type ℓ} {B : Type ℓ′} (f : A → B) → Type (ℓ ⊔ ℓ′)
HasSection {A = A} {B} f = Σ[ g ∈ (B → A) ] (f ∘ g ~ idFunction B)