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 (λ j → λ { (i = i0) → C .paths x j ; (i = i1) → C .paths y j } ) (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 (λ k → λ { (i = i0) → h x (p j) k ; (i = i1) → h x (q j) k ; (j = i0) → h x x k ; (j = i1) → h x y k }) 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 (λ k → λ { (i = i0) → h₁ (h₁ x j) k ; (i = i1) → h₁ (h₂ x j) k ; (j = i0) → h₁ (h₁ c₂ i) k ; (j = i1) → h₁ x k }) 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