Identity systems of descent data for pushouts

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

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

{-# OPTIONS --lossy-unification #-}

module synthetic-homotopy-theory.identity-systems-descent-data-pushouts where
Imports 
open import foundation.commuting-squares-of-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.identity-systems
open import foundation.identity-types
open import foundation.sections
open import foundation.singleton-induction
open import foundation.span-diagrams
open import foundation.torsorial-type-families
open import foundation.transposition-identifications-along-equivalences
open import foundation.universal-property-dependent-pair-types
open import foundation.universal-property-identity-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-universal-property-pushouts
open import synthetic-homotopy-theory.descent-data-equivalence-types-over-pushouts
open import synthetic-homotopy-theory.descent-data-identity-types-over-pushouts
open import synthetic-homotopy-theory.descent-data-pushouts
open import synthetic-homotopy-theory.descent-property-pushouts
open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
open import synthetic-homotopy-theory.families-descent-data-pushouts
open import synthetic-homotopy-theory.flattening-lemma-pushouts
open import synthetic-homotopy-theory.morphisms-descent-data-pushouts
open import synthetic-homotopy-theory.sections-descent-data-pushouts
open import synthetic-homotopy-theory.universal-property-pushouts

Idea

We define a universal property of descent data for the identity types of pushouts, which allows their alternative characterizations. The property is analogous to being an identity system; in fact, we show that a type family over a pushout is an identity system if and only if the corresponding descent data satisfies this universal property.

Given descent data (PA, PB, PS) for the pushout

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

and a point p₀ : PA a₀ over a basepoint a₀ : A, we would like to mirror the definition of identity systems. A naïve translation would lead us to define dependent descent data and its sections. We choose to sidestep building that technical infrastructure. By the descent property, there is a unique type family P : X → 𝒰 corresponding to (PA, PB, PS). Observe that the type of dependent type families (x : X) → (p : P x) → 𝒰 is equivalent to the uncurried form (Σ X P) → 𝒰. By the flattening lemma, the total space Σ X P is the pushout of the span diagram of total spaces

  Σ A PA <----- Σ S (PA ∘ f) -----> Σ B PB,

so, again by the descent property, descent data over it correspond to type families over Σ X P. Hence we can talk about descent data (RΣA, RΣB, RΣS) over the total span diagram instead of dependent descent data.

Every such descent data induces an evaluation map ev-refl on its sections, which takes a section (tA, tB, tS) of (RΣA, RΣB, RΣS) to the point tA (a₀, p₀) : RΣA (a₀, p₀). We say that (PA, PB, PS) is an identity system based at p₀ if ev-refl has a section, in the sense that there is a converse map ind-R : RΣA (a₀, p₀) → section-descent-data (RΣA, RΣB, RΣS) such that (ind-R r)A (a₀, p₀) = r for all r : RΣA (a₀, p₀). Mind the unfortunate terminology clash between "sections of descent data" and "sections of a map".

Note that this development is biased towards to left --- we pick a basepoint in the domain a₀ : A, a point in the left type family p₀ : PA a₀, and the evaluation map evaluates the left map of the section. By symmetry of pushouts we could just as well work with the points b₀ : B, p₀ : PB b₀, and the evaluation map evaluating the right map of the section.

By showing that the canonical descent data for identity types is an identity system, we recover the "induction principle for pushout equality" stated and proved by Kraus and von Raumer in [KvR19].

First observe that the type of sections of the evaluation map is

  Σ (ind-R : (r : RΣA (a₀, p₀)) → section (RΣA, RΣB, RΣS))
    (is-sect : (r : RΣA (a₀, p₀)) → (ind-R r)A (a₀, p₀) = r),

which is equivalent to the type

  (r : RΣA (a₀, p₀)) →
  Σ (ind : section (RΣA, RΣB, RΣS))
    (preserves-pt : indA (a₀, p₀) = r)

by distributivity of Π over Σ.

Then the induction terms from [KvR19] (with names changed to fit our naming scheme)

  indᴬ : (a : A) (q : ia₀ = ia) → RΣA (a, q)
  indᴮ : (b : B) (q : ia₀ = jb) → RΣB (b, q)

are the first and second components of the section of (RΣA, RΣB, RΣS) induced by r, and their computation rules

  indᴬ a₀ refl = r
  (s : S) (q : ia₀ = ifa) → RΣS (s, q) (indᴬ fs q) = indᴮ gs (q ∙ H s)

arise as the preserves-pt component above, and the coherence condition of a section of (RΣA, RΣB, RΣS), respectively.

Definitions

The evaluation map of a section of descent data for pushouts

module _
  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
  (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮}
  (p₀ : left-family-descent-data-pushout P a₀)
  where

  ev-refl-section-descent-data-pushout :
    {l5 : Level}
    (R :
      descent-data-pushout (span-diagram-flattening-descent-data-pushout P) l5)
    (t : section-descent-data-pushout R) →
    left-family-descent-data-pushout R (a₀ , p₀)
  ev-refl-section-descent-data-pushout R t =
    left-map-section-descent-data-pushout R t (a₀ , p₀)

The predicate of being an identity system on descent data for pushouts

module _
  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
  (P : descent-data-pushout 𝒮 l4) {a₀ : domain-span-diagram 𝒮}
  (p₀ : left-family-descent-data-pushout P a₀)
  where

  is-identity-system-descent-data-pushout : UUω
  is-identity-system-descent-data-pushout =
    {l5 : Level}
    (R :
      descent-data-pushout
        ( span-diagram-flattening-descent-data-pushout P)
        ( l5)) →
    section (ev-refl-section-descent-data-pushout P p₀ R)

Properties

A type family over a pushout is an identity system if and only if the corresponding descent data is an identity system

Given a family with descent data P ≃ (PA, PB, PS) and a point p₀ : PA a₀, we show that (PA, PB, PS) is an identity system at p₀ if an only if P is an identity system at (eᴾA a)⁻¹ p₀ : P (ia₀).

Proof: Consider a family with descent data RΣ ≈ (RΣA, RΣB, RΣS). Recall that this datum consists of a type family RΣ : Σ X P → 𝒰, descent data

  RΣA : Σ A PA → 𝒰
  RΣB : Σ B PB → 𝒰
  RΣS : ((s, p) : (Σ (s : S) (p : PA fs))) → RΣA (fs, p) ≃ RΣB (gs, PS s p),

a pair of equivalences

  eᴿA : ((a, p) : Σ A PA) → RΣ (ia, (eᴾA a)⁻¹ p) ≃ RΣA (a, p)
  eᴿB : ((b, p) : Σ B PB) → RΣ (jb, (eᴾB b)⁻¹ p) ≃ RΣB (b, p),

and a coherence between them that isn't relevant here. Then there is a commuting square

  (x : X) → (p : P x) → RΣ (x, p) ---> (u : Σ X P) → RΣ u ----> section (RΣA, RΣB, RΣS)
                |                                                           |
                | ev-refl ((eᴾA a)⁻¹ p₀)                                    | ev-refl p₀
                |                                                           |
                ∨                                                           ∨
      RΣ (ia₀, (eᴾA a)⁻¹ p₀) ---------------------------------------> RΣA (a₀, p₀).
                                      eᴿA (a₀, p₀)

Since the top and bottom maps are equivalences, we get that the left map has a section if and only if the right map has a section.

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)
  {a₀ : domain-span-diagram 𝒮}
  (p₀ : left-family-family-with-descent-data-pushout P a₀)
  where

  private
    cocone-flattening :
      cocone-span-diagram
        ( span-diagram-flattening-descent-data-pushout
          ( descent-data-family-with-descent-data-pushout P))
        ( Σ X (family-cocone-family-with-descent-data-pushout P))
    cocone-flattening =
      cocone-flattening-descent-data-pushout _ _ c
        ( descent-data-family-with-descent-data-pushout P)
        ( family-cocone-family-with-descent-data-pushout P)
        ( inv-equiv-descent-data-family-with-descent-data-pushout P)

  square-ev-refl-section-descent-data-pushout :
    {l5 : Level}
    (R :
      family-with-descent-data-pushout
        ( cocone-flattening-descent-data-pushout _ _ c
          ( descent-data-family-with-descent-data-pushout P)
          ( family-cocone-family-with-descent-data-pushout P)
          ( inv-equiv-descent-data-pushout _ _
            ( equiv-descent-data-family-with-descent-data-pushout P)))
        ( l5)) →
    coherence-square-maps
      ( section-descent-data-section-family-cocone-span-diagram R ∘ ind-Σ)
      ( ev-refl-identity-system
        ( inv-left-map-family-with-descent-data-pushout P a₀ p₀))
      ( ev-refl-section-descent-data-pushout
        ( descent-data-family-with-descent-data-pushout P)
        ( p₀)
        ( descent-data-family-with-descent-data-pushout R))
      ( left-map-family-with-descent-data-pushout R (a₀ , p₀))
  square-ev-refl-section-descent-data-pushout R = refl-htpy

