truncated higher inductive type

Truncations and truncated higher inductive types

Truncation is a homotopy-theoretic construction that given a space and an integer n returns an n-truncated space together with a map in an universal way. More precisely, if i is the inclusion of n-truncated spaces into spaces, then n-truncation is left adjoint to i. ( is the free n-truncated space built from ).

Moreover, the notion of truncated object is something already known in homotopy type theory: a type is n-truncated precisely if it is of h-level n+2.

Truncations are very useful in homotopy theory, and are also useful for foundations of mathematics, especially for n=-1,0:

• The (-1)-truncation is also known as isinhab: given a type A it returns a proposition isinhab A which is true if and only if A is inhabited (by “proposition” and “set” I will always mean “h-proposition” and “h-set”). This has already been considered by Vladimir Voevodsky here, where isinhab A is defined using impredicative quantification and resizing rules, and this is also present in the Coq HoTT library here where isinhab is defined using higher inductive types.
• The 0-truncation of a space is the set of its connected components. This allows us, among other things, to build initial algebras by generators and relations and to build quotients of sets by (prop valued) equivalence relations.

The aim of this post is to explain how to define n-truncations for every n using higher inductive types and how to use 0-truncations to construct free algebras for algebraic theories (free groups, for instance). Everything has been formalized in Agda, and the code is available in my GitHub repository here.

Preliminary remarks and definitions

In the HoTT library, the (-1)-truncation is defined by the following higher inductive type (translated in Agda notation):

data isinhab {i : Level} (A : Set i) : Set i where
  inhab : A → isinhab A
  inhab-path : (x y : isinhab A) → x ≡ y

A few remarks about Agda:

• Level is the type of universe levels. Here I’m quantifying over every universe level i and over every type A in the ith universe.
• The Set keyword in Agda corresponds to Type in Coq. It has nothing to do with the Set of Coq nor with sets in HoTT (the name clash is a bit unfortunate, perhaps we should rename Set to Type or even to Space)
• I’m using ≡ for propositional equality / identity types / path types / …

This definition means roughly that in order to obtain isinhab A, we start from A, we add paths between all pairs of elements of A, then paths between all pairs of the elements we just added, and so on transfinitely until it stabilizes, and then what we get is exactly isinhab A.

It is not very difficult to prove that isinhab A is a proposition and to prove its universal property (if P is a proposition then the map (isinhab A → P) → (A → P) given by pre-composition with inhab is an equivalence).

In a similar way, we could define the 0-truncation with the following higher inductive type:

data π₀ {i : Level} (A : Set i) : Set i where
  π₀-proj : A → π₀ A
  π₀-path : (x y : π₀ A) (p q : x ≡ y) → p ≡ q

Here we add paths between every all pairs of parallel paths (transfinitely) in order to fill all 1-dimensional holes.

While this is probably a perfectly correct definition, there are a few technical issues with it:

• It involves 2-dimensional path constructors, and I don’t know how to work with higher dimensional path constructors
• It does not seem easy to generalize this definition to an arbitrary n because I don’t know how to define towers of nested identity types cleanly.

So instead of using this definition, I will use another definition easily generalizable to every n and involving only 1-dimensional path constructors.

Definition of the truncation

The idea is that to define the (-1)-truncation, we filled every map from the 0-dimensional sphere (the disjoint union of two points) to the (-1)-truncation. Hence, we will define the n-truncation of A as the higher inductive type containing A and such that every (n+1)-sphere is filled.

We first need to define the spheres. Given a space A, the suspension of A is the space with two points n and s and a path from n to s for every point of A. In particular, the suspension of the n-sphere is the (n+1)-sphere.

So we define the following higher inductive type:

data suspension {i : Level} (A : Set i) : Set i where
  north : suspension A
  south : suspension A
  paths : A → (north A ≡ south A)

And the spheres are defined by induction with

Sⁿ : ℕ → Set
Sⁿ O = ⊥
Sⁿ (S n) = suspension (Sⁿ n)

where

data ⊥ : Set where

is the empty inductive type.

Note that Sⁿ O is the (-1)-dimensional sphere and in general Sⁿ n is the (n-1)-dimensional sphere. This numbering may look odd, but it has the advantage that filling n-spheres gives (hlevel n)-truncation, which is easy to remember.

We can now define the truncation with the following higher inductive type:

data τ {i : Level} (n : ℕ) (A : Set i) : Set i where
  proj : A → τ n A
  top  : (f : Sⁿ n → τ n A) → τ n A
  rays : (f : Sⁿ n → τ n A) (x : Sⁿ n) → top f ≡ f x

The last two constructors say that for every map f from Sⁿ n to τ n A, you can find a filling of f, where top f is the center and the rays f x are rays from top f to every point x in the sphere in τ n A (see the pictures in Peter Lumsdaine’s blog post here to get the idea).

