# Sections

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-02-04.
Last modified on 2024-04-25.

module foundation-core.sections where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies


## Idea

A section of a map f : A → B consists of a map s : B → A equipped with a homotopy f ∘ s ~ id. In other words, a section of a map f is a right inverse of f. For example, every dependent function induces a section of the projection map.

Note that unlike retractions, sections don't induce sections on identity types. A map f equipped with a section such that all actions on identifications ap f : (x ＝ y) → (f x ＝ f y) come equipped with sections is called a path split map. The condition of being path split is equivalent to being an equivalence.

## Definition

### The predicate of being a section of a map

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

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


### The type of sections of a map

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
where

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

map-section : section → B → A
map-section = pr1

is-section-map-section : (s : section) → is-section f (map-section s)
is-section-map-section = pr2


## Properties

### If g ∘ h has a section then g has a section

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(g : B → X) (h : A → B) (s : section (g ∘ h))
where

map-section-left-factor : X → B
map-section-left-factor = h ∘ map-section (g ∘ h) s

is-section-map-section-left-factor : is-section g map-section-left-factor
is-section-map-section-left-factor = pr2 s

section-left-factor : section g
pr1 section-left-factor = map-section-left-factor
pr2 section-left-factor = is-section-map-section-left-factor


### Composites of sections are sections of composites

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(g : B → X) (h : A → B) (t : section h) (s : section g)
where

map-section-comp : X → A
map-section-comp = map-section h t ∘ map-section g s

is-section-map-section-comp :
is-section (g ∘ h) map-section-comp
is-section-map-section-comp =
( g ·l (is-section-map-section h t ·r map-section g s)) ∙h
( is-section-map-section g s)

section-comp : section (g ∘ h)
pr1 section-comp = map-section-comp
pr2 section-comp = is-section-map-section-comp


### In a commuting triangle g ∘ h ~ f, any section of f induces a section of g

In a commuting triangle of the form

       h
A ------> B
\       /
f\     /g
\   /
∨ ∨
X,


if s : X → A is a section of the map f on the left, then h ∘ s is a section of the map g on the right.

Note: In this file we are unable to use the definition of commuting triangles, because that would result in a cyclic module dependency.

We state two versions: one with a homotopy g ∘ h ~ f, and the other with a homotopy f ~ g ∘ h. Our convention for commuting triangles of maps is that the homotopy is specified in the second way, i.e., as f ~ g ∘ h.

#### First version, with the commutativity of the triangle opposite to our convention

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (H' : g ∘ h ~ f) (s : section f)
where

map-section-right-map-triangle' : X → B
map-section-right-map-triangle' = h ∘ map-section f s

is-section-map-section-right-map-triangle' :
is-section g map-section-right-map-triangle'
is-section-map-section-right-map-triangle' =
(H' ·r map-section f s) ∙h is-section-map-section f s

section-right-map-triangle' : section g
pr1 section-right-map-triangle' =
map-section-right-map-triangle'
pr2 section-right-map-triangle' =
is-section-map-section-right-map-triangle'


#### Second version, with the commutativity of the triangle accoring to our convention

We state the same result as the previous result, only with the homotopy witnessing the commutativity of the triangle inverted.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h) (s : section f)
where

map-section-right-map-triangle : X → B
map-section-right-map-triangle =
map-section-right-map-triangle' f g h (inv-htpy H) s

is-section-map-section-right-map-triangle :
is-section g map-section-right-map-triangle
is-section-map-section-right-map-triangle =
is-section-map-section-right-map-triangle' f g h (inv-htpy H) s

section-right-map-triangle : section g
section-right-map-triangle =
section-right-map-triangle' f g h (inv-htpy H) s


### Composites of sections in commuting triangles are sections

In a commuting triangle of the form

       h
A ------> B
\       /
f\     /g
\   /
∨ ∨
X,


if s : X → B is a section of the map g on the right and t : B → A is a section of the map h on top, then t ∘ s is a section of the map f on the left.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
(f : A → X) (g : B → X) (h : A → B) (H : f ~ g ∘ h) (t : section h)
where

map-section-left-map-triangle : section g → X → A
map-section-left-map-triangle s = map-section-comp g h t s

is-section-map-section-left-map-triangle :
(s : section g) → is-section f (map-section-left-map-triangle s)
is-section-map-section-left-map-triangle s =
( H ·r map-section-comp g h t s) ∙h
( is-section-map-section-comp g h t s)

section-left-map-triangle : section g → section f
pr1 (section-left-map-triangle s) = map-section-left-map-triangle s
pr2 (section-left-map-triangle s) = is-section-map-section-left-map-triangle s