open import 1Lab.HLevel.Retracts
open import 1Lab.Type.Sigma
open import 1Lab.Univalence
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HLevel.Universe where

private variable
β : Level
A B C : Type β


# Universes of n-typesπ

A common phenomenon in higher category theory is that the collection of all $n$-categories in a given universe $\ell$ assembles into an $(n+1)$-category in the successor universe $1+\ell$:

• The collection of all sets (0-categories) is a (1-)-category;
• The collection of all (1-)categories is a 2-category;
• The collection of all 2-categories is a 3-category;

Because of the univalence axiom, the same phenomenon can be observed in homotopy type theory: The subuniverse of $\ell$ consisting of all $n$-types is a $(n+1)$-type in $1+\ell$. That means: the universe of propositions is a set, the universe of sets is a groupoid, the universe of groupoids is a bigroupoid, and so on.

## h-Levels of equivalencesπ

As warmup, we prove that if $A$ and $B$ are $n$-types, then so is the type of equivalences $A \simeq B$. For the case where $n$ is a successor, this only depends on the h-level of $B$.

_ = is-contr

β-is-hlevel : (n : Nat) β is-hlevel A n β is-hlevel B n β is-hlevel (A β B) n
β-is-hlevel {A = A} {B = B} zero Ahl Bhl = contr (f , f-eqv) deform where
f : A β B
f _ = Bhl .centre

f-eqv : is-equiv f
f-eqv = is-contrβis-equiv Ahl Bhl


For the zero case, weβre asked to give a proof of contractibility of A β B. As the centre we pick the canonical function sending $x$ to the centre of contraction of $B$, which is an equivalence because it is a map between contractible types.

By the characterisation of paths in Ξ£ and the fact that being an equivalence is a proposition, we get the required family of paths deforming any $A \simeq B$ to our f.

  deform : (g : A β B) β (f , f-eqv) β‘ g
deform (g , g-eqv) = Ξ£-path (Ξ» i x β Bhl .paths (g x) i)
(is-equiv-is-prop _ _ _)


As mentioned before, the case for successors does not depend on the proof that $A$ has the given h-level. This is because, for $n \ge 1$, $A \simeq B$ has the same h-level as $A \to B$, which is the same as $B$.

β-is-hlevel (suc n) _ Bhl =
Ξ£-is-hlevel (suc n)
(fun-is-hlevel (suc n) Bhl)
Ξ» f β is-propβis-hlevel-suc (is-equiv-is-prop f)


## h-Levels of pathsπ

Univalence states that the type $X β‘ Y$ is equivalent to $X \simeq Y$. Since the latter is of h-level $n$ when $X$ and $Y$ are $n$-types, then so is the former:

β‘-is-hlevel : (n : Nat) β is-hlevel A n β is-hlevel B n β is-hlevel (A β‘ B) n
β‘-is-hlevel n Ahl Bhl = equivβis-hlevel n ua univalenceβ»ΒΉ (β-is-hlevel n Ahl Bhl)


## Universesπ

We refer to the dependent sum of the family is-hlevel - n as n-Type:

record n-Type β n : Type (lsuc β) where
no-eta-equality
constructor el
field
β£_β£   : Type β
is-tr : is-hlevel β£_β£ n
infix 100 β£_β£
instance
H-Level-n-type : β {k} β H-Level β£_β£ (n + k)
H-Level-n-type = basic-instance n is-tr

open n-Type using (β£_β£ ; is-tr ; H-Level-n-type) public


Like mentioned in the introduction, the main theorem of this section is that n-Type is a type of h-level $n+1$. We take a detour first and establish a characterisation of paths for n-Type: Since is-tr is a proposition, paths in n-Type are determined by paths of the underlying types. By univalence, these correspond to equivalences of the underlying type:

n-path : {n : Nat} {X Y : n-Type β n} β β£ X β£ β‘ β£ Y β£ β X β‘ Y
n-path f i .β£_β£ = f i
n-path {n = n} {X} {Y} f i .is-tr =
is-propβpathp (Ξ» i β is-hlevel-is-prop {A = f i} n) (X .is-tr) (Y .is-tr) i

n-ua : {n : Nat} {X Y : n-Type β n} β β£ X β£ β β£ Y β£ β X β‘ Y
n-ua f = n-path (ua f)

n-univalence : {n : Nat} {X Y : n-Type β n} β (β£ X β£ β β£ Y β£) β (X β‘ Y)
n-univalence {n = n} {X} {Y} = n-ua , is-isoβis-equiv isic where
inv : β {Y} β X β‘ Y β β£ X β£ β β£ Y β£
inv p = pathβequiv (ap β£_β£ p)

linv : β {Y} β is-left-inverse (inv {Y}) n-ua
linv x = Ξ£-prop-path is-equiv-is-prop (funext Ξ» x β transport-refl _)

rinv : β {Y} β is-right-inverse (inv {Y}) n-ua
rinv = J (Ξ» y p β n-ua (inv p) β‘ p) path where
path : n-ua (inv {X} refl) β‘ refl
path i j .β£_β£ = ua.Ξ΅ {A = β£ X β£} refl i j
path i j .is-tr = is-propβsquarep
(Ξ» i j β is-hlevel-is-prop
{A = ua.Ξ΅ {A = β£ X β£} refl i j} n)
(Ξ» j β X .is-tr) (Ξ» j β n-ua {X = X} {Y = X} (pathβequiv refl) j .is-tr)
(Ξ» j β X .is-tr) (Ξ» j β X .is-tr)
i j

isic : is-iso n-ua
isic = iso inv rinv (linv {Y})


Since h-levels are closed under equivalence, and we already have an upper bound on the h-level of $X \simeq Y$ when $Y$ is an $n$-type, we know that $n$-Type is a $(n+1)$-type:

n-Type-is-hlevel : β n β is-hlevel (n-Type β n) (suc n)
n-Type-is-hlevel zero x y = n-ua
((Ξ» _ β y .is-tr .centre) , is-contrβis-equiv (x .is-tr) (y .is-tr))
n-Type-is-hlevel (suc n) x y =
is-hlevelβ (suc n) (n-univalence eβ»ΒΉ) (β-is-hlevel (suc n) (x .is-tr) (y .is-tr))


For 1-categorical mathematics, the important h-levels are the propositions and the sets, so they get short names:

Set : β β β Type (lsuc β)
Set β = n-Type β 2

Prop : β β β Type (lsuc β)
Prop β = n-Type β 1

n-Type-square
: β {β} {n}
β {w x y z : n-Type β n}
β {p : x β‘ w} {q : x β‘ y} {s : w β‘ z} {r : y β‘ z}
β Square (ap β£_β£ p) (ap β£_β£ q) (ap β£_β£ s) (ap β£_β£ r)
β Square p q s r
n-Type-square sq i j .β£_β£ = sq i j
n-Type-square {p = p} {q} {s} {r} sq i j .is-tr =
is-propβsquarep (Ξ» i j β is-hlevel-is-prop {A = sq i j} _)
(ap is-tr p) (ap is-tr q) (ap is-tr s) (ap is-tr r) i j

instance
H-Level-nType : β {n k} β H-Level (n-Type β k) (1 + k + n)
H-Level-nType {k = k} = basic-instance (1 + k) (n-Type-is-hlevel k)

H-Level-is-equiv
: β {β β'} {A : Type β} {B : Type β'} {f : A β B} {n}
β H-Level (is-equiv f) (suc n)
H-Level-is-equiv = prop-instance (is-equiv-is-prop _)