Truncations and truncated higher inductive types

Truncation is a homotopy-theoretic construction that given a space A and an integer n returns an n-truncated space \tau_{\le{}n}A together with a map p:A\to\tau_{\le{}n}A 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. (\tau_{\le{}n}A is the free n-truncated space built from A).

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.

About these ads
This entry was posted in Code, Higher Inductive Types. Bookmark the permalink.

15 Responses to Truncations and truncated higher inductive types

  1. Mike Shulman says:

    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

    data truncation-index : Set where
      minus-two : truncation-index
      succ : truncation-index → truncation-index
    

    and

    data sphere-index : Set where
      minus-one : sphere-index
      succ : sphere-index → sphere-index
    

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

  2. Peter Divianszky says:

    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.

      • Peter Divianszky says:

        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.

          • Peter Divianszky says:

            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?

              • Peter Divianszky says:

                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.

      • Mike Shulman says:

        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.

        • 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.

        • Mike Shulman says:

          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”.

        • 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].

        • Mike Shulman says:

          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.

        • > 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.

        • Mike Shulman says:

          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 which n appears to come from the dimension of a Euclidean space, but never, to my knowledge, instantiate n with any actual natural number. One could say something like “higher inductive truncated type”, I suppose.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s