Pointed sections of pointed maps

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

Created on 2022-08-12.
Last modified on 2024-03-13.

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

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

Idea

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.

Definitions

The predicate of being a pointed section of a pointed map

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  is-pointed-section : (B →∗ A) → UU l2
  is-pointed-section g = f ∘∗ g ~∗ id-pointed-map

The type of pointed sections of a pointed map

module _
  {l1 l2 : Level} {A : Pointed-Type l1} {B : Pointed-Type l2} (f : A →∗ B)
  where

  pointed-section : UU (l1 ⊔ l2)
  pointed-section =
    Σ (B →∗ A) (is-pointed-section f)

  module _
    (s : pointed-section)
    where

    pointed-map-pointed-section : B →∗ A
    pointed-map-pointed-section = pr1 s

    is-pointed-section-pointed-section :
      is-pointed-section f pointed-map-pointed-section
    is-pointed-section-pointed-section = pr2 s

    map-pointed-section : type-Pointed-Type B → type-Pointed-Type A
    map-pointed-section = map-pointed-map pointed-map-pointed-section

    preserves-point-pointed-map-pointed-section :
      map-pointed-section (point-Pointed-Type B) ＝ point-Pointed-Type A
    preserves-point-pointed-map-pointed-section =
      preserves-point-pointed-map pointed-map-pointed-section

    is-section-pointed-section :
      is-section (map-pointed-map f) map-pointed-section
    is-section-pointed-section =
      htpy-pointed-htpy is-pointed-section-pointed-section

    section-pointed-section : section (map-pointed-map f)
    pr1 section-pointed-section = map-pointed-section
    pr2 section-pointed-section = is-section-pointed-section

    coherence-point-is-section-pointed-section :
      coherence-point-unpointed-htpy-pointed-Π
        ( f ∘∗ pointed-map-pointed-section)
        ( id-pointed-map)
        ( is-section-pointed-section)
    coherence-point-is-section-pointed-section =
      coherence-point-pointed-htpy is-pointed-section-pointed-section

Recent changes