Morphisms of descent data for pushouts

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

Created on 2024-05-31.

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

Imports
open import foundation.commuting-squares-of-homotopies
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.span-diagrams
open import foundation.structure-identity-principle
open import foundation.torsorial-type-families
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import synthetic-homotopy-theory.descent-data-pushouts


Idea

Given descent data for pushouts (PA, PB, PS) and (QA, QB, QS), a morphism between them is a pair of fiberwise maps

  hA : (a : A) → PA a → QA a
hB : (b : B) → PB b → QB b


equipped with a family of homotopies making

              hA(fs)
PA(fs) --------> QA(fs)
|                |
PS s |                | QS s
|                |
∨                ∨
PB(gs) --------> QB(gs)
hB(gs)


commute for every s : S.

For any two morphisms (hA, hB, hS) and (kA, kB, kS), we can define the type of homotopies between them as the type of triples (HA, HB, HS), where HA and HB are fiberwise homotopies

  HA : (a : A) → hA a ~ kA a
HB : (b : B) → hB b ~ kB b,


and HS is a coherence datum showing that for all s : S, the square of homotopies

                 HB(gs) ·r PS s
hB(gs) ∘ PS s ---------------> kB(gs) ∘ PS s
|                              |
hS s |                              | tS s
|                              |
∨                              ∨
QS s ∘ hA(fs) ---------------> QS s ∘ kA(fs)
QS s ·l HA(fs)


commutes. This coherence datum may be seen as a filler of the diagram one gets by gluing the squares hS and tS along the common vertical maps

             tA(fs)
________
/        ∨
PA(fs)          QA(fs)
|   \________∧  |
|     hA(fs)    |
|               |
PS s |               | QS s
|     tB(gs)    |
|    ________   |
∨   /        ∨  ∨
PB(gs)          QB(gs).
\________∧
hB(gs)


The front and back faces are hS s and tS s, and the top and bottom faces are HA(fs) and HB(gs), respectively. HS then expresses that going along the front face and then the top face is homotopic to first going along the bottom face and then the back face.

We then show that homotopies characterize the identity types of morphisms of descent data.

Definitions

Morphisms of descent data for pushouts

Note that the descent data arguments cannot be inferred when calling left-map-hom-descent-data-pushout and the like, since Agda cannot infer the proofs of is-equiv of their gluing maps.

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

hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
hom-descent-data-pushout =
Σ ( (a : domain-span-diagram 𝒮) →
left-family-descent-data-pushout P a →
left-family-descent-data-pushout Q a)
( λ hA →
Σ ( (b : codomain-span-diagram 𝒮) →
right-family-descent-data-pushout P b →
right-family-descent-data-pushout Q b)
( λ hB →
(s : spanning-type-span-diagram 𝒮) →
coherence-square-maps
( hA (left-map-span-diagram 𝒮 s))
( map-family-descent-data-pushout P s)
( map-family-descent-data-pushout Q s)
( hB (right-map-span-diagram 𝒮 s))))

module _
(h : hom-descent-data-pushout)
where

left-map-hom-descent-data-pushout :
(a : domain-span-diagram 𝒮) →
left-family-descent-data-pushout P a →
left-family-descent-data-pushout Q a
left-map-hom-descent-data-pushout = pr1 h

right-map-hom-descent-data-pushout :
(b : codomain-span-diagram 𝒮) →
right-family-descent-data-pushout P b →
right-family-descent-data-pushout Q b
right-map-hom-descent-data-pushout = pr1 (pr2 h)

coherence-hom-descent-data-pushout :
(s : spanning-type-span-diagram 𝒮) →
coherence-square-maps
( left-map-hom-descent-data-pushout (left-map-span-diagram 𝒮 s))
( map-family-descent-data-pushout P s)
( map-family-descent-data-pushout Q s)
( right-map-hom-descent-data-pushout (right-map-span-diagram 𝒮 s))
coherence-hom-descent-data-pushout = pr2 (pr2 h)


The identity morphism of descent data for pushouts

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

id-hom-descent-data-pushout : hom-descent-data-pushout P P
pr1 id-hom-descent-data-pushout a = id
pr1 (pr2 id-hom-descent-data-pushout) b = id
pr2 (pr2 id-hom-descent-data-pushout) s = refl-htpy


Composition of morphisms of descent data for pushouts

module _
{l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3}
(P : descent-data-pushout 𝒮 l4)
(Q : descent-data-pushout 𝒮 l5)
(R : descent-data-pushout 𝒮 l6)
(g : hom-descent-data-pushout Q R)
(f : hom-descent-data-pushout P Q)
where

