Truncation levels
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-09-10.
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-ℕ
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-𝕋
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-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).
- 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).