# Pointed sections of pointed maps

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

Created on 2022-08-12.

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