module 1Lab.HLevel where

h-LevelsπŸ”—

When working in type theory, the mathematical activities of proving and constructing become intermingled, in a way that sometimes poses serious complications: The method by which a given statement was proven may be relevant in the future, since it is, at heart, a construction β€” of a term of type To tame this annoyance, an important pursuit in type theory is identifying the statements for which the construction can not matter. A simple example is equality between natural numbers: there is no further construction that could tell proofs of apart.

In a homotopy type theory, where a general type might have non-trivial identifications all the way up, it becomes very useful to state that, at some point, a given type stops having distinguishable constructions, and instead has a unique proof β€” for which we could substitute any other potential proof. We have already mentioned the example of the natural numbers: there are a lot of different natural numbers, but as soon as we have a pair if we have any then it’s as good as any other

At this point, we should introduce the proper terminology, rather than speaking of β€œproving” types and β€œconstructing” types. We say that a type is a proposition, written is-prop below, if any two of its inhabitants are identified. Since every construction is invariant under identifications (by definition), this means that any two putative constructions are indistinguishable β€” they’re really the same proof.

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

The information that a type is a proposition can also be seen as a form of induction principle: If is a proposition, and is a type family over then constructing a section can be done by showing for any at all. If we had this induction principle, then we could recover the notion of propositionality above by taking to be the family

subst-prop : βˆ€ {β„“ β„“'} {A : Type β„“} {P : A β†’ Type β„“'} β†’ is-prop A β†’ βˆ€ a β†’ P a β†’ βˆ€ b β†’ P b
subst-prop {P = P} prop a pa b = subst P (prop a b) pa

Keep in mind that, even if a type is a proposition, it might still be possible to project interesting data from a proof β€” but, were we to project this data from instead, we would get something identical. Propositions abound: the statement that is a proposition turns out to be one, for example, as is the statement that a function is an equivalence. Even though any two proofs that is an equivalence are interchangeable, if we’re given such a proof, we can project out the inverse β€” and there might be a lot of functions laying around!

Knowing about propositions, we can now rephrase our earlier statement about the natural numbers: each identity type is a proposition. Types for which this statement holds are called sets. A proof that a type is a set is a licence to stop caring about how we show that are identified β€” we even say that they’re just equal.

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

While it may seem unusual to ever explicitly ask whether a pair of proofs are identical, we might certainly end up in such a situation if we’re comparing larger structures! For example, if and are groups, then it makes perfect sense to ask whether homomorphisms are identical. But the data of a group homomorphism consists of a function between the types underlying each group, and a value in the type Knowing that a group has an underlying set means that this type is a proposition β€” this value is really a proof that preserves multiplication, and we do not have to care about it.

Since a set is defined to be a type whose identity types are propositions, it’s natural to ask: is there a name for a type whose identity types are sets? The answer is yes! These are called groupoids. We can extend this process recursively to ask about any natural number of iterated identity types. This is called the type’s h-level. If we’re thinking of a type as a space, and of the identifications as paths, then the statement β€œ has h-level ” tells you that the homotopy groups for are all zero.

Thinking about how much information carries, we could say that a proposition carries the information of whether it is true or false; a set carries the information of which inhabitant we’re looking at; a groupoid carries that, and, additionally, the set of symmetries of that inhabitant, and so on. From this perspective, there are types which are even less interesting β€” those that carry no information at all: the propositions we know are inhabited. In traditional foundations, we might call this a singleton; in homotopy type theory, we call them contractible.

Making the notion concrete, to say that is contractible means giving a point called the centre of contraction, and an operation that, given a point yields a path We will show below that every proposition is a set, which means that, since the identity types of a proposition are all pointed, they are all contractible. Thus, the contractible types naturally fit into the hierarchy of h-levels.

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

open is-contr public

We can now write down the definition of is-hlevel, as a function of the type and the specific level. Note that, even though that being a proposition is equivalent to having contractible identity types, we’ll define is-hlevel so that it agrees with our previous definition.

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

The recursive definition above agrees with is-set at level 2. We can also take this opportunity to define the groupoids as the types for which is-hlevel holds at level 3.

_ : is-set A ≑ is-hlevel A 2
_ = refl

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