To show the forward implication, assume that (PA, PB, PS) is an identity system at p₀. We need to show that for every R : (x : X) (p : P x) → 𝒰, the evaluation map ev-refl ((eᴾA a)⁻¹ p₀) has a section. By the descent property, there is unique descent data (RΣA, RΣB, RΣS) for the uncurried family RΣ := λ (x, p) → R x p. Then we get the above square, and by assumption the right map has a section, hence the left map has a section.

  abstract
    is-identity-system-is-identity-system-descent-data-pushout :
      universal-property-pushout _ _ c →
      is-identity-system-descent-data-pushout
        ( descent-data-family-with-descent-data-pushout P)
        ( p₀) →
      is-identity-system
        ( family-cocone-family-with-descent-data-pushout P)
        ( horizontal-map-cocone _ _ c a₀)
        ( inv-left-map-family-with-descent-data-pushout P a₀ p₀)
    is-identity-system-is-identity-system-descent-data-pushout
      up-c id-system-P {l} R =
      section-left-map-triangle _ _ _
        ( square-ev-refl-section-descent-data-pushout fam-R)
        ( section-is-equiv
          ( is-equiv-comp _ _
            ( is-equiv-ind-Σ)
            ( is-equiv-section-descent-data-section-family-cocone-span-diagram
              ( fam-R)
              ( flattening-lemma-descent-data-pushout _ _ c
                ( descent-data-family-with-descent-data-pushout P)
                ( family-cocone-family-with-descent-data-pushout P)
                ( inv-equiv-descent-data-family-with-descent-data-pushout P)
                ( up-c)))))
        ( id-system-P (descent-data-family-with-descent-data-pushout fam-R))
      where
        fam-R : family-with-descent-data-pushout cocone-flattening l
        fam-R =
          family-with-descent-data-pushout-family-cocone
            ( cocone-flattening)
            ( ind-Σ R)

