Martin Escardo, January 2019.

Minimal development of hlevels. For simplicity, for the moment we
assume univalence globally, although it is not necessary. Our
convention here is that propositions are at level zero (apologies).

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.Univalence

module UF.HLevels (ua : Univalence) where

open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.UA-FunExt

private
fe : FunExt
fe  = Univalence-gives-FunExt ua
fe' : Fun-Ext
fe' = Univalence-gives-Fun-Ext ua

_is-of-hlevel_ : 𝓤 ̇ → ℕ → 𝓤 ̇
X is-of-hlevel zero     = is-prop X
X is-of-hlevel (succ n) = (x x' : X) → (x ＝ x') is-of-hlevel n

hlevel-relation-is-prop : (n : ℕ) (X : 𝓤 ̇ ) → is-prop  (X is-of-hlevel n)
hlevel-relation-is-prop {𝓤} zero     X = being-prop-is-prop (fe 𝓤 𝓤)
hlevel-relation-is-prop {𝓤} (succ n) X =
Π₂-is-prop fe'
(λ x x' → hlevel-relation-is-prop {𝓤} n (x ＝ x'))

props-have-all-hlevels : (n : ℕ) (P : 𝓤 ̇ ) → is-prop P → P is-of-hlevel n
props-have-all-hlevels zero     P i = i
props-have-all-hlevels (succ n) P i = λ x x' → props-have-all-hlevels n (x ＝ x')
(props-are-sets i)

hlevels-closed-under-Σ : (n : ℕ)
→ (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
→ X is-of-hlevel n
→ ((x : X) → (Y x) is-of-hlevel n)
→ (Σ Y) is-of-hlevel n
hlevels-closed-under-Σ {𝓤} zero X Y l m = Σ-is-prop l m
hlevels-closed-under-Σ {𝓤} (succ n) X Y l m = γ
where
γ : (σ τ : Σ Y) → (σ ＝ τ) is-of-hlevel n
γ σ τ = transport⁻¹ (_is-of-hlevel n) a IH
where
a : (σ ＝ τ) ＝ (Σ p ꞉ pr₁ σ ＝ pr₁ τ , transport Y p (pr₂ σ) ＝ pr₂ τ)
a = eqtoid (ua 𝓤) _ _ Σ-＝-≃
IH : (Σ p ꞉ pr₁ σ ＝ pr₁ τ , transport Y p (pr₂ σ) ＝ pr₂ τ) is-of-hlevel n
IH = hlevels-closed-under-Σ n
(pr₁ σ ＝ pr₁ τ)
(λ p → transport Y p (pr₂ σ) ＝ pr₂ τ)
(l (pr₁ σ) (pr₁ τ))
(λ p → m (pr₁ τ) (transport Y p (pr₂ σ)) (pr₂ τ))

hlevels-closed-under-Π : (n : ℕ)
→ (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
→ ((x : X) → (Y x) is-of-hlevel n)
→ (Π Y) is-of-hlevel n
hlevels-closed-under-Π {𝓤} zero X Y m = Π-is-prop (fe 𝓤 𝓤) m
hlevels-closed-under-Π {𝓤} (succ n) X Y m = γ
where
γ : (f g : Π Y) → (f ＝ g) is-of-hlevel n
γ f g = transport⁻¹ (_is-of-hlevel n) a IH
where
a : (f ＝ g) ＝ (f ∼ g)
a = eqtoid (ua 𝓤) (f ＝ g) (f ∼ g) (≃-funext (fe 𝓤 𝓤) f g)
IH : (f ∼ g) is-of-hlevel n
IH = hlevels-closed-under-Π {𝓤} n X (λ x → f x ＝ g x) (λ x → m x (f x) (g x))

\end{code}

The subuniverse of types of hlevel n:

\begin{code}

ℍ : ℕ → (𝓤 : Universe) → 𝓤 ⁺ ̇
ℍ n 𝓤 = Σ X ꞉ 𝓤 ̇ , X is-of-hlevel n

\end{code}