Set truncations

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

module foundation.set-truncations where
Imports
open import foundation.effective-maps-equivalence-relations
open import foundation.equality-coproduct-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.mere-equality
open import foundation.reflecting-maps-equivalence-relations
open import foundation.sets
open import foundation.slice
open import foundation.surjective-maps
open import foundation.truncations
open import foundation.uniqueness-set-truncations
open import foundation.unit-type
open import foundation.universal-property-coproduct-types
open import foundation.universal-property-dependent-pair-types
open import foundation.universal-property-image
open import foundation.universal-property-set-quotients
open import foundation.universal-property-set-truncation

open import foundation-core.cartesian-product-types
open import foundation-core.contractible-types
open import foundation-core.coproduct-types
open import foundation-core.dependent-pair-types
open import foundation-core.embeddings
open import foundation-core.empty-types
open import foundation-core.equivalences
open import foundation-core.functions
open import foundation-core.functoriality-dependent-function-types
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.functoriality-function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.truncation-levels
open import foundation-core.universe-levels

Idea

The set truncation of a type A is a map η : A → trunc-Set A that satisfies the universal property of set truncations.

Definition

type-trunc-Set : {l : Level}  UU l  UU l
type-trunc-Set = type-trunc zero-𝕋

is-set-type-trunc-Set : {l : Level} {A : UU l}  is-set (type-trunc-Set A)
is-set-type-trunc-Set = is-trunc-type-trunc

trunc-Set : {l : Level}  UU l  Set l
trunc-Set = trunc zero-𝕋

unit-trunc-Set : {l : Level} {A : UU l}  A  type-trunc-Set A
unit-trunc-Set = unit-trunc

is-set-truncation-trunc-Set :
  {l1 l2 : Level} (A : UU l1) 
  is-set-truncation l2 (trunc-Set A) unit-trunc-Set
is-set-truncation-trunc-Set A = is-truncation-trunc

Properties

The dependent universal property of set truncations

dependent-universal-property-trunc-Set :
  {l1 : Level} {A : UU l1} {l : Level} 
  dependent-universal-property-set-truncation l (trunc-Set A) unit-trunc-Set
dependent-universal-property-trunc-Set = dependent-universal-property-trunc

equiv-dependent-universal-property-trunc-Set :
  {l1 l2 : Level} {A : UU l1} (B : type-trunc-Set A  Set l2) 
  ((x : type-trunc-Set A)  type-Set (B x)) 
  ((a : A)  type-Set (B (unit-trunc-Set a)))
equiv-dependent-universal-property-trunc-Set =
  equiv-dependent-universal-property-trunc

module _
  {l1 : Level} {A : UU l1}
  where

  Π-trunc-Set :
    {l2 : Level} (B : type-trunc-Set A  Set l2)
    (f : (a : A)  type-Set (B (unit-trunc-Set a)))  UU (l1  l2)
  Π-trunc-Set B f =
    Σ ( (x : type-trunc-Set A)  type-Set (B x))
      ( λ g  (g  unit-trunc-Set) ~ f)

  function-dependent-universal-property-trunc-Set :
    {l2 : Level} (B : type-trunc-Set A  Set l2) 
    ((x : A)  type-Set (B (unit-trunc-Set x))) 
    (x : type-trunc-Set A)  type-Set (B x)
  function-dependent-universal-property-trunc-Set B f =
    function-dependent-universal-property-trunc B f

  compute-dependent-universal-property-trunc-Set :
    {l2 : Level} (B : type-trunc-Set A  Set l2) 
    (f : (x : A)  type-Set (B (unit-trunc-Set x))) 
    (function-dependent-universal-property-trunc-Set B f  unit-trunc-Set) ~ f
  compute-dependent-universal-property-trunc-Set B f =
    htpy-dependent-universal-property-trunc B f

  apply-dependent-universal-property-trunc-Set' :
    {l2 : Level} (B : type-trunc-Set A  Set l2) 
    ((x : A)  type-Set (B (unit-trunc-Set x))) 
    (x : type-trunc-Set A)  type-Set (B x)
  apply-dependent-universal-property-trunc-Set' B =
    map-inv-equiv (equiv-dependent-universal-property-trunc-Set B)

The universal property of set truncations

universal-property-trunc-Set :
  {l1 l2 : Level} (A : UU l1) 
  universal-property-set-truncation l2
    ( trunc-Set A)
    ( unit-trunc-Set)
universal-property-trunc-Set A = universal-property-trunc zero-𝕋 A

