Before discussing any, let’s quickly recap what ZF (Zermelo-Fraenkel axioms of set theory) and HoTT (Homotopy type theory) are meant to be, shall we?

Part 0: Foundations

So, every mathematical object has it’s own rules; you can talk about groups, probability distributions, matrices, metric spaces and other stuff. It would be nice if all of these things could be described by the same elemental object. A thing to represent everything else.

In this sense, ZF and HoTT are “foundational theories” in the sense that, every structure can be described as an elemental object from the theory.

ZF’s elemental object are the sets. They are meant to capture the idea of a “Collection of things with properties in common”, like the collection of all natural numbers, the collection of all symetries of a triangle, the collection off all the weighted coins, and things like that. Of course, as a couple of you may or may not know, letting everything be a set has a couple of undesirable consequences:

So not every “Collection of any things” can be described as a set. The job of the ZF axioms is to explain which collections are sets and which new sets can be made from previous sets.

HoTT on the other hand is something different. For starters, it’s elemental object are the types. Which encode the idea of “An object with a defined behaviour”. A number behaves in a fundamentally different way than a function, or a group, or a mere set, or a proposition, or a word. You get the idea. While ZF avoids Russell’s paradox by restricting what a set can be, HoTT avoids Russell’s paradox by adding a hierarchy.

You see, the analogous to the “collection of all sets” in type theory isn’t a “member of itself”. The way other theories beyond ZF manage to do this is to declare that the collection of all sets is something higher than a set, is a class. And the collection of all classes would be something even higher than that. This is what I mean by a hierarchy. This would avoid the paradox in a slighltly more convoluted way but it has some advantages like being able to have arbitrarialy large families of sets, classes or things like that.

So the former uses sets (collections of things with shared properties) and the latter uses types (objects with a defined behaviour). What’s the difference?

Part 1: The structure of objects

Let’s consider a group:

Given a set G and an operation [math]\cdot_G : G \times G \to G[/math]. We say that [math](G, \cdot_G)[/math] is a group if the following criteria is met:

• There is a neutral element on [math]G[/math]. That is, some [math]e \in G[/math] such that [math]e \cdot_G x = x = x \cdot_G e[/math], where [math]x[/math] can be any element on [math]G[/math]
• The operation is associative, meaning that we don’t have to bother with parenthesis ([math]a \cdot_G b \cdot_G c[/math] isn’t ambiguous because [math](a \cdot_G b) \cdot_G c = a \cdot_G (b \cdot_G c)[/math]).
• Every object can be inverted. That is, for any [math]x \in G[/math] there is some [math]\bar{x} \in G[/math] such that [math]x \cdot_G \bar{x} = e = \bar{x} \cdot_G x[/math].

An example of a group is the integers with adition. Is easy to verify that all of the criteria are met. Another example are the positive racional numbers with multiplication. Another less “mathy” example are the symmetries of a square (all the things that you can do to a square that leave it looking the same) with the operation of “just make one after the other”.

