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

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).