```{-# OPTIONS --without-K #-}

open import lib.Base
open import lib.PathGroupoid
open import lib.Relation

module lib.NType {i} where

{- Definition of contractible types and truncation levels -}

is-contr : Type i → Type i
is-contr A = Σ A (λ x → ((y : A) → x == y))

has-level : ℕ₋₂ → (Type i → Type i)
has-level ⟨-2⟩ A = is-contr A
has-level (S n) A = (x y : A) → has-level n (x == y)

is-prop = has-level ⟨-1⟩
is-set  = has-level ⟨0⟩

{- To be a mere proposition, it is sufficient that all points are equal -}

has-all-paths : Type i → Type i
has-all-paths A = (x y : A) → x == y

abstract
all-paths-is-prop : {A : Type i} → (has-all-paths A → is-prop A)
all-paths-is-prop {A} c x y = (c x y , canon-path) where

canon-path : {x y : A} (p : x == y) → c x y == p
canon-path {.y} {y} idp =
c y y               =⟨ lemma (! (c y y)) ⟩
(! (c y y)) ∙ c y y =⟨ !-inv-l (c y y) ⟩
idp ∎  where

lemma : {x y : A} (p : x == y) → c x y == p ∙ c y y
lemma idp = idp

{- Truncation levels are cumulative -}
abstract
raise-level : {A : Type i} (n : ℕ₋₂)
→ (has-level n A → has-level (S n) A)
raise-level ⟨-2⟩ q =
all-paths-is-prop (λ x y → ! (snd q x) ∙ snd q y)
raise-level (S n) q =
λ x y → raise-level n (q x y)

{- Having decidable equality is stronger that being a set -}

has-dec-eq : Type i → Type i
has-dec-eq A = Dec (_==_ :> Rel A i)

abstract
dec-eq-is-set : {A : Type i} → (has-dec-eq A → is-set A)
dec-eq-is-set {A} d x y = all-paths-is-prop UIP where

UIP : {x y : A} (p q : x == y) -> p == q
UIP {x} idp q with d x x | lemma q  where

T : {x y : A} → x == y → Type i
T {x} {y} p =
match (d x y) withl (λ b → match (d x x) withl (λ b' → p == ! b' ∙ b)
withr (λ _ → Lift Empty))
withr (λ _ → Lift Empty)

lemma : {x y : A} → (p : x == y) -> T p
lemma {x} idp with (d x x)
lemma idp | inl a = ! (!-inv-l a)
lemma idp | inr r = lift (r idp)

UIP idp q | inl a | p' = ! (!-inv-l a) ∙ (! p')
UIP idp q | inr r | _ = Empty-elim (r idp)

{- Relationships between levels -}

module _ {A : Type i} where
abstract
contr-has-all-paths : is-contr A → has-all-paths A
contr-has-all-paths c x y = ! (snd c x) ∙ snd c y

prop-has-all-paths : is-prop A → has-all-paths A
prop-has-all-paths c x y = fst (c x y)

inhab-prop-is-contr : A → is-prop A → is-contr A
inhab-prop-is-contr x₀ p = (x₀ , λ y → fst (p x₀ y))

inhab-to-contr-is-prop : (A → is-contr A) → is-prop A
inhab-to-contr-is-prop c = all-paths-is-prop \$
λ x y → ! (snd (c x) x) ∙ snd (c x) y

contr-has-level : {n : ℕ₋₂} → (is-contr A → has-level n A)
contr-has-level {n = ⟨-2⟩} p = p
contr-has-level {n = S n} p = raise-level n (contr-has-level p)

prop-has-level-S : {n : ℕ₋₂} → (is-prop A → has-level (S n) A)
prop-has-level-S {n = ⟨-2⟩} p = p
prop-has-level-S {n = S n} p = raise-level (S n) (prop-has-level-S p)

set-has-level-SS : {n : ℕ₋₂} → (is-set A → has-level (S (S n)) A)
set-has-level-SS {n = ⟨-2⟩} p = p
set-has-level-SS {n = S n} p = raise-level (S (S n)) (set-has-level-SS p)

contr-is-prop : is-contr A → is-prop A
contr-is-prop = contr-has-level

contr-is-set : is-contr A → is-set A
contr-is-set = contr-has-level

prop-is-set : is-prop A → is-set A
prop-is-set = prop-has-level-S

{- If [A] has level [n], then so does [x == y] for [x y : A] -}
=-preserves-level : (n : ℕ₋₂) {x y : A}
→ (has-level n A → has-level n (x == y))
=-preserves-level ⟨-2⟩ p = (contr-has-all-paths p _ _ , unique-path) where
unique-path : {u v : A} (q : u == v)
→ contr-has-all-paths p u v == q
unique-path idp = !-inv-l (snd p _)
=-preserves-level (S n) {x} {y} p = raise-level n (p x y)

=-preserves-set : {x y : A} → (is-set A → is-set (x == y))
=-preserves-set = =-preserves-level ⟨0⟩

=-preserves-prop : {x y : A} → (is-prop A → is-prop (x == y))
=-preserves-prop = =-preserves-level ⟨-1⟩

{- The type of paths from a fixed point is contractible -}
pathfrom-is-contr : (x : A) → is-contr (Σ A (λ t → x == t))
pathfrom-is-contr x = ((x , idp) , pathfrom-unique-path) where
pathfrom-unique-path : {u : A} (pp : Σ A (λ t → u == t)) → (u , idp) == pp
pathfrom-unique-path (u , idp) = idp

{- The type of paths to a fixed point is contractible -}
pathto-is-contr : (x : A) → is-contr (Σ A (λ t → t == x))
pathto-is-contr x = ((x , idp) , pathto-unique-path) where
pathto-unique-path : {u : A} (pp : Σ A (λ t → t == u)) → (u , idp) == pp
pathto-unique-path (u , idp) = idp

{-
If [B] is a fibration over a contractible type [A], then any point in any
fiber of [B] gives a section
-}
contr-has-section : ∀ {j} {A : Type i} {B : A → Type j}
→ (is-contr A → (x : A) → (u : B x) → Π A B)
contr-has-section {B = B} (x , p) x₀ y₀ t = transport B (! (p x₀) ∙ p t) y₀
```