open import 1Lab.Path
open import 1Lab.Type

module 1Lab.HLevel where

h-LevelsπŸ”—

The β€œhomotopy level” (h-level for short) of a type is a measure of how truncated it is, where the numbering is offset by 2. Specifically, a (-2)-truncated type is a type of h-level 0. In another sense, h-level measures how β€œhomotopically interesting” a given type is:

  • The contractible types are maximally uninteresting because there is only one.

  • The only interesting information about a proposition is whether it is inhabited.

  • The interesting information about a set is the collection of its inhabitants.

  • The interesting information about a groupoid includes, in addition to its inhabitants, the way those are related by paths. As an extreme example, the delooping groupoid of a group – for instance, the circle – has uninteresting points (there’s only one), but interesting loops.

For convenience, we refer to the collection of types of h-level nn as homotopy (nβˆ’2)(n-2)-types. For instance: β€œThe sets are the homotopy 0-types”. The use of the βˆ’2-2 offset is so the naming here matches that of the HoTT book.

The h-levels are defined by induction, where the base case are the contractible types.

record is-contr {β„“} (A : Type β„“) : Type β„“ where
  constructor contr
  field
    centre : A
    paths : (x : A) β†’ centre ≑ x

open is-contr public

⊀-is-contr : is-contr ⊀
⊀-is-contr .centre = tt
⊀-is-contr .paths _ = refl

A contractible type is one for which the unique map X β†’ ⊀ is an equivalence. Thus, it has β€œone element”. This doesn’t mean that we can’t have β€œmultiple”, distinctly named, inhabitants of the type; It means any inhabitants of the type must be connected by a path, and this path must be picked uniformly.

module _ where
  data [0,1] : Type where
    ii0 : [0,1]
    ii1 : [0,1]
    seg : ii0 ≑ ii1

An example of a contractible type that is not directly defined as another name for ⊀ is the unit interval, defined as a higher inductive type.

  interval-contractible : is-contr [0,1]
  interval-contractible .centre = ii0
  interval-contractible .paths ii0 i = ii0
  interval-contractible .paths ii1 i = seg i
  interval-contractible .paths (seg i) j = seg (i ∧ j)

A type is (n+1)-truncated if its path types are all n-truncated. However, if we directly take this as the definition, the types we end up with are very inconvenient! That’s why we introduce this immediate step: An h-proposition, or proposition for short, is a type where any two elements are connected by a path.

is-prop : βˆ€ {β„“} β†’ Type β„“ β†’ Type _
is-prop A = (x y : A) β†’ x ≑ y

With this, we can define the is-hlevel predicate. For h-levels greater than zero, this definition results in much simpler types!

is-hlevel : βˆ€ {β„“} β†’ Type β„“ β†’ Nat β†’ Type _
is-hlevel A 0 = is-contr A
is-hlevel A 1 = is-prop A
is-hlevel A (suc n) = (x y : A) β†’ is-hlevel (Path A x y) n

Since types of h-level 2 are very common, they get a special name: h-sets, or just sets for short. This is justified because we can think of classical sets as being equipped with an equality proposition x=yx = y - having propositional paths is exactly the definition of is-set. The universe of all types that are sets, is, correspondingly, called Set.

is-set : βˆ€ {β„“} β†’ Type β„“ β†’ Type β„“
is-set A = is-hlevel A 2

Similarly, the types of h-level 3 are called groupoids.

is-groupoid : βˆ€ {β„“} β†’ Type β„“ β†’ Type β„“
is-groupoid A = is-hlevel A 3

private
  variable
    β„“ : Level
    A : Type β„“

Preservation of h-levelsπŸ”—

If a type is of h-level nn, then it’s automatically of h-level k+nk+n, for any kk. We first prove a couple of common cases that deserve their own names:

is-contr→is-prop : is-contr A → is-prop A
is-contrβ†’is-prop C x y i = hcomp (βˆ‚ i) Ξ» where
  j (i = i0) β†’ C .paths x j
  j (i = i1) β†’ C .paths y j
  j (j = i0) β†’ C .centre

