# Truncation levels

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-01-26.

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)


add-𝕋 : 𝕋 → 𝕋 → 𝕋
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 _+𝕋_


### 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-𝕋 (succ-𝕋 (succ-𝕋 neg-two-𝕋)) = refl
left-unit-law-add-𝕋 (succ-𝕋 (succ-𝕋 (succ-𝕋 k))) = refl

right-unit-law-add-𝕋 : (k : 𝕋) → k +𝕋 zero-𝕋 ＝ 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)