module 1Lab.HLevel.Universe where
Universes of n-typesπ
A common phenomenon in higher category theory is that the collection of all -categories in a given universe assembles into an -category in the successor universe :
- 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 consisting of all -types is a -type in . 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 and are -types, then so is the type of equivalences . For the case where is a successor, this only depends on the h-level of .
β-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
to the centre of contraction of
,
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
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 has the given h-level. This is because, for , has the same h-level as , which is the same as .
β-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 is equivalent to . Since the latter is of h-level when and are -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
.
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 when is an -type, we know that -Type is a -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 _)