# Descent data for pushouts

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

Created on 2024-05-31.

module synthetic-homotopy-theory.descent-data-pushouts where

Imports
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.span-diagrams
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans


## Idea

Descent data for the pushout of a span diagram 𝒮

     f     g
A <-- S --> B


is a triple (PA, PB, PS), where PA : A → 𝒰 is a type family over A, PB : B → 𝒰 is a type family over B, and PS is a family of equivalences

  PS : (s : S) → PA (f a) ≃ PB (g a).


In descent-property-pushouts, we show that this is exactly the data one needs to "glue together" a type family P : X → 𝒰 over the pushout X of 𝒮.

The identity type of descent data is characterized in equivalences-descent-data-pushouts.

It may not be immediately clear why "descent data" is an appropriate name for this concept, because there is no apparent downward motion. Traditionally, descent is studied in the context of a collection of objects Xᵢ covering a single object X, and local structure on the individual Xᵢ's descending onto X, collecting into a global structure, given that the pieces are appropriately compatible on any "overlaps". A pushout of 𝒮 is covered by A and B, and the overlaps are encoded in f and g. Then structure on A and B, expressed as type families PA and PB, "descends" to a structure on X (a type family over X). Two elements "overlap" in X if there is an identification between them coming from S, and the gluing/compatibility condition exactly requires the local structure of PA and PB to agree on such elements, i.e. asks for an equivalence PA(fs) ≃ PB(gs).

## Definitions

### Descent data for pushouts

module _
{l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3)
where

descent-data-pushout : (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4)
descent-data-pushout l =
Σ ( domain-span-diagram 𝒮 → UU l)
( λ PA →
Σ ( codomain-span-diagram 𝒮 → UU l)
( λ PB →
(s : spanning-type-span-diagram 𝒮) →
PA (left-map-span-diagram 𝒮 s) ≃ PB (right-map-span-diagram 𝒮 s)))


### Components of descent data for pushouts

module _
{l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
(P : descent-data-pushout 𝒮 l4)
where

left-family-descent-data-pushout : domain-span-diagram 𝒮 → UU l4
left-family-descent-data-pushout = pr1 P

right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l4
right-family-descent-data-pushout = pr1 (pr2 P)

equiv-family-descent-data-pushout :
(s : spanning-type-span-diagram 𝒮) →
left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃
right-family-descent-data-pushout (right-map-span-diagram 𝒮 s)
equiv-family-descent-data-pushout = pr2 (pr2 P)

map-family-descent-data-pushout :
(s : spanning-type-span-diagram 𝒮) →
left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) →
right-family-descent-data-pushout (right-map-span-diagram 𝒮 s)
map-family-descent-data-pushout s =
map-equiv (equiv-family-descent-data-pushout s)

is-equiv-map-family-descent-data-pushout :
(s : spanning-type-span-diagram 𝒮) →
is-equiv (map-family-descent-data-pushout s)
is-equiv-map-family-descent-data-pushout s =
is-equiv-map-equiv (equiv-family-descent-data-pushout s)


### Descent data induced by families over cocones

Given a cocone

        g
S -----> B
|        |
f |        | j
∨        ∨
A -----> X
i


and a family P : X → 𝒰, we can obtain PA and PB by precomposing with i and j, respectively. Then to produce an equivalence PS s : P (ifs) ≃ P (jgs), we transport along the coherence H s : ifs = jgs, which is an equivalence.

module _
{l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
{X : UU l4} (c : cocone-span-diagram 𝒮 X)
where

descent-data-family-cocone-span-diagram :
{l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5
pr1 (descent-data-family-cocone-span-diagram P) =
P ∘ horizontal-map-cocone _ _ c
pr1 (pr2 (descent-data-family-cocone-span-diagram P)) =
P ∘ vertical-map-cocone _ _ c
pr2 (pr2 (descent-data-family-cocone-span-diagram P)) s =
equiv-tr P (coherence-square-cocone _ _ c s)