equiv-universal-property-trunc-Set :
  {l1 l2 : Level} (A : UU l1) (B : Set l2) 
  (type-trunc-Set A  type-Set B)  (A  type-Set B)
equiv-universal-property-trunc-Set = equiv-universal-property-trunc

apply-universal-property-trunc-Set :
  {l1 l2 : Level} {A : UU l1} (t : type-trunc-Set A) (B : Set l2) 
  (A  type-Set B)  type-Set B
apply-universal-property-trunc-Set t B f = map-universal-property-trunc B f t

map-universal-property-trunc-Set :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) 
  (A  type-Set B)  type-hom-Set (trunc-Set A) B
map-universal-property-trunc-Set = map-universal-property-trunc

triangle-universal-property-trunc-Set :
  {l1 l2 : Level} {A : UU l1} (B : Set l2) 
  (f : A  type-Set B) 
  (map-universal-property-trunc-Set B f  unit-trunc-Set) ~ f
triangle-universal-property-trunc-Set = triangle-universal-property-trunc

module _
  {l1 : Level} {A : UU l1}
  where

  Map-trunc-Set :
    {l2 : Level} (B : Set l2) (f : A  type-Set B)  UU (l1  l2)
  Map-trunc-Set B f =
    Σ (type-trunc-Set A  type-Set B)  g  (g  unit-trunc-Set) ~ f)

  apply-universal-property-trunc-Set' :
    {l2 : Level} (t : type-trunc-Set A) (B : Set l2) 
    (A  type-Set B)  type-Set B
  apply-universal-property-trunc-Set' t B f =
    map-universal-property-trunc-Set B f t

The set truncation of X is the set quotient by the mere equality relation

reflecting-map-mere-eq-unit-trunc-Set :
  {l : Level} (A : UU l) 
  reflecting-map-Eq-Rel (mere-eq-Eq-Rel A) (type-trunc-Set A)
reflecting-map-mere-eq-unit-trunc-Set A =
  pair unit-trunc-Set (reflects-mere-eq (trunc-Set A) unit-trunc-Set)

abstract
  is-set-quotient-trunc-Set :
    {l1 l2 : Level} (A : UU l1) 
    is-set-quotient l2
      ( mere-eq-Eq-Rel A)
      ( trunc-Set A)
      ( reflecting-map-mere-eq-unit-trunc-Set A)
  is-set-quotient-trunc-Set A =
    is-set-quotient-is-set-truncation
      ( trunc-Set A)
      ( unit-trunc-Set)
      ( λ {l}  is-set-truncation-trunc-Set A)

abstract
  is-surjective-and-effective-unit-trunc-Set :
    {l1 : Level} (A : UU l1) 
    is-surjective-and-effective (mere-eq-Eq-Rel A) unit-trunc-Set
  is-surjective-and-effective-unit-trunc-Set A =
    is-surjective-and-effective-is-set-quotient
      ( mere-eq-Eq-Rel A)
      ( trunc-Set A)
      ( unit-trunc-Set ,
        reflects-mere-eq (trunc-Set A) unit-trunc-Set)
      ( λ {l}  is-set-quotient-trunc-Set A)

abstract
  is-surjective-unit-trunc-Set :
    {l1 : Level} (A : UU l1)  is-surjective (unit-trunc-Set {A = A})
  is-surjective-unit-trunc-Set A =
    pr1 (is-surjective-and-effective-unit-trunc-Set A)

abstract
  is-effective-unit-trunc-Set :
    {l1 : Level} (A : UU l1) 
    is-effective (mere-eq-Eq-Rel A) (unit-trunc-Set {A = A})
  is-effective-unit-trunc-Set A =
    pr2 (is-surjective-and-effective-unit-trunc-Set A)

abstract
  apply-effectiveness-unit-trunc-Set :
    {l1 : Level} {A : UU l1} {x y : A} 
    unit-trunc-Set x  unit-trunc-Set y  mere-eq x y
  apply-effectiveness-unit-trunc-Set {A = A} {x} {y} =
    map-equiv (is-effective-unit-trunc-Set A x y)

abstract
  apply-effectiveness-unit-trunc-Set' :
    {l1 : Level} {A : UU l1} {x y : A} 
    mere-eq x y  unit-trunc-Set x  unit-trunc-Set y
  apply-effectiveness-unit-trunc-Set' {A = A} {x} {y} =
    map-inv-equiv (is-effective-unit-trunc-Set A x y)

emb-trunc-Set :
  {l1 : Level} (A : UU l1)  type-trunc-Set A  (A  Prop l1)
