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 nn-categories in a given universe β„“\ell assembles into an (n+1)(n+1)-category in the successor universe 1+β„“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 nn-types is a (n+1)(n+1)-type in 1+β„“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 AA and BB are nn-types, then so is the type of equivalences A≃BA \simeq B. For the case where nn is a successor, this only depends on the h-level of BB.

_ = 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 xx to the centre of contraction of BB, 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≃BA \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 AA has the given h-level. This is because, for nβ‰₯1n \ge 1, A≃BA \simeq B has the same h-level as Aβ†’BA \to B, which is the same as BB.

≃-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≑YX ≑ Y is equivalent to X≃YX \simeq Y. Since the latter is of h-level nn when XX and YY are nn-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+1n+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≃YX \simeq Y when YY is an nn-type, we know that nn-Type is a (n+1)(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 _)