This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Truncation levels

module foundation-core.truncation-levels where
Imports 
open import foundation.universe-levels

Idea

The type of truncation levels is a type similar to the type of natural numbers, but starting the count at -2, so that sets have truncation level 0.

Definitions

The type of truncation levels

data 𝕋 : UU lzero where
  neg-two-𝕋 : 𝕋
  succ-𝕋 : 𝕋 → 𝕋

Aliases for common truncation levels

neg-one-𝕋 : 𝕋
neg-one-𝕋 = succ-𝕋 neg-two-𝕋

zero-𝕋 : 𝕋
zero-𝕋 = succ-𝕋 neg-one-𝕋

one-𝕋 : 𝕋
one-𝕋 = succ-𝕋 zero-𝕋

two-𝕋 : 𝕋
two-𝕋 = succ-𝕋 one-𝕋