comp-hom-descent-data-pushout : hom-descent-data-pushout P R
pr1 comp-hom-descent-data-pushout a =
left-map-hom-descent-data-pushout Q R g a ∘
left-map-hom-descent-data-pushout P Q f a
pr1 (pr2 comp-hom-descent-data-pushout) b =
right-map-hom-descent-data-pushout Q R g b ∘
right-map-hom-descent-data-pushout P Q f b
pr2 (pr2 comp-hom-descent-data-pushout) s =
pasting-horizontal-coherence-square-maps
( left-map-hom-descent-data-pushout P Q f
( left-map-span-diagram 𝒮 s))
( left-map-hom-descent-data-pushout Q R g
( left-map-span-diagram 𝒮 s))
( map-family-descent-data-pushout P s)
( map-family-descent-data-pushout Q s)
( map-family-descent-data-pushout R s)
( right-map-hom-descent-data-pushout P Q f
( right-map-span-diagram 𝒮 s))
( right-map-hom-descent-data-pushout Q R g
( right-map-span-diagram 𝒮 s))
( coherence-hom-descent-data-pushout P Q f s)
( coherence-hom-descent-data-pushout Q R g s)


Homotopies between morphisms of descent data for pushouts

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

htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
htpy-hom-descent-data-pushout =
Σ ( (a : domain-span-diagram 𝒮) →
left-map-hom-descent-data-pushout P Q f a ~
left-map-hom-descent-data-pushout P Q g a)
( λ HA →
Σ ( (b : codomain-span-diagram 𝒮) →
right-map-hom-descent-data-pushout P Q f b ~
right-map-hom-descent-data-pushout P Q g b)
( λ HB →
(s : spanning-type-span-diagram 𝒮) →
coherence-square-homotopies
( ( HB (right-map-span-diagram 𝒮 s)) ·r
( map-family-descent-data-pushout P s))
( coherence-hom-descent-data-pushout P Q f s)
( coherence-hom-descent-data-pushout P Q g s)
( ( map-family-descent-data-pushout Q s) ·l
( HA (left-map-span-diagram 𝒮 s)))))


The reflexive homotopy between morphisms of descent data for pushouts

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

refl-htpy-hom-descent-data-pushout : htpy-hom-descent-data-pushout P Q f f
pr1 refl-htpy-hom-descent-data-pushout a = refl-htpy
pr1 (pr2 refl-htpy-hom-descent-data-pushout) b = refl-htpy
pr2 (pr2 refl-htpy-hom-descent-data-pushout) s = right-unit-htpy


Properties

Characterizing the identity type of morphisms of descent data for pushouts

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

htpy-eq-hom-descent-data-pushout :
(g : hom-descent-data-pushout P Q) →
(f ＝ g) → htpy-hom-descent-data-pushout P Q f g
htpy-eq-hom-descent-data-pushout .f refl =
refl-htpy-hom-descent-data-pushout P Q f

abstract
is-torsorial-htpy-hom-descent-data-pushout :
is-torsorial (htpy-hom-descent-data-pushout P Q f)
is-torsorial-htpy-hom-descent-data-pushout =
is-torsorial-Eq-structure
( is-torsorial-Eq-Π
( λ a →
is-torsorial-htpy (left-map-hom-descent-data-pushout P Q f a)))
( left-map-hom-descent-data-pushout P Q f , λ a → refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-Eq-Π
( λ b →
is-torsorial-htpy (right-map-hom-descent-data-pushout P Q f b)))
( right-map-hom-descent-data-pushout P Q f , λ b → refl-htpy)
( is-torsorial-Eq-Π
( λ s →
is-torsorial-htpy
( coherence-hom-descent-data-pushout P Q f s ∙h refl-htpy))))

is-equiv-htpy-eq-hom-descent-data-pushout :
(g : hom-descent-data-pushout P Q) →
is-equiv (htpy-eq-hom-descent-data-pushout g)
is-equiv-htpy-eq-hom-descent-data-pushout =
fundamental-theorem-id
( is-torsorial-htpy-hom-descent-data-pushout)
( htpy-eq-hom-descent-data-pushout)

extensionality-hom-descent-data-pushout :
(g : hom-descent-data-pushout P Q) →
(f ＝ g) ≃ htpy-hom-descent-data-pushout P Q f g
pr1 (extensionality-hom-descent-data-pushout g) =
htpy-eq-hom-descent-data-pushout g
pr2 (extensionality-hom-descent-data-pushout g) =
is-equiv-htpy-eq-hom-descent-data-pushout g

eq-htpy-hom-descent-data-pushout :
(g : hom-descent-data-pushout P Q) →
htpy-hom-descent-data-pushout P Q f g → f ＝ g
eq-htpy-hom-descent-data-pushout g =
map-inv-equiv (extensionality-hom-descent-data-pushout g)