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}