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 2023-11-27.
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.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 truncation levels into the natural numbers
nat-succ-succ-𝕋 : 𝕋 → ℕ nat-succ-succ-𝕋 neg-two-𝕋 = zero-ℕ nat-succ-succ-𝕋 (succ-𝕋 k) = succ-ℕ (nat-succ-succ-𝕋 k)
Addition of truncation levels
add-𝕋 : 𝕋 → 𝕋 → 𝕋 add-𝕋 neg-two-𝕋 neg-two-𝕋 = neg-two-𝕋 add-𝕋 neg-two-𝕋 (succ-𝕋 neg-two-𝕋) = neg-two-𝕋 add-𝕋 neg-two-𝕋 (succ-𝕋 (succ-𝕋 l)) = l add-𝕋 (succ-𝕋 neg-two-𝕋) neg-two-𝕋 = neg-two-𝕋 add-𝕋 (succ-𝕋 neg-two-𝕋) (succ-𝕋 l) = l add-𝕋 (succ-𝕋 (succ-𝕋 k)) neg-two-𝕋 = k add-𝕋 (succ-𝕋 (succ-𝕋 k)) (succ-𝕋 l) = succ-𝕋 (add-𝕋 (succ-𝕋 k) (succ-𝕋 l)) infixl 35 _+𝕋_ _+𝕋_ = add-𝕋
Iterated successor functions on truncation levels
Although we can define an addition operation on truncation levels, when it comes to doing induction on them, it is more natural to speak in terms of an iterated successor:
iterated-succ-𝕋 : ℕ → 𝕋 → 𝕋 iterated-succ-𝕋 zero-ℕ x = x iterated-succ-𝕋 (succ-ℕ n) x = iterated-succ-𝕋 n (succ-𝕋 x) iterated-succ-𝕋' : 𝕋 → ℕ → 𝕋 iterated-succ-𝕋' x n = iterated-succ-𝕋 n x
Properties
Unit laws for addition of truncation levels
left-unit-law-add-𝕋 : (k : 𝕋) → zero-𝕋 +𝕋 k = k left-unit-law-add-𝕋 neg-two-𝕋 = refl left-unit-law-add-𝕋 (succ-𝕋 neg-two-𝕋) = refl left-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 neg-two-𝕋)) = refl left-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) = refl right-unit-law-add-𝕋 : (k : 𝕋) → k +𝕋 zero-𝕋 = k right-unit-law-add-𝕋 neg-two-𝕋 = refl right-unit-law-add-𝕋 (succ-𝕋 neg-two-𝕋) = refl right-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 k)) = ap succ-𝕋 (right-unit-law-add-𝕋 (succ-𝕋 k))
Successor laws for addition of truncation levels
left-successor-law-add-𝕋 : (n k : 𝕋) → (succ-𝕋 (succ-𝕋 (succ-𝕋 n))) +𝕋 k = succ-𝕋 (add-𝕋 (succ-𝕋 (succ-𝕋 n)) k) left-successor-law-add-𝕋 n neg-two-𝕋 = refl left-successor-law-add-𝕋 n (succ-𝕋 k) = refl right-successor-law-add-𝕋 : (k n : 𝕋) → k +𝕋 (succ-𝕋 (succ-𝕋 (succ-𝕋 n))) = succ-𝕋 (k +𝕋 (succ-𝕋 (succ-𝕋 n))) right-successor-law-add-𝕋 neg-two-𝕋 n = refl right-successor-law-add-𝕋 (succ-𝕋 neg-two-𝕋) n = refl right-successor-law-add-𝕋 (succ-𝕋 (succ-𝕋 k)) n = ap succ-𝕋 (right-successor-law-add-𝕋 (succ-𝕋 k) n)
Recent changes
- 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).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).