emb-trunc-Set A =
  emb-is-surjective-and-effective
    ( mere-eq-Eq-Rel A)
    ( trunc-Set A)
    ( unit-trunc-Set)
    ( is-surjective-and-effective-unit-trunc-Set A)

hom-slice-trunc-Set :
  {l1 : Level} (A : UU l1) 
  hom-slice (mere-eq-Prop {A = A}) (map-emb (emb-trunc-Set A))
hom-slice-trunc-Set A =
  pair
    ( unit-trunc-Set)
    ( triangle-emb-is-surjective-and-effective
      ( mere-eq-Eq-Rel A)
      ( trunc-Set A)
      ( unit-trunc-Set)
      ( is-surjective-and-effective-unit-trunc-Set A))

abstract
  is-image-trunc-Set :
    {l1 l2 : Level} (A : UU l1) 
    is-image l2
      ( mere-eq-Prop {A = A})
      ( emb-trunc-Set A)
      ( hom-slice-trunc-Set A)
  is-image-trunc-Set A =
    is-image-is-surjective-and-effective
      ( mere-eq-Eq-Rel A)
      ( trunc-Set A)
      ( unit-trunc-Set)
      ( is-surjective-and-effective-unit-trunc-Set A)

Uniqueness of trunc-Set

module _
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B)
  {h : type-hom-Set B (trunc-Set A)} (H : (h  f) ~ unit-trunc-Set)
  where

  abstract
    is-equiv-is-set-truncation' :
      ({l : Level}  is-set-truncation l B f)  is-equiv h
    is-equiv-is-set-truncation' Sf =
      is-equiv-is-set-truncation-is-set-truncation
        ( B)
        ( f)
        ( trunc-Set A)
        ( unit-trunc-Set)
        ( H)
        ( Sf)
        ( λ {h}  is-set-truncation-trunc-Set A)

  abstract
    is-set-truncation-is-equiv' :
      is-equiv h  ({l : Level}  is-set-truncation l B f)
    is-set-truncation-is-equiv' Eh =
      is-set-truncation-is-equiv-is-set-truncation
        ( B)
        ( f)
        ( trunc-Set A)
        ( unit-trunc-Set)
        ( H)
        ( λ {l}  is-set-truncation-trunc-Set A)
        ( Eh)

module _
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B)
  {h : type-hom-Set (trunc-Set A) B} (H : (h  unit-trunc-Set) ~ f)
  where

  abstract
    is-equiv-is-set-truncation :
      ({l : Level}  is-set-truncation l B f)  is-equiv h
    is-equiv-is-set-truncation Sf =
      is-equiv-is-set-truncation-is-set-truncation
        ( trunc-Set A)
        ( unit-trunc-Set)
        ( B)
        ( f)
        ( H)
        ( λ {l}  is-set-truncation-trunc-Set A)
        ( Sf)

  abstract
    is-set-truncation-is-equiv :
      is-equiv h  ({l : Level}  is-set-truncation l B f)
    is-set-truncation-is-equiv Eh =
      is-set-truncation-is-set-truncation-is-equiv
        ( trunc-Set A)
        ( unit-trunc-Set)
        ( B)
        ( f)
        ( H)
        ( Eh)
        ( λ {l}  is-set-truncation-trunc-Set A)

is-equiv-unit-trunc-Set :
  {l : Level} (A : Set l)  is-equiv (unit-trunc-Set {A = type-Set A})
is-equiv-unit-trunc-Set = is-equiv-unit-trunc

equiv-unit-trunc-Set :
  {l : Level} (A : Set l)  type-Set A  type-trunc-Set (type-Set A)
equiv-unit-trunc-Set = equiv-unit-trunc

equiv-unit-trunc-empty-Set : empty  type-trunc-Set empty
equiv-unit-trunc-empty-Set = equiv-unit-trunc-Set empty-Set

abstract
  is-empty-trunc-Set :
    {l : Level} {A : UU l}  is-empty A  is-empty (type-trunc-Set A)
  is-empty-trunc-Set f x = apply-universal-property-trunc-Set' x empty-Set f

abstract
  is-empty-is-empty-trunc-Set :
    {l : Level} {A : UU l}  is-empty (type-trunc-Set A)  is-empty A
  is-empty-is-empty-trunc-Set f = f  unit-trunc-Set

equiv-unit-trunc-unit-Set : unit  type-trunc-Set unit
equiv-unit-trunc-unit-Set = equiv-unit-trunc-Set unit-Set

