The universal property of truncations

module foundation-core.universal-property-truncation where

Imports

open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.type-theoretic-principle-of-choice

open import foundation-core.contractible-maps
open import foundation-core.contractible-types
open import foundation-core.dependent-pair-types
open import foundation-core.functions
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.sections
open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

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)

is-truncation :
  (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (B : Truncated-Type l2 k) → (A → type-Truncated-Type B) →
  UU (l1 ⊔ l2 ⊔ lsuc l)
is-truncation l {k = k} B f =
  (C : Truncated-Type l k) → is-equiv (precomp-Trunc f C)

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

The universal property of truncations

universal-property-truncation :
  (l : Level) {l1 l2 : Level} {k : 𝕋} {A : UU l1}
  (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) →
  UU (lsuc l ⊔ l1 ⊔ l2)
universal-property-truncation l {k = k} {A} B f =
  (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)

dependent-universal-property-truncation :
  {l1 l2 : Level} (l : Level) {k : 𝕋} {A : UU l1} (B : Truncated-Type l2 k)
  (f : A → type-Truncated-Type B) → UU (l1 ⊔ l2 ⊔ lsuc l)
dependent-universal-property-truncation l {k} B f =
  (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) →
    {l : Level} → is-truncation l (pair 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) →
    {l : Level} → is-truncation l 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 :
      ({l : Level} → universal-property-truncation l B f) →
      ({l : Level} → is-truncation l 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 :
      ({l : Level} → is-truncation l B f) →
      ({l : Level} → universal-property-truncation l 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 :
    ({l : Level} → is-truncation l 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 : {l : Level} → is-truncation l 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 :
      ({l : Level} → is-truncation l B f) →
      {l : Level} → dependent-universal-property-truncation l 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 :
      ({l : Level} → dependent-universal-property-truncation l B f) →
      {l : Level} → is-truncation l B f
    is-truncation-dependent-universal-property-truncation H X =
      H (λ b → X)

  sec-is-truncation :
    ({l : Level} → is-truncation l 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) → sec g
  sec-is-truncation H C h g K =
    map-distributive-Π-Σ
      ( map-inv-is-equiv
        ( dependent-universal-property-truncation-is-truncation H
          ( fib-Truncated-Type C B g))
        ( λ a → pair (h a) (inv (K a))))