In 2013, a consortium of the greatest mathematicians published a massive volume which reboots our conception of mathematics. Plus, in April 2014, Carnegie Mellon has received 7.5 million dollars from the Department of Defense to write the sequels of that book. In this article, we’ll dig into a new structure they’ve defined, which seems like a revolutionary and liberating breakthrough to me. This structure is that of **higher inductive types**, and it is the basis of **homotopy type theory**.

$\require{color}$

## Previously, on Science4All…

But before getting to homotopy type theory, let’s have a quick recap on the essential elements of type theory. Type theory is the theory of **types**, which are structures made of *terms*. The type $\mathbb N$ of natural numbers is an example of such types, whose terms are natural numbers like $0$, $1$ and $1729$. We write $1729:\mathbb N$, to signify that $1729$ is a *term* (or *inhabitant*) of the type $\mathbb N$.

There’s one big difference though. Types must be defined along with **constructors**. Every term of a type can only be defined by use of a constructor of the type. These constructors may also be regarded as the incoming functions of a type. This means that any function that outputs an element of a type must involve a constructor of that type. This perspective on types yields a formidably computable approach to mathematics.

Yes. Well, we must also have a way to use the constructed terms of a type to define outgoing functions. This other side of the coin is known as the **induction principle**. Schematically, we have the following figure:

I’ve found it useful to regard terms of types as the full sequence of constructions that led to them. Then, we have a direct way to assert equality: Two terms $x$ and $y$ are **definitionally equal** (or judgmentally) if they are the same sequence of constructions. We denote $x \equiv y$. Clearly, by definition, $x \equiv x$.

They’d be *definitionally unequal* indeed. But, as Poincaré asserted it, “mathematics is the art of giving the same name to different things”. So, in many cases, we might want to prove the **propositional equality** of two definitionally unequal terms. More precisely, type theory defines the propositional equality of two terms $x$ and $y$ as a type $(x=y)$ whose terms are *proofs* of the equality. In other words, proving the *propositional identity* $x=y$ boils down to constructing an *inhabitant* $p$ of the type $(x=y)$, which we denote $p: (x=y)$, or, more simply, $p:x=y$.

First, we have a reflexivity proof $\mathsf{refl}_x : x = x$ derived from any definitional equality $x \equiv x$. Plus, we can use proofs to derive other proofs. In particular, using the induction principle of identity paths, we have the important **action-on-path** lemma: For any function $f$, and any two terms $x$ and $y$, we can construct a function $\mathsf{ap}_f : (x=y) \rightarrow (f(x) = f(y))$. This function $\mathsf{ap}_f$ constructs a proof of $\mathsf{ap}_f(p) : f(x) = f(y)$ from any proof $p:x=y$. Written informally, this says that the propositional identity $x=y$ *implies* the propositional identity $f(x)=f(y)$. More generally, an implication is now just a function!

## Integer Numbers

Now, a big portion of homotopy type theory builds upon the univalence axiom which I’ll only get to in the third part of this series. But there’s already a beautiful universe to explore without that univalence axiom. And it’s all based on **higher inductive types**.

In classical type theory, constructors could only construct *terms* of types. But, in an impulse of freeing us from that rigid law, homotopy type theorists have proposed to allow for the constructions of *propositional identities* as well. And this turned out to be extremely empowering!

Let me show you that with an example of construction of the type of integer numbers. A famous approach consists in defining $\mathbb Z$ as a quotient set of $\mathbb N \times \mathbb N$. I discussed it in my article on the set-theoretical construction of numbers, and its type-theoretical counterpart is quite interesting, as it already involves higher inductive types. Informally, this construction identifies pairs $(a,b)$ with the integer number “$a-b$”. Here’s an illustration of that construction.

Yet, I don’t know about you, but that does not look like a very natural construction to me. I mean, when you actually use integers, do you really picture them as equivalence classes of the Cartesian square of natural numbers? Surely, that *works*, but that’s not how *informal mathematics* works. Fortunately, one of the designated goals of homotopy type theory is to allow for more natural definitions of objects, hence making *formal mathematics* more like *informal mathematics*!

**not**from the homotopy type theory book, which defines integers accordingly to the figure above. In fact, here, we’ll get a type which is not “the same” as the integer type $\mathbb Z$ of the book, as our type will not be a “set”. But I find our type so much more insightful to understand both integers and higher inductive types.

