Pointed sections of pointed maps

Content created by Jonathan Prieto-Cubides, Fredrik Bakke and Egbert Rijke.

Created on 2022-08-12.
Last modified on 2023-05-03.

module structured-types.pointed-sections where
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import structured-types.pointed-homotopies
open import structured-types.pointed-maps
open import structured-types.pointed-types


A pointed section of a pointed map f : A →∗ B consists of a pointed map g : B →∗ A equipped with a pointed homotopy H : (f ∘∗ g) ~∗ id.

pointed-section-Pointed-Type :
  {l1 l2 : Level} (A : Pointed-Type l1) (B : Pointed-Type l2) 
  (A →∗ B)  UU (l1  l2)
pointed-section-Pointed-Type A B f =
  Σ ( B →∗ A)
    ( λ g  (f ∘∗ g) ~∗ id-pointed-map)

Recent changes