The universal property of truncations

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-07-17.
Last modified on 2024-02-06.

module foundation-core.universal-property-truncation where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.universal-property-equivalences
open import foundation.universe-levels

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.precomposition-functions
open import foundation-core.sections
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.type-theoretic-principle-of-choice

Idea

We say that a map f : A → B into a k-truncated type B is a k-truncation of A – or that it satisfies the universal property of the k-truncation of A – if any map g : A → C into a k-truncated type C extends uniquely along f to a map B → C.

Definition

The condition on a map to be a truncation

precomp-Trunc :
  {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
  (C : Truncated-Type l3 k) →
  (B → type-Truncated-Type C) → (A → type-Truncated-Type C)
precomp-Trunc f C = precomp f (type-Truncated-Type C)

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
  where

  is-truncation : UUω
  is-truncation =
    {l : Level} (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C)

  equiv-is-truncation :
    {l3 : Level} (H : is-truncation) (C : Truncated-Type l3 k) →
    ( type-Truncated-Type B → type-Truncated-Type C) ≃
    ( A → type-Truncated-Type C)
  pr1 (equiv-is-truncation H C) = precomp-Trunc f C
  pr2 (equiv-is-truncation H C) = H C

The universal property of truncations

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
  where

  universal-property-truncation : UUω
  universal-property-truncation =
    {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
    is-contr (Σ (type-hom-Truncated-Type k B C) (λ h → h ∘ f ~ g))

The dependent universal property of truncations

precomp-Π-Truncated-Type :
  {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} {B : UU l2} (f : A → B)
  (C : B → Truncated-Type l3 k) →
  ((b : B) → type-Truncated-Type (C b)) →
  ((a : A) → type-Truncated-Type (C (f a)))
precomp-Π-Truncated-Type f C h a = h (f a)

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B)
  where

  dependent-universal-property-truncation : UUω
  dependent-universal-property-truncation =
    {l : Level} (X : type-Truncated-Type B → Truncated-Type l k) →
    is-equiv (precomp-Π-Truncated-Type f X)

Properties

Equivalences into k-truncated types are truncations

abstract
  is-truncation-id :
    {l1 : Level} {k : 𝕋} {A : UU l1} (H : is-trunc k A) →
    is-truncation (A , H) id
  is-truncation-id H B =
    is-equiv-precomp-is-equiv id is-equiv-id (type-Truncated-Type B)

abstract
  is-truncation-equiv :
    {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
    (e : A ≃ type-Truncated-Type B) →
    is-truncation B (map-equiv e)
  is-truncation-equiv B e C =
    is-equiv-precomp-is-equiv
      ( map-equiv e)
      ( is-equiv-map-equiv e)
      ( type-Truncated-Type C)

A map into a truncated type is a truncation if and only if it satisfies the universal property of the truncation

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
  (f : A → type-Truncated-Type B)
  where

  abstract
    is-truncation-universal-property-truncation :
      universal-property-truncation B f → is-truncation B f
    is-truncation-universal-property-truncation H C =
      is-equiv-is-contr-map
        ( λ g →
          is-contr-equiv
            ( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ~ g))
            ( equiv-tot (λ h → equiv-funext))
            ( H C g))

  abstract
    universal-property-truncation-is-truncation :
      is-truncation B f → universal-property-truncation B f
    universal-property-truncation-is-truncation H C g =
      is-contr-equiv'
        ( Σ (type-hom-Truncated-Type k B C) (λ h → (h ∘ f) ＝ g))
        ( equiv-tot (λ h → equiv-funext))
        ( is-contr-map-is-equiv (H C) g)

  map-is-truncation :
    is-truncation B f →
    {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
    type-hom-Truncated-Type k B C
  map-is-truncation H C g =
    pr1 (center (universal-property-truncation-is-truncation H C g))

  triangle-is-truncation :
    (H : is-truncation B f) →
    {l : Level} (C : Truncated-Type l k) (g : A → type-Truncated-Type C) →
    map-is-truncation H C g ∘ f ~ g
  triangle-is-truncation H C g =
    pr2 (center (universal-property-truncation-is-truncation H C g))

A map into a truncated type is a truncation if and only if it satisfies the dependent universal property of the truncation

module _
  {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
  (f : A → type-Truncated-Type B)
  where

  abstract
    dependent-universal-property-truncation-is-truncation :
      is-truncation B f →
      dependent-universal-property-truncation B f
    dependent-universal-property-truncation-is-truncation H X =
      is-fiberwise-equiv-is-equiv-map-Σ
        ( λ (h : A → type-Truncated-Type B) →
          (a : A) → type-Truncated-Type (X (h a)))
        ( λ (g : type-Truncated-Type B → type-Truncated-Type B) → g ∘ f)
        ( λ g (s : (b : type-Truncated-Type B) →
          type-Truncated-Type (X (g b))) (a : A) → s (f a))
        ( H B)
        ( is-equiv-equiv
          ( inv-distributive-Π-Σ)
          ( inv-distributive-Π-Σ)
          ( ind-Σ (λ g s → refl))
          ( H (Σ-Truncated-Type B X)))
        ( id)

  abstract
    is-truncation-dependent-universal-property-truncation :
      dependent-universal-property-truncation B f → is-truncation B f
    is-truncation-dependent-universal-property-truncation H X = H (λ _ → X)

  section-is-truncation :
    is-truncation B f →
    {l3 : Level} (C : Truncated-Type l3 k)
    (h : A → type-Truncated-Type C) (g : type-hom-Truncated-Type k C B) →
    f ~ g ∘ h → section g
  section-is-truncation H C h g K =
    map-distributive-Π-Σ
      ( map-inv-is-equiv
        ( dependent-universal-property-truncation-is-truncation H
          ( fiber-Truncated-Type C B g))
        ( λ a → (h a , inv (K a))))

Recent changes