Similarly, assume P is an identity system at (eᴾA a)⁻¹ p₀, and assume descent data (RΣA, RΣB, RΣS). There is a unique corresponding type family RΣ. Then the square above commutes, and the left map has a section by assumption, so the right map has a section.

  abstract
    is-identity-system-descent-data-pushout-is-identity-system :
      universal-property-pushout _ _ c →
      is-identity-system
        ( family-cocone-family-with-descent-data-pushout P)
        ( horizontal-map-cocone _ _ c a₀)
        ( inv-left-map-family-with-descent-data-pushout P a₀ p₀) →
      is-identity-system-descent-data-pushout
        ( descent-data-family-with-descent-data-pushout P)
        ( p₀)
    is-identity-system-descent-data-pushout-is-identity-system
      up-c id-system-P {l} R =
      section-right-map-triangle _ _ _
        ( square-ev-refl-section-descent-data-pushout fam-R)
        ( section-comp _ _
          ( id-system-P
            ( ev-pair (family-cocone-family-with-descent-data-pushout fam-R)))
          ( section-map-equiv
            ( left-equiv-family-with-descent-data-pushout fam-R (a₀ , p₀))))
      where
        fam-R : family-with-descent-data-pushout cocone-flattening l
        fam-R =
          family-with-descent-data-pushout-descent-data-pushout
            ( flattening-lemma-descent-data-pushout _ _ c
              ( descent-data-family-with-descent-data-pushout P)
              ( family-cocone-family-with-descent-data-pushout P)
              ( inv-equiv-descent-data-family-with-descent-data-pushout P)
              ( up-c))
            ( R)

