Truncation levels
module foundation.truncation-levels where
Imports
open import foundation-core.truncation-levels public open import elementary-number-theory.natural-numbers open import foundation-core.functions 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)) infix 30 _+𝕋_ _+𝕋_ = 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)