Notice that a group is just a set (a collection of things) with some added structure (the operation in question. Most mathy things will have the same… feature. A metric space is a collection of things (points) with a distance function. A probability space is a collection of things (the things that could happen) together with a probability distribution (a way to determine the “likelyhood” of the things that could happen). And so on.

HoTT on the other hand, cannot define an object without some behaviour. To make an example, here is how the natural numbers are defined:

Introduction:

• [math]0 : \N[/math] read as “0 is of type [math]\N[/math]" or “0 has type [math]\N[/math]"
• [math]succ : \N \to \N[/math], understood as [math]succ[/math] being a function from the natural numbers to the natural numbers. The usual succesor function.

Elimination:

Let [math]P : \N \to U[/math] a family of types indexed by [math]\N[/math]. To show that each [math]P(x)[/math] is inhabited (there is a point [math]a : P(x)[/math] it’s sufficient to show that:

• [math]P(0)[/math] is inhabited (there is some [math]a : P(0)[/math])
• Given [math]n : \N[/math], [math]x : P(n)[/math], show a general procedure to construct some inhabitant of [math]P(succ (n))[/math] (Some [math]g[/math] that taking [math]n[/math] and [math]x[/math] produces the inhabitant [math]g(n, x) : P(succ(n))[/math]).

With those two ingredients, there is a function [math]f_{(c, g)}[/math] that takes any [math]x : \N[/math] and produces some [math]f_{(c, g)}(x) : P(x)[/math].

Computation:

The function [math]f_{(c, g)}[/math] behaves as espected:

• [math]f_{(c, g)}(0) = c : P(0)[/math]
• [math]f_{(c, g)}(succ(n)) = g(n, f_{(c, g)}(n))[/math]

Reading in between all the jargon, you might notice that the “elimination-computation” parts are just the induction principle for the natural numbers. More over, the computation part looks very similar to the recursive definitions for functions. This is because on HoTT, propositions are also representable by types, so the recursive theorem and the induction principle are two faces of the same coin (the former is a special case of the latter).

If you think about it, everything from [math]\N[/math] can be constructed using it’s recursion and induction. So this type fully captures what [math]\N[/math] is meant to represent. We can also have a universe of groups by considering all the types on a universe (one of the levels from the hierarchy discussed before) which some operation that satisfies all of the criteria required. “An object with a defined behaviour” can encapsulate all sorts of structure, call it distance function, call it order relationship, call it whatever. HoTT allows you to construct a single type which encodes all of this information.

But other than that small detail, there doesn’t seem to be an improvement, does it?

Part 2: Types aren’t sets

A set is just a collection of points (things). There is no aditional information on the collection itself. That’s why it is neccesary to add some aditional structure. The sets have this feature called extensionality where two sets are the same when they have the exact same objects. This is good because it means that the collection of all the natural numbers that can be expressed as a product of two naturals bigger than 1 and the collection of all the natural numbers which aren’t prime nor 1 are the same collections. Regardless of the properties defining them being different.

But it also means that a set “forgets” where it came from. Given an arbitrary collection of things, it can be very hard to find the property (or one of the properties) that they had in common.

I casually threw the following sentence before:

Propositions are also representable by types

This is a huge game changer, because that means that types are intentional, they can “remember” which properties defined them. A member from “the type of all natural numbers which can be expressed as a product of two naturals bigger than 1” is not just a number (like [math]6[/math]) but also a proof of that number being expressable as a product of two naturals bigger than 1 (meaning, a proof of [math]6 = 3 \times 2[/math] and two proofs of [math]3 > 1[/math] and [math]2 > 1[/math]), while a member from “the type of all natural numbers which aren’t prime nor 1” is a number (like [math]6[/math]) together with a proof that it isn’t a prime nor is it [math]1[/math] (meaning, a proof that [math]6[/math] isn’t a prime number, and a proof that [math]6 \ne 1[/math]).

You may think that this means that the former and the latter aren’t equal since their points have very different structures. But the way equality is even treated in types is more… complicated, than it is for sets.

Part 3: Defined or proved?

Taking [math]P: \N \to U[/math] to be constant at [math]\N[/math] ([math]P(x)[/math] is [math]\N[/math] for all [math]x : \N[/math]) we can define a function from [math]\N[/math] to [math]\N[/math] by:

• [math]f(0) = 1[/math]
• [math]f(succ (n)) = (succ (n)) \times f(n)[/math]

it doesn’t make any sense at all if someone asked us to “proof that [math]f(0)[/math] is equal to [math]1[/math]". At that question we would answer simply “that’s true by definition”. It may be less obvious if someone asked us to proof that “[math]f(4) = 24[/math]". Simply stating “by definition” and calling it done doesn’t seem as convincing as the previous time, and indeed it isn’t, since in this case the proof requires multiple steps, not just one:

• [math]f(4) = 4 \times f(3) = 4 \times 3 \times f(2) = \cdots = 4 \times 3 \times 2 \times 1 \times f(0) = 4 \times 3 \times 2 \times 1 \times 1 = 24[/math]

We usually don’t notice it, but equality is a proposition. That is, “[math]a = b[/math]" is just a statement that may or may not hold between two pre-existing objects [math]a[/math] and [math]b[/math]. Or at least, that’s what ZF agrees on. But there is obviously something fundamentally different between defining something and proving, when we state that [math]f(0) = 1[/math] we’re not trying to say “we have a proof that this rare function [math]f[/math] evaluated at [math]0[/math] returns the value [math]1[/math]". Instead, we mean something more along the lines of “we declare that this function at [math]0[/math] takes the value [math]1[/math]”; we declare that [math]f(0)[/math] and [math]1[/math] are exactly the same thing.

It is different to say that something is defined to be something else, at proving that something is something else. For example, we can define [math]\sqrt{2}[/math] to be some positive real number which the property that [math]\sqrt{2} \times \sqrt{2} = \sqrt{2}^2 = 2[/math]. But that definition doesn’t acert that such real number actually exists. We can proof that the number actually exists by constructing the following real number

[math]sup \{x : \R, x^2 < 2\}[/math]

and showing that this real number has indeed the desired property.

There is a fundamental distinction between declaring that something is literally the same thing as something else, and proving that something is indeed like something else. HoTT makes this distinction even more explicit, writting “[math]a \equiv b[/math]" to mean “[math]a[/math] is literally the same thing as [math]b[/math]" and “[math]a = b[/math]" to mean “the proposition that [math]a[/math] is indeed like [math]b[/math]".

With this distinction in mind we can finally understand the types from the previous section. They are not literally the same thing, but you can proof that they are alike.

Final: base = base, and beyond.

by the way that I’ve presented it, it looks like HoTT deals with a lot more of complications than ZF to acomplish the same things. But trust me when I say that there are types that quite literally don’t have an analogous as a set.

Take the following type:

Introduction:

[math]base : S^1[/math]

[math]loop : base =_{S^1} base[/math]

This may look like something absurd, since its a type with a single point (base) and a proof of that point being indeed like itself (loop). But due to the nature of equality ([math]a = b[/math] and [math]b = c[/math] implies [math]a = c[/math], [math]a = b[/math] implies [math]b = a[/math]) this single “non-trivial proof” that base is indeed like base gives rice to a much richer structure.

Taking [math]a[/math], [math]b[/math], [math]c[/math] to be [math]base[/math], we have that [math]loop[/math] is a proof that [math]base = base[/math] and [math]loop[/math] is a proof that [math]base = base[/math]. Then we can construct a new proof [math]loop^2[/math] that ensures the obviousness of [math]base = base[/math]. Likewise, since [math]base = base[/math] ([math]a = b[/math]) we should be able to “reverse” this proof to obtain a new proof [math]loop^{-1}[/math] of the fact that [math]base = base[/math] ([math]b = a[/math]). And applying transitivity with these two proofs should give rice to the trivial proof that [math]base = base[/math].

Indeed, this trivial proof is called reflexivity on [math]a[/math] or [math]refl_a[/math] for short. Is the trivial proof that any object is indeed like itself. And while [math]loop \circ loop^{-1}[/math] may not be exactly the same thing as [math]refl_{base}[/math], they are indeed like eachother.

It turns out that this misterious type is actually a circle. Thinking on base as some arbitrary point, and loop as an actual loop starting and ending at base. You may see why this type reflects (in some way) the structure of a circle. To fully capture the analogous of this using sets it is not enough to have the collection of all points of a circle (since that doesn’t capture where [math]loop^2[/math] or [math]loop^{-1}[/math] come from) but to have some aditional structure. This gives rise to homotopy theory which, broadly speaking, is the study of paths between points, and paths between paths or “homotopies”.

I don’t know how to end this text…