The traditional numbering for h-levels says that the sets are at level zero, and that the propositions and contractible types are at negative levels (-1 and -2, respectively). While there is no mathematical benefit to using this numbering over starting at zero, there are social benefits. For example, the groupoids (at level 3) turn out to be the types underlying (univalent) 1-categories.

We will, therefore, sometimes use the historical numbering in prose. To clarify the distinction, we will say that a type is of h-level if is-hlevel T n holds and, when using the traditional numbering, we will say that is an , or is . For example, sets are of h-level but are or

ExamplesπŸ”—

We can now mention some examples of types at the various h-levels, to show that the notion is not vacuous. Starting at the contractible types, the most obvious example is the literal singleton β€” or rather, unit β€” type.

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

We have previously mentioned that path induction says that the singletons, in the sense of the subtype of identical to a given , are also contractible. Even though we have a shorter cubical proof (used in the definition of path induction), we can demonstrate the application of path induction:

_ : (a : A) β†’ is-contr (Ξ£[ b ∈ A ] (b ≑ a))
_ = Ξ» t β†’ record
  { centre = (t , refl)
  ; paths  = Ξ» (s , p) β†’ J' (Ξ» s t p β†’ (t , refl) ≑ (s , p)) (Ξ» t β†’ refl) p
  }

This provides an example of a type that is not literally defined to be of a certain h-level, but there are also geometric examples. One is the unit interval, defined as a higher inductive type, which has two points and a path between them.

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

Thinking geometrically, the construction of the contraction β€œfixes” the endpoint at zero, and β€œpulls in” the other endpoint; in the process, the path between them becomes trivial. We also have a direct cubical proof that this results in a contractible 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)

Propositions are setsπŸ”—

We have previously mentioned that being a proposition is a proposition, when applied to a specific type. We will show this by showing that every proposition is a set: since is-prop is then a (dependent) function valued in propositions, it’s also a proposition. Showing this in axiomatic homotopy type theory is slightly tricky, but showing it in cubical type theory is a remarkable application of lifting properties.

First, we’ll make the geometry of the problem clear: we’re given points and paths What we want to show, that is visualised as a square. In one dimension, say we have and and these are opposite faces in another dimension, say

Recall that, by fibrancy of we can obtain such a square by displaying it as the missing higher-dimensional face in some higher cube, then appealing to hcomp. As the base face, opposite to what we want in some new direction we choose the square that is constantly We then have to give terms filling the four boundary squares β€” these will turn out to be very similar. Let’s focus on the square.

The diagram below illustrates the setup: in addition to varying horizontally and varying vertically, we now have varying β€œfront to back”. At the face, we have the constantly square; at the boundary is the dashed square we’re looking for. The square is on the left, in red.

By abstracting over the dimension, we can think of the boundary of the red square as giving a path type β€” we’re looking to construct a path between and But since is a proposition, we have such a path! If we write for the witness that is-prop A, we find that we can fill the square by All of the other squares follow this same reasoning. You can see them in the code below.

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 (k = i0) β†’ x
  k (j = i0) β†’ h x x k
  k (j = i1) β†’ h x y k
  k (i = i0) β†’ h x (p j) k
  k (i = i1) β†’ h x (q j) k
For completeness, we can also diagram the solution above.

A minor snag, which is not relevant to the overall idea, is the boundary of the square we used for At we’re left with and not just Practically, this means that the filler of the top face can’t be since that wouldn’t agree with the left face on their shared edge; It has to be the odd-looking instead.

As an immediate application, we can show that defining the types of h-level to be the propositions, rather than asking for contractible identity types, does not make a difference in the setup:

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 = record
  { centre = ahl x y
  ; paths  = is-prop→is-set ahl _ _ _
  }
Path-is-hlevel' (suc n) h x y = h x y

Upwards closureπŸ”—

The proof that propositions are sets extends by induction to a proof that any is an However, recall we started the hierarchy with the contractible types, so that the propositions are not literally the base case. We’re still missing a proof that being contractible implies being a proposition. Since we have some cubical momentum going, it’s not hard to construct a homogeneous composition that expresses that contractible types are propositions:

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

Reading the code above as a diagram, we can see that this is precisely the composition of sym (C .paths x) with C .paths y. It would not have made any difference whether we used the pre-existing definition of path composition, but it’s always a good idea to practice writing hcomps.

