Equivalences of descent data for pushouts

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

Created on 2024-05-31.
Last modified on 2024-06-05.

module synthetic-homotopy-theory.equivalences-descent-data-pushouts where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalence-extensionality
open import foundation.equivalences
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.univalence
open import foundation.universe-levels

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

Idea

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

  eA : (a : A) → PA a ≃ QA a
  eB : (b : B) → PB b ≃ QB b

equipped with a family of homotopies making

              eA(fs)
     PA(fs) --------> QA(fs)
       |                |
  PS s |                | QS s
       |                |
       ∨                ∨
     PB(gs) --------> QB(gs)
              eB(gs)

commute for every s : S.

We show that equivalences characterize the identity types of descent data for pushouts.

By forgetting that the fiberwise maps are equivalences, we get the underlying morphism of descent data. We define homotopies of equivalences of descent data to be homotopies of the underlying morphisms, and show that homotopies characterize the identity type of equivalences of descent data.

Definitions

Equivalences of descent data for pushouts

Note that the descent data arguments cannot be inferred when calling left-equiv-equiv-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

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

  module _
    (e : equiv-descent-data-pushout)
    where

    left-equiv-equiv-descent-data-pushout :
      (a : domain-span-diagram 𝒮) →
      left-family-descent-data-pushout P a ≃
      left-family-descent-data-pushout Q a
    left-equiv-equiv-descent-data-pushout = pr1 e

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

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

    inv-left-map-equiv-descent-data-pushout :
      (a : domain-span-diagram 𝒮) →
      left-family-descent-data-pushout Q a →
      left-family-descent-data-pushout P a
    inv-left-map-equiv-descent-data-pushout a =
      map-inv-equiv (left-equiv-equiv-descent-data-pushout a)

    right-equiv-equiv-descent-data-pushout :
      (b : codomain-span-diagram 𝒮) →
      right-family-descent-data-pushout P b ≃
      right-family-descent-data-pushout Q b
    right-equiv-equiv-descent-data-pushout = pr1 (pr2 e)

    right-map-equiv-descent-data-pushout :
      (b : codomain-span-diagram 𝒮) →
      right-family-descent-data-pushout P b →
      right-family-descent-data-pushout Q b
    right-map-equiv-descent-data-pushout b =
      map-equiv (right-equiv-equiv-descent-data-pushout b)

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

    inv-right-map-equiv-descent-data-pushout :
      (b : codomain-span-diagram 𝒮) →
      right-family-descent-data-pushout Q b →
      right-family-descent-data-pushout P b
    inv-right-map-equiv-descent-data-pushout b =
      map-inv-equiv (right-equiv-equiv-descent-data-pushout b)

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

    hom-equiv-descent-data-pushout : hom-descent-data-pushout P Q
    pr1 hom-equiv-descent-data-pushout =
      left-map-equiv-descent-data-pushout
    pr1 (pr2 hom-equiv-descent-data-pushout) =
      right-map-equiv-descent-data-pushout
    pr2 (pr2 hom-equiv-descent-data-pushout) =
      coherence-equiv-descent-data-pushout

The identity equivalence of descent data for pushouts

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

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

Inverses of equivalences of descent data for pushouts

Taking an inverse of an equivalence (eA, eB, eS) of descent data amounts to taking the inverses of the fiberwise maps

  a : A ⊢ eA(a)⁻¹ : QA a ≃ PA a
  b : B ⊢ eB(b)⁻¹ : QB b ≃ PB b

and mirroring the coherence squares vertically to get

             eA(a)⁻¹
     QA(fs) --------> PA(fs)
       |                |
  QS s |                | PS s
       |                |
       ∨                ∨
     QB(gs) --------> PB(gs).
             eB(a)⁻¹

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

  inv-equiv-descent-data-pushout :
    equiv-descent-data-pushout P Q → equiv-descent-data-pushout Q P
  pr1 (inv-equiv-descent-data-pushout e) a =
    inv-equiv (left-equiv-equiv-descent-data-pushout P Q e a)
  pr1 (pr2 (inv-equiv-descent-data-pushout e)) b =
    inv-equiv (right-equiv-equiv-descent-data-pushout P Q e b)
  pr2 (pr2 (inv-equiv-descent-data-pushout e)) s =
    horizontal-inv-equiv-coherence-square-maps
      ( left-equiv-equiv-descent-data-pushout P Q e (left-map-span-diagram 𝒮 s))
      ( map-family-descent-data-pushout P s)
      ( map-family-descent-data-pushout Q s)
      ( right-equiv-equiv-descent-data-pushout P Q e
        ( right-map-span-diagram 𝒮 s))
      ( coherence-equiv-descent-data-pushout P Q e s)

Homotopies of equivalences 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)
  where

  htpy-equiv-descent-data-pushout :
    (e f : equiv-descent-data-pushout P Q) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
  htpy-equiv-descent-data-pushout e f =
    htpy-hom-descent-data-pushout P Q
      ( hom-equiv-descent-data-pushout P Q e)
      ( hom-equiv-descent-data-pushout P Q f)

Properties

Characterization of identity types of descent data for pushouts

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

  equiv-eq-descent-data-pushout :
    (Q : descent-data-pushout 𝒮 l4) →
    P ＝ Q → equiv-descent-data-pushout P Q
  equiv-eq-descent-data-pushout .P refl = id-equiv-descent-data-pushout P

  abstract
    is-torsorial-equiv-descent-data-pushout :
      is-torsorial (equiv-descent-data-pushout {l5 = l4} P)
    is-torsorial-equiv-descent-data-pushout =
      is-torsorial-Eq-structure
        ( is-torsorial-Eq-Π
          ( λ a → is-torsorial-equiv (left-family-descent-data-pushout P a)))
        ( left-family-descent-data-pushout P , λ a → id-equiv)
        ( is-torsorial-Eq-structure
          ( is-torsorial-Eq-Π
            ( λ b → is-torsorial-equiv (right-family-descent-data-pushout P b)))
          ( right-family-descent-data-pushout P , λ b → id-equiv)
          ( is-torsorial-Eq-Π
            ( λ s →
              is-torsorial-htpy-equiv (equiv-family-descent-data-pushout P s))))

    is-equiv-equiv-eq-descent-data-pushout :
      (Q : descent-data-pushout 𝒮 l4) →
      is-equiv (equiv-eq-descent-data-pushout Q)
    is-equiv-equiv-eq-descent-data-pushout =
      fundamental-theorem-id
        ( is-torsorial-equiv-descent-data-pushout)
        ( equiv-eq-descent-data-pushout)

  extensionality-descent-data-pushout :
    (Q : descent-data-pushout 𝒮 l4) →
    (P ＝ Q) ≃ equiv-descent-data-pushout P Q
  pr1 (extensionality-descent-data-pushout Q) =
    equiv-eq-descent-data-pushout Q
  pr2 (extensionality-descent-data-pushout Q) =
    is-equiv-equiv-eq-descent-data-pushout Q

  eq-equiv-descent-data-pushout :
    (Q : descent-data-pushout 𝒮 l4) →
    equiv-descent-data-pushout P Q → P ＝ Q
  eq-equiv-descent-data-pushout Q =
    map-inv-equiv (extensionality-descent-data-pushout Q)

Characterization of identity types of equivalences of descent data of pushouts

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

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

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

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

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

Recent changes