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 as homotopy -types. For instance: βThe sets are the homotopy 0-typesβ. The use of the 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
- 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 , then itβs automatically of h-level , for any . 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
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 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
is an n-type, then paths in
are also
-types.
This is because, by definition, the paths in a
-type
are
β-typesβ,
which is-hlevel-suc
extends into
-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.) Path
s for any two elements, we
have PathP
s. 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