I don’t know about you, but, back when I was in elementary school, I found the image of the (European) elevator very useful. In this metaphor, numbers are floors of an (infinite) elevator. And, because the elevator can move down, below the ground floor, we can get to negative numbers. More precisely, elevators have a *one-floor-down move* and a *one-floor-up move*. Interestingly, using these moves, we can get to any integer floor by starting at ground floor… Do you see the analogy with a type of integers?

Exactly! More precisely, the *elevator-floor* type $\mathsf{Floor}$ will have three constructors:

- The zero constructor $0:\mathsf{Floor}$.
- The up constructor $\color{OliveGreen} \uparrow: \mathsf{Floor} \rightarrow \mathsf{Floor}$, which gets us one floor up.
- The down constructor $\color{NavyBlue} \downarrow: \mathsf{Floor} \rightarrow \mathsf{Floor}$, which gets us one floor down.

So, intuitively, we’d have ${\color{OliveGreen} \uparrow}(0)$ being the “1” floor, while ${\color{NavyBlue} \downarrow} (0)$ would be the “-1” floor. But if our definition of constructors of $\mathsf{Floor}$ stopped here, there’d be one big trouble. If we go up then down, we wouldn’t end up at 0. In formal words, the term ${\color{NavyBlue} \downarrow}( {\color{OliveGreen} \uparrow} (0))$ here wouldn’t equal $0$.

Exactly! More precisely, let’s add the two identity constructors:

- For all $n : \mathsf{Floor}$, we have an identity constructor $\mathsf{id_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}}(n) : n = {\color{OliveGreen} \uparrow}({\color{NavyBlue} \downarrow}(n))$, which proves that going down then up is equivalent to staying still.
- For all $n : \mathsf{Floor}$, we have an identity constructor $\mathsf{id_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}}(n) : n = {\color{NavyBlue} \downarrow}({\color{OliveGreen} \uparrow}(n))$, which proves that going up then down is equivalent to staying still..

To complete the definition of our type $\mathsf{Floor}$, we now need an induction principle to construct functions $f:\mathsf{Floor} \rightarrow A$ going out of $\mathsf{Floor}$. Like for $\mathbb N$, we first need the image $f(0):A$ of $0:\mathsf{Floor}$. Then, we need to know how to construct $f({\color{OliveGreen} \uparrow}(n)) : A$ from $f(n) : A$, which is done by a function $g_{\color{OliveGreen} \uparrow} : A \rightarrow A$. Similarly, to construct $f({\color{NavyBlue} \downarrow}(n))$ from $f(n)$, we need a function $g_{\color{NavyBlue} \downarrow} : A \rightarrow A$.

Excellent remark! We need to make sure that equal floors have equal images. This corresponds to determining proofs $\mathsf{id}^g_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}(x) : x = g_{\color{OliveGreen} \uparrow}(g_{\color{NavyBlue} \downarrow}(x))$ and $\mathsf{id}^g_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}(x) : x = g_{\color{NavyBlue} \downarrow} (g_{\color{OliveGreen} \uparrow} (x))$.

Yes! Given $f(0)$, $g_{\color{OliveGreen} \uparrow}$, $g_{\color{NavyBlue} \downarrow}$, $\mathsf{id}^g_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}$ and $\mathsf{id}^g_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}$, we now have a function $f: \mathsf{Floor} \rightarrow A$.

## Identity Proofs are Paths!

Now, intuitively, the rules we have introduced for our type $\mathsf{Floor}$ yield several *different* constructions of floor “$1$” in $\mathsf{Floor}$. This intuition is true. For instance, ${\color{OliveGreen} \uparrow}({\color{NavyBlue} \downarrow}({\color{NavyBlue} \downarrow}({\color{OliveGreen} \uparrow}({\color{OliveGreen} \uparrow}(0)))))$ equals ${\color{OliveGreen} \uparrow}(0)$. Let’s prove it! To simplify notations, from now on, I’ll drop parentheses when composing constructors ${\color{OliveGreen} \uparrow}$ and ${\color{NavyBlue} \downarrow}$, and the 0 which is always the first input term of any sequence of constructors. So, with these notations, what we want to prove, is ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$.