abstract
  is-contr-trunc-Set :
    {l : Level} {A : UU l}  is-contr A  is-contr (type-trunc-Set A)
  is-contr-trunc-Set {l} {A} H =
    is-contr-equiv'
      ( A)
      ( equiv-unit-trunc-Set (pair A (is-set-is-contr H)))
      ( H)

module _
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B)
  (Sf : {l : Level}  is-set-truncation l B f)
  where

  abstract
    uniqueness-trunc-Set :
      is-contr
        ( Σ (type-trunc-Set A  type-Set B)
        ( λ e  (map-equiv e  unit-trunc-Set) ~ f))
    uniqueness-trunc-Set =
      uniqueness-set-truncation (trunc-Set A) unit-trunc-Set B f
        ( λ {l}  is-set-truncation-trunc-Set A)
        ( Sf)

  equiv-uniqueness-trunc-Set : type-trunc-Set A  type-Set B
  equiv-uniqueness-trunc-Set =
    pr1 (center uniqueness-trunc-Set)

  map-equiv-uniqueness-trunc-Set : type-trunc-Set A  type-Set B
  map-equiv-uniqueness-trunc-Set =
    map-equiv equiv-uniqueness-trunc-Set

  triangle-uniqueness-trunc-Set :
    (map-equiv-uniqueness-trunc-Set  unit-trunc-Set) ~ f
  triangle-uniqueness-trunc-Set =
    pr2 (center uniqueness-trunc-Set)

module _
  {l1 l2 : Level} {A : UU l1} (B : Set l2) (f : A  type-Set B)
  (Sf : {l : Level}  is-set-truncation l B f)
  where

  abstract
    uniqueness-trunc-Set' :
      is-contr
        ( Σ ( type-Set B  type-trunc-Set A)
            ( λ e  (map-equiv e  f) ~ unit-trunc-Set))
    uniqueness-trunc-Set' =
      uniqueness-set-truncation B f (trunc-Set A) unit-trunc-Set Sf
        ( λ {l}  is-set-truncation-trunc-Set A)

  equiv-uniqueness-trunc-Set' : type-Set B  type-trunc-Set A
  equiv-uniqueness-trunc-Set' =
    pr1 (center uniqueness-trunc-Set')

  map-equiv-uniqueness-trunc-Set' : type-Set B  type-trunc-Set A
  map-equiv-uniqueness-trunc-Set' =
    map-equiv equiv-uniqueness-trunc-Set'

  triangle-uniqueness-trunc-Set' :
    (map-equiv-uniqueness-trunc-Set'  f) ~ unit-trunc-Set
  triangle-uniqueness-trunc-Set' =
    pr2 (center uniqueness-trunc-Set')

The set truncation of a set is equivalent to the set

module _
  {l : Level} (A : Set l)
  where

  equiv-unit-trunc-set :
    type-Set A  type-trunc-Set (type-Set A)
  equiv-unit-trunc-set =
    equiv-unit-trunc A

Distributive of set truncation over coproduct

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  abstract
    distributive-trunc-coprod-Set :
      is-contr
        ( Σ ( type-equiv-Set
              ( trunc-Set (A + B))
              ( coprod-Set (trunc-Set A) (trunc-Set B)))
            ( λ e 
              ( map-equiv e  unit-trunc-Set) ~
              ( map-coprod unit-trunc-Set unit-trunc-Set)))
    distributive-trunc-coprod-Set =
      uniqueness-trunc-Set
        ( coprod-Set (trunc-Set A) (trunc-Set B))
        ( map-coprod unit-trunc-Set unit-trunc-Set)
        ( λ {l} C 
          is-equiv-right-factor
            ( ev-inl-inr  x  type-Set C))
            ( precomp-Set (map-coprod unit-trunc-Set unit-trunc-Set) C)
            ( universal-property-coprod (type-Set C))
            ( is-equiv-comp
              ( map-prod
                ( precomp-Set unit-trunc-Set C)
                ( precomp-Set unit-trunc-Set C))
              ( ev-inl-inr  x  type-Set C))
              ( universal-property-coprod (type-Set C))
              ( is-equiv-map-prod
                ( precomp-Set unit-trunc-Set C)
                ( precomp-Set unit-trunc-Set C)
                ( is-set-truncation-trunc-Set A C)
                ( is-set-truncation-trunc-Set B C))))

  equiv-distributive-trunc-coprod-Set :
    type-equiv-Set
      ( trunc-Set (A + B))
      ( coprod-Set (trunc-Set A) (trunc-Set B))
  equiv-distributive-trunc-coprod-Set =
    pr1 (center distributive-trunc-coprod-Set)

  map-equiv-distributive-trunc-coprod-Set :
    type-hom-Set
      ( trunc-Set (A + B))
      ( coprod-Set (trunc-Set A) (trunc-Set B))
  map-equiv-distributive-trunc-coprod-Set =
    map-equiv equiv-distributive-trunc-coprod-Set

  triangle-distributive-trunc-coprod-Set :
    ( map-equiv-distributive-trunc-coprod-Set  unit-trunc-Set) ~
    ( map-coprod unit-trunc-Set unit-trunc-Set)
  triangle-distributive-trunc-coprod-Set =
    pr2 (center distributive-trunc-coprod-Set)

Set truncations of Σ-types

module _
  {l1 l2 : Level} (A : UU l1) (B : A  UU l2)
  where

  abstract
    trunc-Σ-Set :
      is-contr
        ( Σ ( type-trunc-Set (Σ A B) 
              type-trunc-Set (Σ A  x  type-trunc-Set (B x))))
            ( λ e 
              ( map-equiv e  unit-trunc-Set) ~
              ( unit-trunc-Set  tot  x  unit-trunc-Set))))
    trunc-Σ-Set =
      uniqueness-trunc-Set
        ( trunc-Set (Σ A  x  type-trunc-Set (B x))))
        ( unit-trunc-Set  tot  x  unit-trunc-Set))
        ( λ {l} C 
          is-equiv-right-factor
            ( ev-pair)
            ( precomp-Set (unit-trunc-Set  tot  x  unit-trunc-Set)) C)
            ( is-equiv-ev-pair)
            ( is-equiv-htpy-equiv
              ( ( equiv-map-Π
                  ( λ x  equiv-universal-property-trunc-Set (B x) C)) ∘e
                ( ( equiv-ev-pair) ∘e
                  ( equiv-universal-property-trunc-Set
                    ( Σ A (type-trunc-Set  B)) C)))
              ( refl-htpy)))

  equiv-trunc-Σ-Set :
    type-trunc-Set (Σ A B)  type-trunc-Set (Σ A  x  type-trunc-Set (B x)))
  equiv-trunc-Σ-Set =
    pr1 (center trunc-Σ-Set)

  map-equiv-trunc-Σ-Set :
    type-trunc-Set (Σ A B)  type-trunc-Set (Σ A  x  type-trunc-Set (B x)))
  map-equiv-trunc-Σ-Set =
    map-equiv equiv-trunc-Σ-Set

