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)