# Descent property of sequential colimits

Content created by Vojtěch Štěpančík.

Created on 2024-04-16.

module synthetic-homotopy-theory.descent-property-sequential-colimits where

Imports
open import elementary-number-theory.natural-numbers

open import foundation.binary-homotopies
open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.univalence
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
open import synthetic-homotopy-theory.descent-data-sequential-colimits
open import synthetic-homotopy-theory.sequential-diagrams
open import synthetic-homotopy-theory.universal-property-sequential-colimits


## Idea

The descent property of sequential colimits characterizes type families over sequential colimits as descent data over the base sequential diagram.

Given a sequential diagram (A, a) and a cocone with vertex X, there is a commuting triangle

          cocone-map
(X → 𝒰) ---------> cocone A 𝒰
\       /
\     /
\   /
∨ ∨
descent-data A .


From univalence it follows that the right map is an equivalence. If X is a colimit of A, then we have that the top map is an equivalence, which imples that the left map is an equivalence.

## Theorem

module _
{l1 : Level} {A : sequential-diagram l1}
where

equiv-descent-data-cocone-sequential-diagram :
{l2 : Level} →
cocone-sequential-diagram A (UU l2) ≃
descent-data-sequential-colimit A l2
equiv-descent-data-cocone-sequential-diagram =
equiv-tot
( λ B →
equiv-Π-equiv-family
( λ n → equiv-Π-equiv-family (λ a → equiv-univalence)))

descent-data-cocone-sequential-diagram :
{l2 : Level} →
cocone-sequential-diagram A (UU l2) →
descent-data-sequential-colimit A l2
descent-data-cocone-sequential-diagram =
map-equiv equiv-descent-data-cocone-sequential-diagram

is-equiv-descent-data-cocone-sequential-diagram :
{l2 : Level} → is-equiv (descent-data-cocone-sequential-diagram {l2})
is-equiv-descent-data-cocone-sequential-diagram =
is-equiv-map-equiv equiv-descent-data-cocone-sequential-diagram

module _
{l1 l2 : Level} {A : sequential-diagram l1}
{X : UU l2} (c : cocone-sequential-diagram A X)
where

triangle-descent-data-family-cocone-sequential-diagram :
{l3 : Level} →
coherence-triangle-maps
( descent-data-family-cocone-sequential-diagram c)
( descent-data-cocone-sequential-diagram)
( cocone-map-sequential-diagram c {Y = UU l3})
triangle-descent-data-family-cocone-sequential-diagram P =
eq-pair-eq-fiber
( eq-binary-htpy _ _
( λ n a →
inv
( compute-equiv-eq-ap
( coherence-cocone-sequential-diagram c n a))))

module _
{l1 l2 l3 : Level} {A : sequential-diagram l1}
{X : UU l2} {c : cocone-sequential-diagram A X}
(up-c : universal-property-sequential-colimit c)
where

is-equiv-descent-data-family-cocone-sequential-diagram :
is-equiv (descent-data-family-cocone-sequential-diagram c {l3})
is-equiv-descent-data-family-cocone-sequential-diagram =
is-equiv-left-map-triangle
( descent-data-family-cocone-sequential-diagram c)
( descent-data-cocone-sequential-diagram)
( cocone-map-sequential-diagram c)
( triangle-descent-data-family-cocone-sequential-diagram c)
( up-c (UU l3))
( is-equiv-descent-data-cocone-sequential-diagram)

equiv-descent-data-family-cocone-sequential-diagram :
(X → UU l3) ≃ descent-data-sequential-colimit A l3
pr1 equiv-descent-data-family-cocone-sequential-diagram =
descent-data-family-cocone-sequential-diagram c
pr2 equiv-descent-data-family-cocone-sequential-diagram =
is-equiv-descent-data-family-cocone-sequential-diagram

family-cocone-descent-data-sequential-colimit :
descent-data-sequential-colimit A l3 → (X → UU l3)
family-cocone-descent-data-sequential-colimit =
map-inv-equiv
( equiv-descent-data-family-cocone-sequential-diagram)