Truncation levels
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.
Created on 2022-01-26.
Last modified on 2025-08-30.
module foundation.truncation-levels where open import foundation-core.truncation-levels public
Imports
open import elementary-number-theory.natural-numbers open import foundation.action-on-identifications-functions open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types
Definitions
Inclusions of the natural numbers into the truncation levels
truncation-level-minus-two-ℕ : ℕ → 𝕋 truncation-level-minus-two-ℕ zero-ℕ = neg-two-𝕋 truncation-level-minus-two-ℕ (succ-ℕ n) = succ-𝕋 (truncation-level-minus-two-ℕ n) truncation-level-minus-one-ℕ : ℕ → 𝕋 truncation-level-minus-one-ℕ = succ-𝕋 ∘ truncation-level-minus-two-ℕ truncation-level-ℕ : ℕ → 𝕋 truncation-level-ℕ = succ-𝕋 ∘ truncation-level-minus-one-ℕ
Inclusion of the double successors of truncation levels into the natural numbers
nat+2-𝕋 : 𝕋 → ℕ nat+2-𝕋 neg-two-𝕋 = zero-ℕ nat+2-𝕋 (succ-𝕋 k) = succ-ℕ (nat+2-𝕋 k)
Recent changes
- 2025-08-30. Fredrik Bakke. Closure properties of π-finite types (#1311).
- 2024-11-05. Fredrik Bakke. Some results about path-cosplit maps (#1167).
- 2023-11-27. Elisabeth Stenholm, Daniel Gratzer and Egbert Rijke. Additions during work on material set theory in HoTT (#910).
- 2023-11-01. Fredrik Bakke. Opposite categories, gaunt categories, replete subprecategories, large Yoneda, and miscellaneous additions (#880).
- 2023-09-10. Fredrik Bakke. Define precedence levels and associativities for all binary operators (#712).