Truncated types
Content created by Egbert Rijke, Fredrik Bakke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-06-08.
module foundation.truncated-types where open import foundation-core.truncated-types public
Imports
open import foundation.dependent-pair-types open import foundation.subtype-identity-principle open import foundation.univalence open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.embeddings open import foundation-core.equivalences open import foundation-core.identity-types open import foundation-core.subtypes open import foundation-core.truncation-levels
Definition
The subuniverse of truncated types is itself truncated
is-contr-total-equiv-Truncated-Type : {l : Level} {k : 𝕋} (A : Truncated-Type l k) → is-contr (Σ (Truncated-Type l k) (type-equiv-Truncated-Type A)) is-contr-total-equiv-Truncated-Type A = is-contr-total-Eq-subtype ( is-contr-total-equiv (type-Truncated-Type A)) ( is-prop-is-trunc _) ( type-Truncated-Type A) ( id-equiv) ( is-trunc-type-Truncated-Type A) extensionality-Truncated-Type : {l : Level} {k : 𝕋} (A B : Truncated-Type l k) → (A = B) ≃ type-equiv-Truncated-Type A B extensionality-Truncated-Type A = extensionality-type-subtype ( is-trunc-Prop _) ( is-trunc-type-Truncated-Type A) ( id-equiv) ( λ X → equiv-univalence) abstract is-trunc-Truncated-Type : {l : Level} (k : 𝕋) → is-trunc (succ-𝕋 k) (Truncated-Type l k) is-trunc-Truncated-Type k X Y = is-trunc-equiv k ( type-equiv-Truncated-Type X Y) ( extensionality-Truncated-Type X Y) ( is-trunc-type-equiv-Truncated-Type X Y) Truncated-Type-Truncated-Type : (l : Level) (k : 𝕋) → Truncated-Type (lsuc l) (succ-𝕋 k) pr1 (Truncated-Type-Truncated-Type l k) = Truncated-Type l k pr2 (Truncated-Type-Truncated-Type l k) = is-trunc-Truncated-Type k
The embedding of the subuniverse of truncated types into the universe
emb-type-Truncated-Type : (l : Level) (k : 𝕋) → Truncated-Type l k ↪ UU l emb-type-Truncated-Type l k = emb-subtype (is-trunc-Prop k)
Recent changes
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).