is-contrβ†’extend : is-contr A β†’ (Ο† : I) (p : Partial Ο† A) β†’ A [ Ο† ↦ p ]
is-contr→extend C φ p = inS (hcomp φ
  Ξ» { j (Ο† = i1) β†’ C .paths (p 1=1) j
    ; j (j = i0) β†’ C .centre
    })

extendβ†’is-contr : (βˆ€ Ο† (p : Partial Ο† A) β†’ A [ Ο† ↦ p ]) β†’ is-contr A
extend→is-contr ext = contr (outS (ext i0 λ ())) λ x i → outS (ext i λ _ → x)

is-contr→is-set : is-contr A → is-set A
is-contrβ†’is-set C x y p q i j = outS (is-contrβ†’extend C (βˆ‚ i ∨ βˆ‚ j) Ξ» where
  (i = i0) β†’ p j
  (i = i1) β†’ q j
  (j = i0) β†’ x
  (j = i1) β†’ y)

SingletonP : βˆ€ {β„“} (A : I β†’ Type β„“) (a : A i0) β†’ Type _
SingletonP A a = Σ[ x ∈ A i1 ] PathP A a x

SinglP-is-contr : βˆ€ {β„“} (A : I β†’ Type β„“) (a : A i0) β†’ is-contr (SingletonP A a)
SinglP-is-contr A a .centre = _ , transport-filler (Ξ» i β†’ A i) a
SinglP-is-contr A a .paths (x , p) i = _ , Ξ» j β†’ fill A (βˆ‚ i) j Ξ» where
  j (i = i0) β†’ coe0β†’i A j a
  j (i = i1) β†’ p j
  j (j = i0) β†’ a

SinglP-is-prop : βˆ€ {β„“} {A : I β†’ Type β„“} {a : A i0} β†’ is-prop (SingletonP A a)
SinglP-is-prop = is-contr→is-prop (SinglP-is-contr _ _)

This enables another useful characterisation of being a proposition, which is that the propositions are precisely the types which are contractible when they are inhabited:

is-contr-if-inhabitedβ†’is-prop : βˆ€ {β„“} {A : Type β„“} β†’ (A β†’ is-contr A) β†’ is-prop A
is-contr-if-inhabited→is-prop cont x y = is-contr→is-prop (cont x) x y

is-propβˆ™β†’is-contr : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ A β†’ is-contr A
is-propβˆ™β†’is-contr prop x .centre = x
is-propβˆ™β†’is-contr prop x .paths y = prop x y

The proof that any contractible type is a proposition is not too complicated. We can get a line connecting any two elements as the lid of the square below:

This is equivalently the composition of sym (C .paths x) βˆ™ C.paths y - a path xβ†’yx \to y which factors through the centre. The direct cubical description is, however, slightly more efficient.

is-prop→is-set : is-prop A → is-set A
is-propβ†’is-set h x y p q i j = hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
  k (i = i0) β†’ h x (p j) k
  k (i = i1) β†’ h x (q j) k
  k (j = i0) β†’ h x x k
  k (j = i1) β†’ h x y k
  k (k = i0) β†’ x

The proof that any proposition is a set is slightly more complicated. Since the desired homotopy p ≑ q is a square, we need to describe a cube where the missing face is the square we need. I have painstakingly illustrated it here:

To set your perspective: You are looking at a cube that has a transparent front face. The front face has four x corners, and four Ξ» i β†’ x edges. Each double arrow pointing from the front face to the back face is one of the sides of the composition. They’re labelled with the terms in the hcomp for is-propβ†’is-set: For example, the square you get when fixing i = i0 is on top of the diagram. Since we have an open box, it has a lid β€” which, in this case, is the back face β€” which expresses the identification we wanted: p ≑ q.

With these two base cases, we can prove the general case by recursion:

is-hlevel-suc : βˆ€ {β„“} {A : Type β„“} (n : Nat) β†’ is-hlevel A n β†’ is-hlevel A (suc n)
is-hlevel-suc 0 x = is-contr→is-prop x
is-hlevel-suc 1 x = is-prop→is-set x
is-hlevel-suc (suc (suc n)) h x y = is-hlevel-suc (suc n) (h x y)

By another inductive argument, we can prove that any offset works:

is-hlevel-+ : βˆ€ {β„“} {A : Type β„“} (n k : Nat) β†’ is-hlevel A n β†’ is-hlevel A (k + n)
is-hlevel-+ n zero x    = x
is-hlevel-+ n (suc k) x = is-hlevel-suc _ (is-hlevel-+ n k x)

A very convenient specialisation of the argument above is that if AA is a proposition, then it has any non-zero h-level:

is-prop→is-hlevel-suc
  : βˆ€ {β„“} {A : Type β„“} {n : Nat} β†’ is-prop A β†’ is-hlevel A (suc n)
is-prop→is-hlevel-suc {n = zero} aprop = aprop
is-prop→is-hlevel-suc {n = suc n} aprop =
  is-hlevel-suc (suc n) (is-prop→is-hlevel-suc aprop)

Furthermore, by the upwards closure of h-levels, we have that if AA is an n-type, then paths in AA are also nn-types. This is because, by definition, the paths in a nn-type are β€œ(nβˆ’1)(n-1)-types”, which is-hlevel-suc extends into nn-types.

Path-is-hlevel : βˆ€ {β„“} {A : Type β„“} (n : Nat) β†’ is-hlevel A n β†’ {x y : A}
               β†’ is-hlevel (x ≑ y) n
Path-is-hlevel zero ahl =
  contr (is-contr→is-prop ahl _ _)
        λ x → is-prop→is-set (is-contr→is-prop ahl) _ _ _ x
Path-is-hlevel (suc n) ahl = is-hlevel-suc (suc n) ahl _ _

PathP-is-hlevel : βˆ€ {β„“} {A : I β†’ Type β„“} (n : Nat)
                 β†’ is-hlevel (A i1) n
                 β†’ {x : A i0} {y : A i1}
                 β†’ is-hlevel (PathP A x y) n
PathP-is-hlevel {A = A} n ahl {x} {y} =
  subst (Ξ» e β†’ is-hlevel e n) (sym (PathP≑Path A x y)) (Path-is-hlevel n ahl)

Path-is-hlevel' : (n : Nat) β†’ is-hlevel A (suc n) β†’ (x y : A) β†’ is-hlevel (x ≑ y) n
Path-is-hlevel' 0 ahl x y =
  contr (ahl x y) λ x → is-prop→is-set ahl _ _ _ x

Path-is-hlevel' (suc n) h x y = h x y

PathP-is-hlevel' : βˆ€ {β„“} {A : I β†’ Type β„“} (n : Nat)
                  β†’ is-hlevel (A i1) (suc n)
                  β†’ (x : A i0) (y : A i1)
                  β†’ is-hlevel (PathP A x y) n