We could now prove the universal property of the truncation, but actually the story does not end here.

Indeed, the truncation alone is not enough to build free algebras for every algebraic theory. The reason is that sometimes (when there are operations of infinite arity, for instance) we have to build the free algebra inductively and truncate it at the same time. Doing one after the other will not work. See also Mike Shulman’s comment here about this issue.

Moreover, type theorists do not use universal properties but dependent eliminators. Both should be equivalent, but for instance when you want to prove something about every point of a truncated higher inductive type, you will want a dependent eliminator.

Truncated higher inductive types

We want more than truncations, we want a notion of truncated higher inductive type (a higher inductive type which is also truncated at the same time). The idea is just to add the constructors top and rays to any higher inductive definition:

data n-truncated-HIT : Set where
  -- point constructors
  […]

  -- path constructors
  […]

  -- truncation constructors
  top-truncated-HIT  : (f : Sⁿ n → n-truncated-HIT) → n-truncated-HIT
  rays-truncated-HIT : (f : Sⁿ n → n-truncated-HIT) (x : Sⁿ n) → top f ≡ f x

For instance, if A is a set here is a definition of the free group on A (see here)

data freegroup : Set where
  e     : freegroup
  _·_   : A → freegroup → freegroup
  _⁻¹·_ : A → freegroup → freegroup

  right-inverse-· : (x : A) (u : freegroup) → x · (x ⁻¹· u) ≡ u
  left-inverse-·  : (x : A) (u : freegroup) → x ⁻¹· (x · u) ≡ u

  top  : (f : Sⁿ 2 → freegroup) → freegroup
  rays : (f : Sⁿ 2 → freegroup) (x : Sⁿ 2) → top f ≡ f x

(note that ⁻¹· is a single (infix) symbol)

And if R : A → A → Set is such that R x y is a proposition for every x y : A here is the quotient of A by the equivalence relation generated by R (see here)

data quotient : Set where
  proj : A → quotient
  eq : (x y : A) (_ : R x y) → proj x ≡ proj y

  top  : (f : Sⁿ 2 → quotient) → quotient
  rays : (f : Sⁿ 2 → quotient) (x : Sⁿ 2) → top f ≡ f x

Truncation is also just a special case of truncated higher inductive types.

New elimination rules

The nondependent elimination rule of the general truncated higher inductive type n-truncated-HIT above is the following:

n-truncated-HIT-rec-nondep : ∀ {i} (B : Set i)
  (…) -- usual premisses for points constructors
  (…) -- usual premisses for paths constructors
  (top* :  (f : Sⁿ n → n-truncated-HIT) (p : Sⁿ n → B) → B)
  (rays* : (f : Sⁿ n → n-truncated-HIT) (p : Sⁿ n → B) (x : Sⁿ n) → top* f p ≡ p x)
  → (n-truncated-HIT → B)

and the dependent elimination rule is

n-truncated-HIT-rec : ∀ {i} (P : n-truncated-HIT → Set i)
  (…) -- usual dependent premisses for points constructors
  (…) -- usual dependent premisses for paths constructors
  (top* :  (f : Sⁿ n → n-truncated-HIT) (p : (x : Sⁿ n) → P (f x)) → P (top f))
  (rays* : (f : Sⁿ n → n-truncated-HIT) (p : (x : Sⁿ n) → P (f x)) (x : Sⁿ n)
             → transport P (rays f x) (top* f p) ≡ p x)
  → ((t : n-truncated-HIT) → P t)

But these rules are not very easy to use, so we want the following elimination rules instead:

n-truncated-HIT-rec-nondep-new : ∀ {i} (B : Set i)
  (…) -- usual premisses for points constructors
  (…) -- usual premisses for paths constructors
  (p : is-hlevel n B)
  → (n-truncated-HIT → B)

n-truncated-HIT-rec-new : ∀ {i} (P : n-truncated-HIT → Set i)
  (…) -- usual dependent premisses for points constructors
  (…) -- usual dependent premisses for paths constructors
  (p : (x : n-truncated-HIT) → is-hlevel n (P x))
  → ((t : n-truncated-HIT) → P t)

The complicated hypotheses about the truncation constructors have been replaced by the simple fact that the fibration or the type we’re eliminating into is also truncated. These rules apply less often that the previous rules, but are nevertheless sufficient to prove everything that we want to prove.

So I proved the following in TruncatedHIT.agda:

• If a type has n-spheres filled, then it is of hlevel n
• If a type is of h-level n, then every n-sphere can be filled (meaning that the nondependent top* and rays* are satisfied)
• More generally, if a dependent type has all its fibers of h-level n, then the dependent top* and rays* are satisfied.

The first property shows that a truncated higher inductive type is indeed truncated, and the last two properties are used to build the new elimination rules from the old ones for any truncated higher inductive type.

If someone is interested I can explain the proofs in another post, but this one is already long enough.