The canonical descent data for families of identity types is an identity system

Proof: By the above property, the descent data (IA, IB, IS) is an identity system at refl : ia₀ = ia₀ if and only if the corresponding type family Id (ia₀) : X → 𝒰 is an identity system at refl, which is already established.

module _
  {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
  (up-c : universal-property-pushout _ _ c)
  (a₀ : domain-span-diagram 𝒮)
  where

  abstract
    induction-principle-descent-data-pushout-identity-type :
      is-identity-system-descent-data-pushout
        ( descent-data-identity-type-pushout c (horizontal-map-cocone _ _ c a₀))
        ( refl)
    induction-principle-descent-data-pushout-identity-type =
      is-identity-system-descent-data-pushout-is-identity-system
        ( family-with-descent-data-identity-type-pushout c
          ( horizontal-map-cocone _ _ c a₀))
        ( refl)
        ( up-c)
        ( is-identity-system-is-torsorial
          ( horizontal-map-cocone _ _ c a₀)
          ( refl)
          ( is-torsorial-Id _))

Unique uniqueness of identity systems

For any identity system (PA, PB, PS) at p₀, there is a unique equivalence of descent data (IA, IB, IS) ≃ (PA, PB, PS) sending refl to p₀.

Proof: Consider the unique type family P : X → 𝒰 corresponding to (PA, PB, PS). The type of point preserving equivalences between (IA, IB, IS) and (PA, PB, PS) is equivalent to the type of fiberwise equivalences (x : X) → (ia₀ = x) ≃ P x that send refl to (eᴾA a₀)⁻¹ p₀. To show that this type is contractible, it suffices to show that P is torsorial. A type family is torsorial if it is an identity system, and we have shown that (PA, PB, PS) being an identity system implies that P is an identity system.

module _
  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
  (up-c : universal-property-pushout _ _ c)
  (P : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮}
  (p₀ : left-family-descent-data-pushout P a₀)
  (id-system-P : is-identity-system-descent-data-pushout P p₀)
  where

  abstract
    unique-uniqueness-identity-system-descent-data-pushout :
      is-contr
        ( Σ ( equiv-descent-data-pushout
              ( descent-data-identity-type-pushout c
                ( horizontal-map-cocone _ _ c a₀))
              ( P))
            ( λ e → left-map-equiv-descent-data-pushout _ _ e a₀ refl ＝ p₀))
    unique-uniqueness-identity-system-descent-data-pushout =
      is-contr-is-equiv'
        ( Σ ( (x : X) →
              (horizontal-map-cocone _ _ c a₀ ＝ x) ≃
              family-cocone-family-with-descent-data-pushout fam-P x)
            ( λ e → map-equiv (e (horizontal-map-cocone _ _ c a₀)) refl ＝ p₀'))
        ( _)
        ( is-equiv-map-Σ _
          ( is-equiv-equiv-descent-data-equiv-family-cocone-span-diagram
            ( family-with-descent-data-identity-type-pushout c
              ( horizontal-map-cocone _ _ c a₀))
            ( fam-P)
            ( up-c))
          ( λ e →
            is-equiv-map-inv-equiv
              ( eq-transpose-equiv
                ( left-equiv-family-with-descent-data-pushout fam-P a₀)
                ( _)
                ( p₀))))
        ( is-torsorial-pointed-fam-equiv-is-torsorial p₀'
          ( is-torsorial-is-identity-system
            ( horizontal-map-cocone _ _ c a₀)
            ( p₀')
            ( is-identity-system-is-identity-system-descent-data-pushout
              ( fam-P)
              ( p₀)
              ( up-c)
              ( id-system-P))))
      where
      fam-P : family-with-descent-data-pushout c l5
      fam-P = family-with-descent-data-pushout-descent-data-pushout up-c P
      p₀' :
        family-cocone-family-with-descent-data-pushout
          ( fam-P)
          ( horizontal-map-cocone _ _ c a₀)
      p₀' =
        map-compute-inv-left-family-cocone-descent-data-pushout up-c P a₀ p₀

Descent data with a converse to the evaluation map of sections of descent data is an identity system

To show that (PA, PB, PS) is an identity system at p₀ : PA a₀, it suffices to provide an element of the type H : RΣA (a₀, p₀) → section (RΣA, RΣB, RΣS) for all (RΣA, RΣB, RΣS).

Proof: Consider the unique family P : X → 𝒰 for (PA, PB, PS). It suffices to show that P is an identity system. As above, we can do that by showing that it is torsorial. By definition, that means that the total space Σ X P is contractible. We can prove that using the property that a type is contractible if we provide a point, here (ia₀, (eᴾA a)⁻¹ p₀), and a map

  H' : (RΣ : Σ X P → 𝒰) → (r₀ : RΣ (ia₀, (eᴾA a)⁻¹ p₀)) → (u : Σ X P) → RΣ u.

Assume such RΣ and r₀. A section (u : Σ X P) → RΣ u is given by a section of (RΣA, RΣB, RΣS), and we can get one by applying H to eᴿA (a₀, p₀) r₀ : RΣA (a₀, p₀).

module _
  {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
  {X : UU l4} {c : cocone-span-diagram 𝒮 X}
  (up-c : universal-property-pushout _ _ c)
  (P : descent-data-pushout 𝒮 l5) {a₀ : domain-span-diagram 𝒮}
  (p₀ : left-family-descent-data-pushout P a₀)
  where

  abstract
    is-identity-system-descent-data-pushout-ind-singleton :
      (H :
        {l6 : Level}
        (R :
          descent-data-pushout
            ( span-diagram-flattening-descent-data-pushout P)
            ( l6))
        (r₀ : left-family-descent-data-pushout R (a₀ , p₀)) →
        section-descent-data-pushout R) →
      is-identity-system-descent-data-pushout P p₀
    is-identity-system-descent-data-pushout-ind-singleton H =
      is-identity-system-descent-data-pushout-is-identity-system
        ( family-with-descent-data-pushout-descent-data-pushout up-c P)
        ( p₀)
        ( up-c)
        ( is-identity-system-is-torsorial
          ( horizontal-map-cocone _ _ c a₀)
          ( p₀')
          ( is-contr-ind-singleton _
            ( horizontal-map-cocone _ _ c a₀ , p₀')
            ( λ R r₀ →
              section-family-section-descent-data-pushout
                ( flattening-lemma-descent-data-pushout _ _ c P
                  ( family-cocone-descent-data-pushout up-c P)
                  ( inv-equiv-family-cocone-descent-data-pushout up-c P)
                  ( up-c))
                ( family-with-descent-data-pushout-family-cocone _ R)
                ( H (descent-data-family-cocone-span-diagram _ R) r₀))))
      where
        p₀' :
          family-cocone-descent-data-pushout up-c P
            ( horizontal-map-cocone _ _ c a₀)
        p₀' =
          map-compute-inv-left-family-cocone-descent-data-pushout up-c P a₀ p₀

References

[KvR19]
Nicolai Kraus and Jakob von Raumer. Path Spaces of Higher Inductive Types in Homotopy Type Theory. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '19. IEEE Press, 2019. arXiv:1901.06022.

Recent changes