Martin Escardo 1st May 2020.

This is ported from the Midlands Graduate School 2019 lecture notes

https://www.cs.bham.ac.uk/~mhe/HoTT-UF.in-Agda-Lecture-Notes/HoTT-UF-Agda.html
https://github.com/martinescardo/HoTT-UF.Agda-Lecture-Notes

\begin{code}

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

module MGS.hlevels where

open import MGS.Basic-UF public

_is-of-hlevel_ : π€ Μ β β β π€ Μ
X is-of-hlevel 0        = is-singleton X
X is-of-hlevel (succ n) = (x x' : X) β ((x οΌ x') is-of-hlevel n)

wconstant : {X : π€ Μ } {Y : π₯ Μ } β (X β Y) β π€ β π₯ Μ
wconstant f = (x x' : domain f) β f x οΌ f x'

wconstant-endomap : π€ Μ β π€ Μ
wconstant-endomap X = Ξ£ f κ (X β X), wconstant f

wcmap : (X : π€ Μ ) β wconstant-endomap X β (X β X)
wcmap X (f , w) = f

wcmap-constancy : (X : π€ Μ ) (c : wconstant-endomap X)
β wconstant (wcmap X c)
wcmap-constancy X (f , w) = w

Hedberg : {X : π€ Μ } (x : X)
β ((y : X) β wconstant-endomap (x οΌ y))
β (y : X) β is-subsingleton (x οΌ y)

Hedberg {π€} {X} x c y p q =

p                         οΌβ¨ a y p β©
(f x (refl x))β»ΒΉ β f y p  οΌβ¨ ap (Ξ» - β (f x (refl x))β»ΒΉ β -) (ΞΊ y p q) β©
(f x (refl x))β»ΒΉ β f y q  οΌβ¨ (a y q)β»ΒΉ β©
q                         β

where
f : (y : X) β x οΌ y β x οΌ y
f y = wcmap (x οΌ y) (c y)

ΞΊ : (y : X) (p q : x οΌ y) β f y p οΌ f y q
ΞΊ y = wcmap-constancy (x οΌ y) (c y)

a : (y : X) (p : x οΌ y) β p οΌ (f x (refl x))β»ΒΉ β f y p
a x (refl x) = (β»ΒΉ-leftβ (f x (refl x)))β»ΒΉ

wconstant-οΌ-endomaps : π€ Μ β π€ Μ
wconstant-οΌ-endomaps X = (x y : X) β wconstant-endomap (x οΌ y)

sets-have-wconstant-οΌ-endomaps : (X : π€ Μ ) β is-set X β wconstant-οΌ-endomaps X
sets-have-wconstant-οΌ-endomaps X s x y = (f , ΞΊ)
where
f : x οΌ y β x οΌ y
f p = p

ΞΊ : (p q : x οΌ y) β f p οΌ f q
ΞΊ p q = s x y p q

types-with-wconstant-οΌ-endomaps-are-sets : (X : π€ Μ )
β wconstant-οΌ-endomaps X β is-set X

types-with-wconstant-οΌ-endomaps-are-sets X c x = Hedberg x
(Ξ» y β wcmap (x οΌ y) (c x y) ,
wcmap-constancy (x οΌ y) (c x y))

subsingletons-have-wconstant-οΌ-endomaps : (X : π€ Μ )
β is-subsingleton X
β wconstant-οΌ-endomaps X

subsingletons-have-wconstant-οΌ-endomaps X s x y = (f , ΞΊ)
where
f : x οΌ y β x οΌ y
f p = s x y

ΞΊ : (p q : x οΌ y) β f p οΌ f q
ΞΊ p q = refl (s x y)

subsingletons-are-sets : (X : π€ Μ ) β is-subsingleton X β is-set X
subsingletons-are-sets X s = types-with-wconstant-οΌ-endomaps-are-sets X
(subsingletons-have-wconstant-οΌ-endomaps X s)

singletons-are-sets : (X : π€ Μ ) β is-singleton X β is-set X
singletons-are-sets X = subsingletons-are-sets X β singletons-are-subsingletons X

π-is-set : is-set π
π-is-set = subsingletons-are-sets π π-is-subsingleton

π-is-set : is-set π
π-is-set = subsingletons-are-sets π π-is-subsingleton

subsingletons-are-of-hlevel-1 : (X : π€ Μ )
β is-subsingleton X
β X is-of-hlevel 1

subsingletons-are-of-hlevel-1 X = g
where
g : ((x y : X) β x οΌ y) β (x y : X) β is-singleton (x οΌ y)
g t x y = t x y , subsingletons-are-sets X t x y (t x y)

types-of-hlevel-1-are-subsingletons : (X : π€ Μ )
β X is-of-hlevel 1
β is-subsingleton X

types-of-hlevel-1-are-subsingletons X = f
where
f : ((x y : X) β is-singleton (x οΌ y)) β (x y : X) β x οΌ y
f s x y = center (x οΌ y) (s x y)

sets-are-of-hlevel-2 : (X : π€ Μ ) β is-set X β X is-of-hlevel 2
sets-are-of-hlevel-2 X = g
where
g : ((x y : X) β is-subsingleton (x οΌ y)) β (x y : X) β (x οΌ y) is-of-hlevel 1
g t x y = subsingletons-are-of-hlevel-1 (x οΌ y) (t x y)

types-of-hlevel-2-are-sets : (X : π€ Μ ) β X is-of-hlevel 2 β is-set X
types-of-hlevel-2-are-sets X = f
where
f : ((x y : X) β (x οΌ y) is-of-hlevel 1) β (x y : X) β is-subsingleton (x οΌ y)
f s x y = types-of-hlevel-1-are-subsingletons (x οΌ y) (s x y)

hlevel-upper : (X : π€ Μ ) (n : β) β X is-of-hlevel n β X is-of-hlevel (succ n)
hlevel-upper X zero = Ξ³
where
Ξ³ : is-singleton X β (x y : X) β is-singleton (x οΌ y)
Ξ³ h x y = p , subsingletons-are-sets X k x y p
where
k : is-subsingleton X
k = singletons-are-subsingletons X h

p : x οΌ y
p = k x y

hlevel-upper X (succ n) = Ξ» h x y β hlevel-upper (x οΌ y) n (h x y)

_has-minimal-hlevel_ : π€ Μ β β β π€ Μ
X has-minimal-hlevel 0        = X is-of-hlevel 0
X has-minimal-hlevel (succ n) = (X is-of-hlevel (succ n)) Γ Β¬ (X is-of-hlevel n)

_has-minimal-hlevel-β : π€ Μ β π€ Μ
X has-minimal-hlevel-β = (n : β) β Β¬ (X is-of-hlevel n)

pointed-types-have-wconstant-endomap : {X : π€ Μ } β X β wconstant-endomap X
pointed-types-have-wconstant-endomap x = ((Ξ» y β x) , (Ξ» y y' β refl x))

empty-types-have-wconstant-endomap : {X : π€ Μ } β is-empty X β wconstant-endomap X
empty-types-have-wconstant-endomap e = (id , (Ξ» x x' β !π (x οΌ x') (e x)))

decidable-has-wconstant-endomap : {X : π€ Μ } β decidable X β wconstant-endomap X
decidable-has-wconstant-endomap (inl x) = pointed-types-have-wconstant-endomap x
decidable-has-wconstant-endomap (inr e) = empty-types-have-wconstant-endomap e

hedberg-lemma : {X : π€ Μ } β has-decidable-equality X β wconstant-οΌ-endomaps X
hedberg-lemma {π€} {X} d x y = decidable-has-wconstant-endomap (d x y)

hedberg : {X : π€ Μ } β has-decidable-equality X β is-set X
hedberg {π€} {X} d = types-with-wconstant-οΌ-endomaps-are-sets X (hedberg-lemma d)

β-is-set : is-set β
β-is-set = hedberg β-has-decidable-equality

π-is-set : is-set π
π-is-set = hedberg π-has-decidable-equality

\end{code}