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`i`

^{th}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.

Very nice!! It’s great to see this all worked out precisely. I wish you would change the name of your “spheres” type, though; the numbering of spheres in homotopy theory is standard and I think we shouldn’t try to change it.

This sort of thing that happens with the numbering of spheres and of hlevels kind of makes me want to define types like

and

which are isomorphic copies of nat, but starting at -2 and -1 respectively. Probably that would be a dumb thing to actually do, though.

It is not directly connected to this post, but I would like to understand your syntax.

Could you help me, would the following be a correct definition of positive natural numbers?

data ℕ⁺ : Set where

one : ℕ⁺

_+_ : ℕ⁺ → ℕ⁺ → ℕ⁺

assoc : (m n k : ℕ⁺) → (m + n) + k ≡ m + (n + k)

If you interpret this as a usual higher inductive type, then it’s not a correct definition because there are two different ways to prove that `((one + one) + one) + one` is equal to `one + (one + (one + one))` (the pentagon), hence the type you have defined is not an h-set, there are coherence conditions missing.

But if you consider the 2-truncated higher inductive type (where 2 stands for h-level 2, i.e. h-set) with the same specification, then it becomes a correct definition of the positive natural numbers and you can prove that this type is equivalent to the usual type of positive natural numbers.

Thanks, then the example is more relevant that I thought.

Is this the correct definition then?

data ℕ⁺ : Set where

one : ℕ⁺

_+_ : ℕ⁺ → ℕ⁺ → ℕ⁺

assoc : (m n k : ℕ⁺) → (m + n) + k ≡ m + (n + k)

top : (f : Sⁿ 2 → ℕ⁺) → ℕ⁺

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

Yes, but I would just write something like the following

(2)data ℕ⁺ : Set where

one : ℕ⁺

_+_ : ℕ⁺ → ℕ⁺ → ℕ⁺

assoc : (m n k : ℕ⁺) → (m + n) + k ≡ m + (n + k)

where the “(2)data” means that you are taking a 2-truncated higher inductive type.

The fact that you can implement it in ordinary HIT using these top and rays constructors looks more like an implementation detail to me. In practice I’m not sure you will ever want to use the elimination rule given by the constructors top and rays, but rather the elimination rule of truncated higher inductive types.

Nice!

Is there any plan to support this in Agda? Is it related to “Towards A Higher Dimensional in Type Theory: The Case of Parametricity (by Jean-Philippe Bernardy)” seen on AIMXVI?

The computational behaviour of higher inductive types is largely not studied so it will probably not be supported in Agda before some time.

I haven’t been at AIMXVI so I don’t know about this, is there a way to find something about this talk online?

Ok, I see.

About the possibly related work: now I think it’s unrelated. Anyway, you can search for

“Type-Theory in ColorJ.-P. Bernardy” to get a paper about it.

Please don’t say “n-truncated” to mean “h-level n”!! The standard definition in homotopy theory and higher category theory is that “n-truncated” means “h-level (n+2)”. In particular, h-sets are 0-truncated. If we start mixing up the words that indicate which indexing conventions we’re using, then we’ll never be able to communicate.

> To be honest, I’m still not entirely sold on the whole h-level renumbering-things-to-start-at-zero idea

Me neither, but that’s still very convenient when writing code.

But actually your idea to have a

`truncation-index`

type is perhaps not so bad. In Coq you could add a coercion from`nat`

to`truncation-index`

and then you could write`truncation 0 A`

when you want the 0-truncation and`truncation (succ minus-two) A`

when you want the (-1)-truncation.Induction on the truncation-index would use different constructors but that’s not a big deal.

Am I missing something ?

> What about my suggestion of “higher inductive n-type” ?

Yes, that looks good. But how do you call the general concept of “higher inductive n-type” for an arbitrary n (what I call “truncated higher inductive type”)? It looks a bit strange to me to have a free variable here but perhaps it’s not.

I agree, it is a little strange to have a free variable there. Not without precedent in mathematics, though: for instance, topologists talk about something called “

n-duality” in whichnappears to come from the dimension of a Euclidean space, but never, to my knowledge, instantiatenwith any actual natural number. One could say something like “higher inductive truncated type”, I suppose.I completely agree, but unfortunately there is no adjective for “being of h-level n”. I probably should have said “0-truncated” though, but then the “2” seems strange.

I think in English, it’s fine to use “h-level n” as an adjective, e.g. “an h-level n type”.

Alternatively, you could just write 0 instead of 2 everywhere. I like to say “n-type” for “n-truncated type” which matches in indexing the homotopy-theorists’ notion of “homotopy n-type”, so that this would be a “higher inductive 0-type”.

I’m uncomfortable about having only a single letter “h” be the harbinger of an off-by-two error. (To be honest, I’m still not entirely sold on the whole h-level renumbering-things-to-start-at-zero idea.)

And how does that solve your problem anyway? Saying “an n-htruncated HIT” still doesn’t tell you whether it’s an HIT that just happens to be h-level n, or whether you’ve manually forced it to be h-level n.

What about my suggestion of “higher inductive n-type” (with n as for truncations)? That could unambiguously mean one which is forced to be n-truncated, whereas “an n-truncated HIT” would be one which just happens to be n-truncated.

Actually that’s not really an adjective that I want, but an adjectival passive present participle, because I don’t want to say that the higher inductive type happens to be truncated but that it is in the process of being truncated.

Unfortunately a lot of languages (including English and French) do not distinguish between passive present participle and passive past participle so the same word “truncated” is used for something which happens to be truncated and for something that is currently being truncated.

But using “h-level n” as an adjective does not carry this meaning at all, it just means that the type happens to be of h-level n.

What about the following? When using homotopy-theoretic terminology we stick with homotopy-theoretic numbering (so 0-truncated for truncation down to h-sets), and in the code or when we really want to use the h-level numbering, we add an extra “h” in front of everything. For instance [is-hconnected n A] is by definition [is-contr (htrunc n A)] where [htrunc n A] is truncation down to h-level [n].