That’s the idea! Let’s start by “removing” the first ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}$ of the term ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} $. I mean, let’s verify that ${\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} ({\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} )$. Well, that’s given by the proof constructor $\mathsf{id_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}} ({\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow})$! Next, we need remove the first ${\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$ of the expression ${\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$. And that’s given by the proof $\mathsf{id_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}}({\color{OliveGreen} \uparrow}) : {\color{OliveGreen} \uparrow} = {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$. So, to recapitulate, we have proofs that ${\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$ and ${\color{OliveGreen} \uparrow} = {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$. But can we use these to construct a proof of ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$?

Here we get to the beautiful central idea of homotopy type theory! Proofs $q : x = y$ may be interpreted as **paths** from $x$ to $y$. Given this, *terms of types* can now also called *points in spaces*. And, using the path induction principle, it can be proved that paths can be composed. Like in homotopy theory! This means that if $q: x = y$ and $r:y=z$, then we can construct a composed path $q \cdot r : x=z$. Similarly, if $q:x=y$, we can invert $q$, hence constructing $q^{-1} : y=x$.

Let’s apply that to prove ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$. Recall that $\mathsf{id_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}}({\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}) : {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$. We can invert this path, yielding $\mathsf{id_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}}({\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow})^{-1} : {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow}$. Similarly, $\mathsf{id_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}}( {\color{OliveGreen} \uparrow})^{-1} : {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$. Finally, using path composition, we have the proof $\mathsf{id_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}}}({\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow})^{-1} \cdot \mathsf{id_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} }}( {\color{OliveGreen} \uparrow})^{-1} : {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$. We’ve done it!

Now, what’s amazing as we view proofs as paths is that we can see the “*different*” terms of the type $\mathsf{Floor}$ as the different connected components. Let’s draw it:

And that’s where things become very interesting from a homotopical viewpoint!

## Homotopy Groups

The pinnacle of homotopy theory is Perelman’s recent proof of the Poincaré conjecture, which states that, for $n \geq 2$, all $n$-spheres are topologically characterized by the triviality of their homotopy group.

You may read my article on homotopy to learn more, but, for our purpose, what it means is that homotopy is a cornerstone of modern mathematics. In particular, **homotopy groups**, also known as *fundamental group*, are, well, fundamental.

Roughly, a homotopy group is a set of *different* loops. Interpreted in terms of homotopy type theory, this homotopy group is the set of *different* proofs of an identity between two identical constructions.

Sure! Our definition of the type $\mathsf{Floor}$ will provide a great one. Let’s give two different proofs that ${\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$. As you’ll see, this will lead us to two different paths ${\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$.

Yes. This corresponds to the proof $\mathsf{id}_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}} ({\color{OliveGreen} \uparrow}) : {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$. But we can work out the equality in a different way. Do you see it?

Exactly. To do so, let’s forget about the first arrow for a second, and prove ${\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow} = 0$. That’s given by $\mathsf{id}_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}(0) : 0 = {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$. We can now derive the former identity by applying the up constructor to both sides. By the action-on-path lemma, we then have a proof $\mathsf{ap}_{\color{OliveGreen} \uparrow} (\mathsf{id}_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}(0) ) : {\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$. And, while it’s actually not formally straightforward, intuitively, the proof $\mathsf{ap}_{\color{OliveGreen} \uparrow} (\mathsf{id}_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}(0) )$ is *different* from $\mathsf{id}_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}} ({\color{OliveGreen} \uparrow})$, as it comes from a completely different proof construction.