PathP-is-hlevel' {A = A} n ahl x y =
  subst (Ξ» e β†’ is-hlevel e n) (sym (PathP≑Path A x y)) (Path-is-hlevel' n ahl _ _)

is-hlevel is a propositionπŸ”—

Perhaps surprisingly, β€œbeing of h-level n” is a proposition, for any n! To get an intuitive feel for why this might be true before we go prove it, I’d like to suggest an alternative interpretation of the proposition is-hlevel A n: The type A admits unique fillers for any n-cube.

A contractible type is one that has a unique point: It has a unique filler for the 0-cube, which is a point. A proposition is a type that admits unique fillers for 1-cubes, which are lines: given any endpoint, there is a line that connects them. A set is a type that admits unique fillers for 2-cubes, or squares, and so on.

Since these fillers are unique, if a type has them, it has them in at most one way!

is-contr-is-prop : is-prop (is-contr A)
is-contr-is-prop {A = A} (contr c₁ h₁) (contr cβ‚‚ hβ‚‚) i .centre = h₁ cβ‚‚ i
is-contr-is-prop {A = A} (contr c₁ h₁) (contr cβ‚‚ hβ‚‚) i .paths x j =
  hcomp (βˆ‚ i ∨ βˆ‚ j) Ξ» where
    k (i = i0) β†’ h₁ (h₁ x j) k
    k (i = i1) β†’ h₁ (hβ‚‚ x j) k
    k (j = i0) β†’ h₁ (h₁ cβ‚‚ i) k
    k (j = i1) β†’ h₁ x k
    k (k = i0) β†’ c₁

First, we prove that being contractible is a proposition. Next, we prove that being a proposition is a proposition. This follows from is-propβ†’is-set, since what we want to prove is that h₁ and hβ‚‚ always give homotopic paths.

is-prop-is-prop : is-prop (is-prop A)
is-prop-is-prop {A = A} h₁ hβ‚‚ i x y = is-propβ†’is-set h₁ x y (h₁ x y) (hβ‚‚ x y) i

Now we can prove the general case by the same inductive argument we used to prove h-levels can be raised:

is-hlevel-is-prop : βˆ€ {β„“} {A : Type β„“} (n : Nat) β†’ is-prop (is-hlevel A n)
is-hlevel-is-prop 0 = is-contr-is-prop
is-hlevel-is-prop 1 = is-prop-is-prop
is-hlevel-is-prop (suc (suc n)) x y i a b =
  is-hlevel-is-prop (suc n) (x a b) (y a b) i

is-hlevel-is-hlevel-suc : βˆ€ {β„“} {A : Type β„“} (k n : Nat) β†’ is-hlevel (is-hlevel A n) (suc k)
is-hlevel-is-hlevel-suc k n = is-prop→is-hlevel-suc (is-hlevel-is-prop n)

Dependent h-LevelsπŸ”—

In cubical type theory, it’s natural to consider a notion of dependent h-level for a family of types, where, rather than having (e.g.) Paths for any two elements, we have PathPs. Since dependent contractibility doesn’t make a lot of sense, this definition is offset by one to start at the propositions.

is-hlevel-dep : βˆ€ {β„“ β„“'} {A : Type β„“} β†’ (A β†’ Type β„“') β†’ Nat β†’ Type _

is-hlevel-dep B zero =
  βˆ€ {x y} (Ξ± : B x) (Ξ² : B y) (p : x ≑ y)
  β†’ PathP (Ξ» i β†’ B (p i)) Ξ± Ξ²

is-hlevel-dep B (suc n) =
  βˆ€ {a0 a1} (b0 : B a0) (b1 : B a1)
  β†’ is-hlevel-dep {A = a0 ≑ a1} (Ξ» p β†’ PathP (Ξ» i β†’ B (p i)) b0 b1) n

It’s sufficient for a type family to be of an h-level everywhere for the whole family to be the same h-level.

is-propβ†’pathp : βˆ€ {B : I β†’ Type β„“} β†’ ((i : I) β†’ is-prop (B i))
              β†’ (b0 : B i0) (b1 : B i1)
              β†’ PathP (Ξ» i β†’ B i) b0 b1
is-prop→pathp {B = B} hB b0 b1 = to-pathp (hB _ _ _)

The base case is turning a proof that a type is a proposition uniformly over the interval to a filler for any PathP.

is-hlevel→is-hlevel-dep
  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : A β†’ Type β„“'}
  β†’ (n : Nat) β†’ ((x : A) β†’ is-hlevel (B x) (suc n))
  β†’ is-hlevel-dep B n
is-hlevel→is-hlevel-dep zero hl α β p = is-prop→pathp (λ i → hl (p i)) α β
is-hlevel→is-hlevel-dep {A = A} {B = B} (suc n) hl {a0} {a1} b0 b1 =
  is-hlevel→is-hlevel-dep n (λ p → helper a1 p b1)
  where
    helper : (a1 : A) (p : a0 ≑ a1) (b1 : B a1)
           β†’ is-hlevel (PathP (Ξ» i β†’ B (p i)) b0 b1) (suc n)
    helper a1 p b1 =
      J (Ξ» a1 p β†’ βˆ€ b1 β†’ is-hlevel (PathP (Ξ» i β†’ B (p i)) b0 b1) (suc n))
        (Ξ» _ β†’ hl _ _ _) p b1

is-prop→squarep
  : βˆ€ {B : I β†’ I β†’ Type β„“} β†’ ((i j : I) β†’ is-prop (B i j))
  β†’ {a : B i0 i0} {b : B i0 i1} {c : B i1 i0} {d : B i1 i1}
  β†’ (p : PathP (Ξ» j β†’ B j i0) a c)
  β†’ (q : PathP (Ξ» j β†’ B i0 j) a b)
  β†’ (s : PathP (Ξ» j β†’ B i1 j) c d)
  β†’ (r : PathP (Ξ» j β†’ B j i1) b d)
  β†’ SquareP B p q s r
is-prop→squarep {B = B} is-propB {a = a} p q s r i j =
  hcomp (βˆ‚ j ∨ βˆ‚ i) Ξ» where
    k (j = i0) β†’ is-propB i j (base i j) (p i) k
    k (j = i1) β†’ is-propB i j (base i j) (r i) k
    k (i = i0) β†’ is-propB i j (base i j) (q j) k
    k (i = i1) β†’ is-propB i j (base i j) (s j) k
    k (k = i0) β†’ base i j
  where
    base : (i j : I) β†’ B i j
    base i j = transport (Ξ» k β†’ B (i ∧ k) (j ∧ k)) a

is-prop→pathp-is-contr
  : {A : I β†’ Type β„“} β†’ ((i : I) β†’ is-prop (A i))
  β†’ (x : A i0) (y : A i1) β†’ is-contr (PathP A x y)
is-prop→pathp-is-contr ap x y .centre = is-prop→pathp ap x y
is-prop→pathp-is-contr ap x y .paths p =
  is-prop→squarep (λ i j → ap j) refl _ _ refl

abstract
  is-set→squarep :
    {A : I β†’ I β†’ Type β„“}
    (is-set : (i j : I) β†’ is-set (A i j))
    β†’ {a : A i0 i0} {b : A i0 i1} {c : A i1 i0} {d : A i1 i1}
    β†’ (p : PathP (Ξ» j β†’ A j i0) a c)
    β†’ (q : PathP (Ξ» j β†’ A i0 j) a b)
    β†’ (s : PathP (Ξ» j β†’ A i1 j) c d)
    β†’ (r : PathP (Ξ» j β†’ A j i1) b d)
    β†’ SquareP A p q s r
  is-setβ†’squarep isset aβ‚€β‚‹ a₁₋ aβ‚‹β‚€ a₋₁ =
    transport (sym (PathP≑Path _ _ _))
              (PathP-is-hlevel' 1 (isset _ _) _ _ _ _)

-- Has to go through:
_ : βˆ€ {A : Type} {a b c d : A} (p : a ≑ c) (q : a ≑ b) (s : c ≑ d) (r : b ≑ d)
  β†’ Square p q s r ≑ SquareP (Ξ» _ _ β†’ A) p q s r
_ = Ξ» _ _ _ _ β†’ refl

is-set→cast-pathp
  : βˆ€ {β„“ β„“β€²} {A : Type β„“} {x y : A} {p q : x ≑ y} (P : A β†’ Type β„“β€²) {px : P x} {py : P y}
  β†’ is-set A
  β†’ PathP (Ξ» i β†’ P (p i)) px py
  β†’ PathP (Ξ» i β†’ P (q i)) px py
is-set→cast-pathp {p = p} {q = q} P {px} {py} set  r =
  coe0β†’1 (Ξ» i β†’ PathP (Ξ» j β†’ P (set _ _ p q i j)) px py) r