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
$n$
as *homotopy
$(n-2)$-types*.
For instance: βThe sets are the homotopy 0-typesβ. The use of the
$-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

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 = 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 $n$, then itβs automatically of h-level $k+n$, for any $k$. 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

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:

contractible-if-inhabited : β {β} {A : Type β} β (A β is-contr A) β is-prop A contractible-if-inhabited cont x y = is-contrβis-prop (cont x) 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 \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 $A$ 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 $A$ is an n-type, then paths in $A$ are also $n$-types. This is because, by definition, the paths in a $n$-type are β$(n-1)$-typesβ, which is-hlevel-suc extends into $n$-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 _ _ Path-p-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 Path-p-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 = record { centre = hβ cβ 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

# 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