With that base case, we can actually perform the inductive argument. A similar argument extends this to showing that any is a for any offset

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)

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 these arguments will allow us to lift a proof that is a proposition to a proof that it has any positive 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)

Finally, we’ll bootstrap some results about the closure of under various operations. Here, we can immediately show that the identity types of an are again

Path-is-hlevel
  : (n : Nat) β†’ is-hlevel A n
  β†’ {x y : A} β†’ is-hlevel (x ≑ y) n
Path-is-hlevel zero ahl = record
  { centre = is-contr→is-prop ahl _ _
  ; paths  = is-prop→is-set (is-contr→is-prop ahl) _ _ _
  }
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 y} β†’ 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)

Note that, while a contractible type is not literally defined to be a pointed proposition, these notions are equivalent. Indeed, if a type is contractible assuming it is pointed, it is a proposition, as the two arguments below show. This explains why propositions are sometimes referred to as contractible-if-inhabited, but we will not use this terminology.

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

Propositionality of truncatednessπŸ”—

With upwards closure out of the way, we can show that being a proposition is a proposition. We have already mentioned it, and gestured towards the proof: since every proposition is a set, any two functions must agree, pointwise, on any The code is similarly simple:

is-prop-is-prop : is-prop (is-prop A)
is-prop-is-prop α β i x y = is-prop→is-set α x y (α x y) (β x y) i

To show that being contractible is a proposition, we’ll use a similar argument. It will suffice to show that the centres of contraction are identical, and that, over this, we have an identification between the contractions. This has a delightfully short proof also:

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

Once again, we can extend this pair of base cases to the entire hierarchy, by an inductive argument of the same shape as the one we used for upwards closure.

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

Dependent h-levelsπŸ”—

When working in a homotopy type theory, we often have to consider, in addition to identity types, dependent identity types; in cubical type theory, these are the primitive notion, implemented by PathPs. Regardless, it makes sense to extend the notion of h-level to talk not only about identifications in a type, but about arbitrary dependent identifications in a family of types.

Rather than novelty, this notion of dependent h-level does turn out to have practical applications β€” except for the dependent analogue to contractibility. Therefore, we bootstrap this notion with the dependent propositions: A family over is a dependent proposition if any pair of elements are identified, over an arbitrary path in the base:

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

However, there is an emergent notion of h-level for families, namely, the pointwise lifting of the ordinary, non-dependent h-levels. While the notion we’ve just defined is more convenient to work with cubically, we’re led to wonder how it compares to the pointwise notion. Fortunately, they are equivalent.

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

The base case is usefully phrased as the helper lemma is-prop→pathp above: if we have a line of types over which is a proposition everywhere, then we can construct a PathP over between any points in the two fibres. The inductive case uses path induction to focus on a single fibre:

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

Contractibility, geometricallyπŸ”—

In cubical type theory, rather than reasoning algebraically about iterated identity types, we often prefer the more direct option of reasoning in a higher-dimensional context, using lifting problems. However, the notions of h-level we have defined all talk about these iterated identity types. There is a more natively cubical phrasing of contractiblity, which we now introduce, in terms of extensibility.

Suppose we have a partial element defined on some cofibration Does extend to a total element? If is contractible, yes! We have a base point the centre of contraction, and, taking as the shape of a lifting problem, we can certainly find a system of partial paths β€” is a proposition, after all!

is-contrβ†’extend : is-contr A β†’ (Ο† : I) (p : Partial Ο† A) β†’ A [ Ο† ↦ p ]
is-contrβ†’extend C Ο† p = inS do hcomp (Ο† ∨ ~ Ο†) Ξ» where
  j (j = i0) β†’ C .centre
  j (Ο† = i0) β†’ C .centre
  j (Ο† = i1) β†’ C .paths (p 1=1) j

Conversely, if we know that every partial element (with our choice of shape is extensible, we can prove that is contractible. The centre is given by extending the empty partial element, taking

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

To come up with a path connecting this empty extension and an we can extend the partial element that is when and undefined everywhere. On the left endpoint, when this is exactly the empty system we used above!

extend→is-contr ext .paths x i = outS (ext i λ _ → x)

We can use this to write a more direct proof that contractible types are sets, eliminating the passage through the proof that they are propositions.

is-contr→is-set : is-contr A → is-set A
is-contr→is-set C x y p q i j = outS do
  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 _ _)

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