Truncations
module foundation.truncations where
Imports
open import foundation.function-extensionality open import foundation.functoriality-dependent-function-types open import foundation.identity-types open import foundation.truncated-types open import foundation.universal-property-dependent-pair-types open import foundation-core.contractible-maps open import foundation-core.contractible-types open import foundation-core.dependent-pair-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.functions open import foundation-core.functoriality-dependent-pair-types open import foundation-core.fundamental-theorem-of-identity-types open import foundation-core.homotopies open import foundation-core.propositions open import foundation-core.truncation-levels open import foundation-core.universal-property-truncation open import foundation-core.universe-levels
Idea
We postulate the existence of truncations
Postulates
postulate type-trunc : {l : Level} (k : 𝕋) → UU l → UU l postulate is-trunc-type-trunc : {l : Level} {k : 𝕋} {A : UU l} → is-trunc k (type-trunc k A) trunc : {l : Level} (k : 𝕋) → UU l → Truncated-Type l k pr1 (trunc k A) = type-trunc k A pr2 (trunc k A) = is-trunc-type-trunc postulate unit-trunc : {l : Level} {k : 𝕋} {A : UU l} → A → type-trunc k A postulate is-truncation-trunc : {l1 l2 : Level} {k : 𝕋} {A : UU l1} → is-truncation l2 (trunc k A) unit-trunc equiv-universal-property-trunc : {l1 l2 : Level} {k : 𝕋} (A : UU l1) (B : Truncated-Type l2 k) → (type-trunc k A → type-Truncated-Type B) ≃ (A → type-Truncated-Type B) pr1 (equiv-universal-property-trunc A B) = precomp-Trunc unit-trunc B pr2 (equiv-universal-property-trunc A B) = is-truncation-trunc B
Properties
The n-truncations satisfy the universal property
universal-property-trunc : {l1 : Level} (k : 𝕋) (A : UU l1) → {l2 : Level} → universal-property-truncation l2 (trunc k A) unit-trunc universal-property-trunc k A = universal-property-truncation-is-truncation ( trunc k A) ( unit-trunc) ( is-truncation-trunc) module _ {l1 l2 : Level} {k : 𝕋} {A : UU l1} where apply-universal-property-trunc : (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) → Σ ( type-trunc k A → type-Truncated-Type B) ( λ h → (h ∘ unit-trunc) ~ f) apply-universal-property-trunc B f = center ( universal-property-truncation-is-truncation ( trunc k A) ( unit-trunc) ( is-truncation-trunc) ( B) ( f)) map-universal-property-trunc : (B : Truncated-Type l2 k) → (A → type-Truncated-Type B) → type-trunc k A → type-Truncated-Type B map-universal-property-trunc B f = pr1 (apply-universal-property-trunc B f) triangle-universal-property-trunc : (B : Truncated-Type l2 k) (f : A → type-Truncated-Type B) → (map-universal-property-trunc B f ∘ unit-trunc) ~ f triangle-universal-property-trunc B f = pr2 (apply-universal-property-trunc B f)
The n-truncations satisfy the dependent universal property
module _ {l1 : Level} {k : 𝕋} {A : UU l1} where dependent-universal-property-trunc : {l : Level} → dependent-universal-property-truncation l (trunc k A) unit-trunc dependent-universal-property-trunc = dependent-universal-property-truncation-is-truncation ( trunc k A) ( unit-trunc) ( is-truncation-trunc) equiv-dependent-universal-property-trunc : {l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) → ((x : type-trunc k A) → type-Truncated-Type (B x)) ≃ ((a : A) → type-Truncated-Type (B (unit-trunc a))) pr1 (equiv-dependent-universal-property-trunc B) = precomp-Π-Truncated-Type unit-trunc B pr2 (equiv-dependent-universal-property-trunc B) = dependent-universal-property-trunc B unique-dependent-function-trunc : {l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) (f : (x : A) → type-Truncated-Type (B (unit-trunc x))) → is-contr ( Σ ( (x : type-trunc k A) → type-Truncated-Type (B x)) ( λ h → (h ∘ unit-trunc) ~ f)) unique-dependent-function-trunc B f = is-contr-equiv' ( fib (precomp-Π-Truncated-Type unit-trunc B) f) ( equiv-tot ( λ h → equiv-funext)) ( is-contr-map-is-equiv ( dependent-universal-property-trunc B) ( f)) apply-dependent-universal-property-trunc : {l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) → (f : (x : A) → type-Truncated-Type (B (unit-trunc x))) → Σ ( (x : type-trunc k A) → type-Truncated-Type (B x)) ( λ h → (h ∘ unit-trunc) ~ f) apply-dependent-universal-property-trunc B f = center (unique-dependent-function-trunc B f) function-dependent-universal-property-trunc : {l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) → (f : (x : A) → type-Truncated-Type (B (unit-trunc x))) → (x : type-trunc k A) → type-Truncated-Type (B x) function-dependent-universal-property-trunc B f = pr1 (apply-dependent-universal-property-trunc B f) htpy-dependent-universal-property-trunc : {l2 : Level} (B : type-trunc k A → Truncated-Type l2 k) → (f : (x : A) → type-Truncated-Type (B (unit-trunc x))) → ( function-dependent-universal-property-trunc B f ∘ unit-trunc) ~ f htpy-dependent-universal-property-trunc B f = pr2 (apply-dependent-universal-property-trunc B f)
Families of k-truncated-types over k+1-truncations of types
unique-truncated-fam-trunc : {l1 l2 : Level} {k : 𝕋} {A : UU l1} → (B : A → Truncated-Type l2 k) → is-contr ( Σ ( type-trunc (succ-𝕋 k) A → Truncated-Type l2 k) ( λ C → (x : A) → type-equiv-Truncated-Type (B x) (C (unit-trunc x)))) unique-truncated-fam-trunc {l1} {l2} {k} {A} B = is-contr-equiv' ( Σ ( type-trunc (succ-𝕋 k) A → Truncated-Type l2 k) ( λ C → (C ∘ unit-trunc) ~ B)) ( equiv-tot ( λ C → equiv-map-Π ( λ x → ( extensionality-Truncated-Type (B x) (C (unit-trunc x))) ∘e ( equiv-inv (C (unit-trunc x)) (B x))))) ( universal-property-trunc ( succ-𝕋 k) ( A) ( Truncated-Type-Truncated-Type l2 k) ( B)) module _ {l1 l2 : Level} {k : 𝕋} {A : UU l1} (B : A → Truncated-Type l2 k) where truncated-fam-trunc : type-trunc (succ-𝕋 k) A → Truncated-Type l2 k truncated-fam-trunc = pr1 (center (unique-truncated-fam-trunc B)) fam-trunc : type-trunc (succ-𝕋 k) A → UU l2 fam-trunc = type-Truncated-Type ∘ truncated-fam-trunc compute-truncated-fam-trunc : (x : A) → type-equiv-Truncated-Type (B x) (truncated-fam-trunc (unit-trunc x)) compute-truncated-fam-trunc = pr2 (center (unique-truncated-fam-trunc B)) map-compute-truncated-fam-trunc : (x : A) → type-Truncated-Type (B x) → (fam-trunc (unit-trunc x)) map-compute-truncated-fam-trunc x = map-equiv (compute-truncated-fam-trunc x) total-truncated-fam-trunc : UU (l1 ⊔ l2) total-truncated-fam-trunc = Σ (type-trunc (succ-𝕋 k) A) fam-trunc module _ {l1 l2 l3 : Level} {k : 𝕋} {A : UU l1} (B : A → Truncated-Type l2 k) ( C : total-truncated-fam-trunc B → Truncated-Type l3 k) ( f : (x : A) (y : type-Truncated-Type (B x)) → type-Truncated-Type ( C ( pair ( unit-trunc x) ( map-equiv (compute-truncated-fam-trunc B x) y)))) where dependent-universal-property-total-truncated-fam-trunc : is-contr ( Σ ( (t : total-truncated-fam-trunc B) → type-Truncated-Type (C t)) ( λ h → (x : A) (y : type-Truncated-Type (B x)) → Id ( h (pair (unit-trunc x) (map-compute-truncated-fam-trunc B x y))) ( f x y))) dependent-universal-property-total-truncated-fam-trunc = is-contr-equiv _ ( equiv-Σ ( λ g → (x : A) → Id ( g (unit-trunc x)) ( map-equiv-Π ( λ u → type-Truncated-Type (C (pair (unit-trunc x) u))) ( compute-truncated-fam-trunc B x) ( λ u → id-equiv) ( f x))) ( equiv-ev-pair) ( λ g → equiv-map-Π ( λ x → ( inv-equiv equiv-funext) ∘e ( equiv-Π ( λ y → Id ( g (pair (unit-trunc x) y)) ( map-equiv-Π ( λ u → type-Truncated-Type (C (pair (unit-trunc x) u))) ( compute-truncated-fam-trunc B x) ( λ u → id-equiv) ( f x) ( y))) ( compute-truncated-fam-trunc B x) ( λ y → equiv-concat' ( g ( pair ( unit-trunc x) ( map-compute-truncated-fam-trunc B x y))) ( inv ( compute-map-equiv-Π ( λ u → type-Truncated-Type (C (pair (unit-trunc x) u))) ( compute-truncated-fam-trunc B x) ( λ y → id-equiv) ( λ y → f x y) ( y)))))))) ( unique-dependent-function-trunc ( λ y → truncated-type-succ-Truncated-Type k ( Π-Truncated-Type k ( truncated-fam-trunc B y) ( λ u → C (pair y u)))) ( λ y → map-equiv-Π ( λ u → type-Truncated-Type (C (pair (unit-trunc y) u))) ( compute-truncated-fam-trunc B y) ( λ u → id-equiv) ( f y))) function-dependent-universal-property-total-truncated-fam-trunc : (t : total-truncated-fam-trunc B) → type-Truncated-Type (C t) function-dependent-universal-property-total-truncated-fam-trunc = pr1 (center dependent-universal-property-total-truncated-fam-trunc) htpy-dependent-universal-property-total-truncated-fam-trunc : (x : A) (y : type-Truncated-Type (B x)) → Id ( function-dependent-universal-property-total-truncated-fam-trunc ( pair (unit-trunc x) (map-compute-truncated-fam-trunc B x y))) ( f x y) htpy-dependent-universal-property-total-truncated-fam-trunc = pr2 (center dependent-universal-property-total-truncated-fam-trunc)
An n-truncated type is equivalent to its n-truncation
module _ {l : Level} {k : 𝕋} (A : Truncated-Type l k) where map-inv-unit-trunc : type-trunc k (type-Truncated-Type A) → type-Truncated-Type A map-inv-unit-trunc = map-universal-property-trunc A id isretr-map-inv-unit-trunc : ( map-inv-unit-trunc ∘ unit-trunc) ~ id isretr-map-inv-unit-trunc = triangle-universal-property-trunc A id issec-map-inv-unit-trunc : ( unit-trunc ∘ map-inv-unit-trunc) ~ id issec-map-inv-unit-trunc = htpy-eq ( pr1 ( pair-eq-Σ ( eq-is-prop' ( is-trunc-succ-is-trunc ( neg-two-𝕋) ( universal-property-trunc ( k) ( type-Truncated-Type A) ( trunc k (type-Truncated-Type A)) ( unit-trunc))) ( pair ( unit-trunc ∘ map-inv-unit-trunc) ( unit-trunc ·l isretr-map-inv-unit-trunc)) ( pair ( id) ( refl-htpy))))) is-equiv-unit-trunc : is-equiv unit-trunc is-equiv-unit-trunc = is-equiv-has-inverse map-inv-unit-trunc issec-map-inv-unit-trunc isretr-map-inv-unit-trunc equiv-unit-trunc : type-Truncated-Type A ≃ type-trunc k (type-Truncated-Type A) pr1 equiv-unit-trunc = unit-trunc pr2 equiv-unit-trunc = is-equiv-unit-trunc
Truncation is idempotent
module _ {l : Level} (k : 𝕋) (A : UU l) where idempotent-trunc : type-trunc k (type-trunc k A) ≃ type-trunc k A idempotent-trunc = inv-equiv (equiv-unit-trunc (trunc k A))
Characterization of the identity types of truncations
module _ {l : Level} (k : 𝕋) {A : UU l} (a : A) where Eq-trunc-Truncated-Type : type-trunc (succ-𝕋 k) A → Truncated-Type l k Eq-trunc-Truncated-Type = truncated-fam-trunc (λ y → trunc k (a ＝ y)) Eq-trunc : type-trunc (succ-𝕋 k) A → UU l Eq-trunc x = type-Truncated-Type (Eq-trunc-Truncated-Type x) compute-Eq-trunc : (x : A) → type-trunc k (a ＝ x) ≃ Eq-trunc (unit-trunc x) compute-Eq-trunc = compute-truncated-fam-trunc (λ y → trunc k (a ＝ y)) map-compute-Eq-trunc : (x : A) → type-trunc k (a ＝ x) → Eq-trunc (unit-trunc x) map-compute-Eq-trunc x = map-equiv (compute-Eq-trunc x) refl-Eq-trunc : Eq-trunc (unit-trunc a) refl-Eq-trunc = map-compute-Eq-trunc a (unit-trunc refl) refl-compute-Eq-trunc : map-compute-Eq-trunc a (unit-trunc refl) ＝ refl-Eq-trunc refl-compute-Eq-trunc = refl is-contr-total-Eq-trunc : is-contr (Σ (type-trunc (succ-𝕋 k) A) Eq-trunc) pr1 (pr1 is-contr-total-Eq-trunc) = unit-trunc a pr2 (pr1 is-contr-total-Eq-trunc) = refl-Eq-trunc pr2 is-contr-total-Eq-trunc = function-dependent-universal-property-total-truncated-fam-trunc ( λ y → trunc k (a ＝ y)) ( Id-Truncated-Type ( Σ-Truncated-Type ( trunc (succ-𝕋 k) A) ( λ b → truncated-type-succ-Truncated-Type k ( Eq-trunc-Truncated-Type b))) ( pair (unit-trunc a) refl-Eq-trunc)) ( λ y → function-dependent-universal-property-trunc ( λ q → Id-Truncated-Type ( Σ-Truncated-Type ( trunc (succ-𝕋 k) A) ( λ y → truncated-type-succ-Truncated-Type k ( Eq-trunc-Truncated-Type y))) ( pair (unit-trunc a) refl-Eq-trunc) ( pair (unit-trunc y) (map-compute-Eq-trunc y q))) ( r y)) where r : (y : A) (p : a ＝ y) → Id { A = Σ (type-trunc (succ-𝕋 k) A) Eq-trunc} ( pair (unit-trunc a) refl-Eq-trunc) ( pair (unit-trunc y) (map-compute-Eq-trunc y (unit-trunc p))) r .a refl = refl Eq-eq-trunc : (x : type-trunc (succ-𝕋 k) A) → (unit-trunc a ＝ x) → Eq-trunc x Eq-eq-trunc .(unit-trunc a) refl = refl-Eq-trunc is-equiv-Eq-eq-trunc : (x : type-trunc (succ-𝕋 k) A) → is-equiv (Eq-eq-trunc x) is-equiv-Eq-eq-trunc = fundamental-theorem-id ( is-contr-total-Eq-trunc) ( Eq-eq-trunc) extensionality-trunc : (x : type-trunc (succ-𝕋 k) A) → (unit-trunc a ＝ x) ≃ Eq-trunc x pr1 (extensionality-trunc x) = Eq-eq-trunc x pr2 (extensionality-trunc x) = is-equiv-Eq-eq-trunc x effectiveness-trunc : (x : A) → type-trunc k (a ＝ x) ≃ (unit-trunc {k = succ-𝕋 k} a ＝ unit-trunc x) effectiveness-trunc x = inv-equiv (extensionality-trunc (unit-trunc x)) ∘e compute-Eq-trunc x map-effectiveness-trunc : (x : A) → type-trunc k (a ＝ x) → (unit-trunc {k = succ-𝕋 k} a ＝ unit-trunc x) map-effectiveness-trunc x = map-equiv (effectiveness-trunc x) refl-effectiveness-trunc : map-effectiveness-trunc a (unit-trunc refl) ＝ refl refl-effectiveness-trunc = isretr-map-inv-equiv (extensionality-trunc (unit-trunc a)) refl
Truncations of Σ-types
module _ {l1 l2 : Level} (k : 𝕋) {A : UU l1} {B : A → UU l2} where map-trunc-Σ : type-trunc k (Σ A B) → type-trunc k (Σ A (λ x → type-trunc k (B x))) map-trunc-Σ = map-universal-property-trunc ( trunc k (Σ A (λ x → type-trunc k (B x)))) ( λ (pair a b) → unit-trunc (pair a (unit-trunc b))) map-inv-trunc-Σ : type-trunc k (Σ A (λ x → type-trunc k (B x))) → type-trunc k (Σ A B) map-inv-trunc-Σ = map-universal-property-trunc ( trunc k (Σ A B)) ( λ (pair a |b|) → map-universal-property-trunc ( trunc k (Σ A B)) ( λ b → unit-trunc (pair a b)) ( |b|)) isretr-map-inv-trunc-Σ : ( map-inv-trunc-Σ ∘ map-trunc-Σ) ~ id isretr-map-inv-trunc-Σ = function-dependent-universal-property-trunc ( λ |ab| → Id-Truncated-Type' ( trunc k (Σ A B)) ( map-inv-trunc-Σ (map-trunc-Σ |ab|)) ( |ab|)) ( λ (pair a b) → ap map-inv-trunc-Σ ( triangle-universal-property-trunc _ ( λ (pair a' b') → unit-trunc (pair a' (unit-trunc b'))) ( pair a b)) ∙ (triangle-universal-property-trunc _ ( λ (pair a' |b'|) → map-universal-property-trunc ( trunc k (Σ A B)) ( λ b' → unit-trunc (pair a' b')) ( |b'|)) ( pair a (unit-trunc b)) ∙ triangle-universal-property-trunc _ ( λ b' → unit-trunc (pair a b')) ( b))) issec-map-inv-trunc-Σ : ( map-trunc-Σ ∘ map-inv-trunc-Σ) ~ id issec-map-inv-trunc-Σ = function-dependent-universal-property-trunc ( λ |a|b|| → Id-Truncated-Type' ( trunc k (Σ A (λ x → type-trunc k (B x)))) ( map-trunc-Σ (map-inv-trunc-Σ |a|b||)) ( |a|b||)) ( λ (pair a |b|) → function-dependent-universal-property-trunc (λ |b'| → Id-Truncated-Type' ( trunc k (Σ A (λ x → type-trunc k (B x)))) (map-trunc-Σ (map-inv-trunc-Σ (unit-trunc (pair a |b'|)))) (unit-trunc (pair a |b'|))) (λ b → ap map-trunc-Σ (triangle-universal-property-trunc _ ( λ (pair a' |b'|) → map-universal-property-trunc ( trunc k (Σ A B)) ( λ b' → unit-trunc (pair a' b')) ( |b'|)) ( pair a (unit-trunc b))) ∙ (ap map-trunc-Σ (triangle-universal-property-trunc ( trunc k (Σ A B)) ( λ b' → unit-trunc (pair a b')) ( b)) ∙ triangle-universal-property-trunc _ ( λ (pair a' b') → unit-trunc (pair a' (unit-trunc b'))) ( pair a b))) ( |b|)) equiv-trunc-Σ : type-trunc k (Σ A B) ≃ type-trunc k (Σ A (λ x → type-trunc k (B x))) pr1 equiv-trunc-Σ = map-trunc-Σ pr2 equiv-trunc-Σ = is-equiv-has-inverse map-inv-trunc-Σ issec-map-inv-trunc-Σ isretr-map-inv-trunc-Σ inv-equiv-trunc-Σ : type-trunc k (Σ A (λ x → type-trunc k (B x))) ≃ type-trunc k (Σ A B) pr1 inv-equiv-trunc-Σ = map-inv-trunc-Σ pr2 inv-equiv-trunc-Σ = is-equiv-has-inverse map-trunc-Σ isretr-map-inv-trunc-Σ issec-map-inv-trunc-Σ