Our two different proofs can now be regarded to different paths ${\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$. This means that we can go from ${\color{OliveGreen} \uparrow}$ to ${\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}$ with one path, and come back to ${\color{OliveGreen} \uparrow}$ with the other path. Formally, this loop is the path composition $\mathsf{id}_{{\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow}} ({\color{OliveGreen} \uparrow}) \cdot \mathsf{ap}^{-1}_{\color{OliveGreen} \uparrow} (\mathsf{id}_{{\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow}}(0) )$, and it represents a non-trivial proof of ${\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$.

Just like in homotopy theory, the homotopy group $\pi_1(\mathsf{Floor}, {\color{OliveGreen} \uparrow})$ centered on ${\color{OliveGreen} \uparrow}$ is the set of *different* paths (or proofs) ${\color{OliveGreen} \uparrow} = {\color{OliveGreen} \uparrow}$. But, crucially, it does not really depend on the point it is centered on, but rather on the connected component which contains that point. This is because $\pi_1(\mathsf{Floor}, {\color{OliveGreen} \uparrow})$ is **isomorphic** to $\pi_1(\mathsf{Floor}, {\color{OliveGreen} \uparrow} {\color{NavyBlue} \downarrow} {\color{OliveGreen} \uparrow})$, in the sense that there is a natural one-to-one map between these two homotopy groups.

Now, the homotopy group $\pi_1(\mathsf{Floor}, {\color{OliveGreen} \uparrow})$ here is actually quite complicated, and I’m not going to venture describing it here. Instead, let’s focus on basic homotopical spaces!

## Circles and Spheres

What would be the simplest higher inductive type with a non trivial homotopy? Well, let’s just have a single constructor of a single term, and a single constructor of a single non-trivial path. We’ll call that type $\mathbb S^1$. Here are its constructors:

- The constructor of the base term defined by $\mathsf{base} : \mathbb S^1$.
- The constructor of a (non-trivial) loop defined by $\mathsf{loop} : \mathsf{base} = \mathsf{base}$.

Let’s draw the homotopy of $\mathbb S^1$.

Note that in this homotopical perspective, the trivial proof $\mathsf{refl_{base}}$ stands for staying still at $\mathsf{base}$. Now, In the figure above, it’s useful to imagine that there’s a whole inside the $\mathsf{loop}$, so that the $\mathsf{loop}$ cannot be continuously deformed into the $\mathsf{refl_{base}}$. Doesn’t this structure remind you of something?

Exactly! As weird as it sounds, the constructors we have given above define the (homotopical) circle $\mathbb S^1$. I bet you’ve never thought of circles that way!

I know! It’s also a much *cleaner* definition of the circle than any other I’ve ever read before. This is especially true when you ponder the fact that there is not always an equivalent of the *usual* real numbers in constructive mathematics! Similarly, the mere definition of topology in constructive mathematics is very tricky. Given that, it’s not obvious how homotopy theory could be developed constructively, and how proofs in homotopy theory could be computationally checked. Amazingly, higher inductive types and homotopy type theory give us a clean, simple and elegant model for homotopy theory!

Intuitively, any path in a circle consists in looping with regards to the $\mathsf{base}$ clockwisely or anti-clockwisely. Plus, we can remark that looping once clockwisely and then once anti-clockwisely is equivalent to staying at the $\mathsf{base}$ all along. In other words, $\mathsf{loop} \cdot \mathsf{loop}^{-1} = \mathsf{refl}_0$. So, intuitively, any path has the form $\mathsf{loop}^n$ with $n \in \mathbb Z$.

It seems obvious. Yet, weirdly enough, we cannot prove it without additional axiom! So, the proof of $\pi_1(\mathbb S^1) = \mathbb Z$ will have to wait for the third part of this series, where we’ll present the univalence axiom!

To conclude this section, let me blow your mind with the most amazing definition I have found in this book.

It’s the definition of the sphere $\mathbb S^2$. What’s a sphere? Well, in homotopy type theory, it’s the type defined by the two following constructors:

- A base point constructor $\mathsf{base} : \mathbb S^2$.
- A (non-trivial)
*2-dimensional path*constructor $\mathsf{surface} : \mathsf{refl_{base}} = \mathsf{refl_{base}}$.

In other words, the sphere is defined as a point with a non-trivial loop of loop from staying at $\mathsf{base}$ to staying at $\mathsf{base}$.

It should! But reflecting on this spectacularly clean but awfully complex structure is the gateway to grasping the key ideas of homotopy type theory. That’s why I’m ending this article here!

## Conclusion

The introduction of higher inductive types starts with a simple idea: Let’s allow the construction of identity proofs! As mathematics has developed into a constructive art, and while mathematicians are asking for more rights to create, such a liberating authorization may turn out to be a cornerstone for an upcoming blow-up of new mathematical ideas. In this article, it’s enabled me to write down a very intuitive construction of integers, which much better fits the intuition we (or at least I) first had about them! But, more importantly, for the top mathematicians at the forefront of the (computable) mathematical frontier, higher inductive type has been an amazing basis to cleanly and elegantly approach homotopy theory from a much more direct way.

However, in this article, there is one missing weapon that our revolution will need to be successful (as far as we know). This weapon is the elegant **univalence axiom**, introduced by Fields medalist Vladimir Voevodsky. In the third and last episode of this series, we’ll see how successful Voevodsky’s weapon may be (or already is!) at reshaping the landscape of mathematics.