trunc-Set distributes over products

module _
  {l1 l2 : Level} (A : UU l1) (B : UU l2)
  where

  abstract
    distributive-trunc-prod-Set :
      is-contr
        ( Σ ( type-trunc-Set (A × B)  ( type-trunc-Set A × type-trunc-Set B))
            ( λ e 
              ( map-equiv e  unit-trunc-Set) ~
              ( map-prod unit-trunc-Set unit-trunc-Set)))
    distributive-trunc-prod-Set =
      uniqueness-trunc-Set
        ( prod-Set (trunc-Set A) (trunc-Set B))
        ( map-prod unit-trunc-Set unit-trunc-Set)
        ( λ {l} C 
          is-equiv-right-factor
            ( ev-pair)
            ( precomp-Set (map-prod unit-trunc-Set unit-trunc-Set) C)
            ( is-equiv-ev-pair)
            ( is-equiv-htpy-equiv
              ( ( equiv-universal-property-trunc-Set A (Π-Set' B  y  C))) ∘e
                ( ( equiv-postcomp
                    ( type-trunc-Set A)
                    (equiv-universal-property-trunc-Set B C)) ∘e
                  ( equiv-ev-pair)))
              ( refl-htpy)))

  equiv-distributive-trunc-prod-Set :
    type-trunc-Set (A × B)  ( type-trunc-Set A × type-trunc-Set B)
  equiv-distributive-trunc-prod-Set =
    pr1 (center distributive-trunc-prod-Set)

  map-equiv-distributive-trunc-prod-Set :
    type-trunc-Set (A × B)  type-trunc-Set A × type-trunc-Set B
  map-equiv-distributive-trunc-prod-Set =
    map-equiv equiv-distributive-trunc-prod-Set

  triangle-distributive-trunc-prod-Set :
    ( map-equiv-distributive-trunc-prod-Set  unit-trunc-Set) ~
    ( map-prod unit-trunc-Set unit-trunc-Set)
  triangle-distributive-trunc-prod-Set =
    pr2 (center distributive-trunc-prod-Set)