# Families with descent data for pushouts

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

Created on 2024-05-31.

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

Imports
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.span-diagrams
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.descent-data-pushouts
open import synthetic-homotopy-theory.equivalences-descent-data-pushouts


## Idea

In descent-property-pushouts we show that given descent data (PA, PB, PS) over a span diagram 𝒮, there is a unique type family P over its pushout such that its induced descent data is equivalent to (PA, PB, PS). When stating theorems, it is sometimes useful to parameterize over a user-provided type family, descent data, and the appropriate equivalence, even though we technically can contract away the equivalence and either of the endpoints. We call such a triple (P, (PA, PB, PS), e) a family with descent data, and denote it P ≈ (PA, PB, PS).

## Definitions

### Type families over a cocone equipped with corresponding descent data for pushouts

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

family-with-descent-data-pushout :
(l5 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ lsuc l5)
family-with-descent-data-pushout l5 =
Σ ( X → UU l5)
( λ P →
Σ ( descent-data-pushout 𝒮 l5)
( λ Q →
equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c P)
( Q)))


### Components of a family with corresponding descent data

module _
{l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
{X : UU l4} {c : cocone-span-diagram 𝒮 X}
(P : family-with-descent-data-pushout c l5)
where

family-cocone-family-with-descent-data-pushout : X → UU l5
family-cocone-family-with-descent-data-pushout = pr1 P

descent-data-family-with-descent-data-pushout : descent-data-pushout 𝒮 l5
descent-data-family-with-descent-data-pushout = pr1 (pr2 P)

left-family-family-with-descent-data-pushout :
domain-span-diagram 𝒮 → UU l5
left-family-family-with-descent-data-pushout =
left-family-descent-data-pushout
( descent-data-family-with-descent-data-pushout)

right-family-family-with-descent-data-pushout :
codomain-span-diagram 𝒮 → UU l5
right-family-family-with-descent-data-pushout =
right-family-descent-data-pushout
( descent-data-family-with-descent-data-pushout)

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

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

equiv-descent-data-family-with-descent-data-pushout :
equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
equiv-descent-data-family-with-descent-data-pushout = pr2 (pr2 P)

inv-equiv-descent-data-family-with-descent-data-pushout :
equiv-descent-data-pushout
( descent-data-family-with-descent-data-pushout)
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
inv-equiv-descent-data-family-with-descent-data-pushout =
inv-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

left-equiv-family-with-descent-data-pushout :
(a : domain-span-diagram 𝒮) →
family-cocone-family-with-descent-data-pushout
( horizontal-map-cocone _ _ c a) ≃
left-family-family-with-descent-data-pushout a
left-equiv-family-with-descent-data-pushout =
left-equiv-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

left-map-family-with-descent-data-pushout :
(a : domain-span-diagram 𝒮) →
family-cocone-family-with-descent-data-pushout
( horizontal-map-cocone _ _ c a) →
left-family-family-with-descent-data-pushout a
left-map-family-with-descent-data-pushout =
left-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

is-equiv-left-map-family-with-descent-data-pushout :
(a : domain-span-diagram 𝒮) →
is-equiv (left-map-family-with-descent-data-pushout a)
is-equiv-left-map-family-with-descent-data-pushout =
is-equiv-left-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

inv-left-map-family-with-descent-data-pushout :
(a : domain-span-diagram 𝒮) →
left-family-family-with-descent-data-pushout a →
family-cocone-family-with-descent-data-pushout
( horizontal-map-cocone _ _ c a)
inv-left-map-family-with-descent-data-pushout =
inv-left-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

right-equiv-family-with-descent-data-pushout :
(b : codomain-span-diagram 𝒮) →
family-cocone-family-with-descent-data-pushout
( vertical-map-cocone _ _ c b) ≃
right-family-family-with-descent-data-pushout b
right-equiv-family-with-descent-data-pushout =
right-equiv-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

right-map-family-with-descent-data-pushout :
(b : codomain-span-diagram 𝒮) →
family-cocone-family-with-descent-data-pushout
( vertical-map-cocone _ _ c b) →
right-family-family-with-descent-data-pushout b
right-map-family-with-descent-data-pushout =
right-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

is-equiv-right-map-family-with-descent-data-pushout :
(b : codomain-span-diagram 𝒮) →
is-equiv (right-map-family-with-descent-data-pushout b)
is-equiv-right-map-family-with-descent-data-pushout =
is-equiv-right-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

inv-right-map-family-with-descent-data-pushout :
(b : codomain-span-diagram 𝒮) →
right-family-family-with-descent-data-pushout b →
family-cocone-family-with-descent-data-pushout
( vertical-map-cocone _ _ c b)
inv-right-map-family-with-descent-data-pushout =
inv-right-map-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)

coherence-family-with-descent-data-pushout :
(s : spanning-type-span-diagram 𝒮) →
coherence-square-maps
( left-map-family-with-descent-data-pushout
( left-map-span-diagram 𝒮 s))
( tr
( family-cocone-family-with-descent-data-pushout)
( coherence-square-cocone _ _ c s))
( map-family-family-with-descent-data-pushout s)
( right-map-family-with-descent-data-pushout
( right-map-span-diagram 𝒮 s))
coherence-family-with-descent-data-pushout =
coherence-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c
( family-cocone-family-with-descent-data-pushout))
( descent-data-family-with-descent-data-pushout)
( equiv-descent-data-family-with-descent-data-pushout)


### Type family together with its induced descent data

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

family-with-descent-data-pushout-family-cocone :
{l5 : Level} (P : X → UU l5) →
family-with-descent-data-pushout c l5
pr1 (family-with-descent-data-pushout-family-cocone P) = P
pr1 (pr2 (family-with-descent-data-pushout-family-cocone P)) =
descent-data-family-cocone-span-diagram c P
pr2 (pr2 (family-with-descent-data-pushout-family-cocone P)) =
id-equiv-descent-data-pushout
( descent-data-family-cocone-span-diagram c P)