Practical example in using (homotopy) type theory

Question

I have just read Grayson's introduction on homotopy type theory as a possible foundation for mathematics. It is very enlightening about what all the fuss is about, but I am left with some doubts. Forgive my naiveté, I am not expert in type theory at all.

When one uses ZFC as a foundation for mathematics, one evenutally moves to doing informal reasoning, knowing that it is always possible, although slightly tedious, to formalize all arguments. I am not sure about how to perform this step in HTT.

Let me take the example of Grayson, who shows how to define a group in HTT. First, he defines

• a type $P$ is a proposition iff it has at most one element (that is, the type $\prod_{p : P} \prod_{q : P} p = q$ is inhabited) - which, if existent, is called a proof of $P$
• a type $S$ ia a set iff for all $s: S$ and $t: S$ the type $s = t$ is a proposition

Then a group is a tuple $(G, e, i, m, \alpha, \lambda, \rho, \lambda', \rho', \iota)$ where

• $G$ is a type
• $e: G$, $i: G \to G$, $m: G \times G \to G$
• $\alpha$ is a proof of the identity stating associativity, and so on for $\lambda, \rho, \lambda', \rho'$ which prove left and right identity of $e$ and existence of left and right inverses
• $\iota$ is a proof that $G$ is a set (according to Grayson, it is a theorem that this fact is itself a proposition)

So far, so good: I am inclined to believe that with a little ingenuity one can in fact define most (all?) usual concepts in mathematics.

Now, I would like to go on proving theorems about groups. The simplest non-trivial theorem I can think of is Lagrange theorem: if $G$ is a finite group and $H < G$ a subgroup, then $|H|$ divides $|G|$. The intuitive proof is very short: for every coset $C$ of $H$ and any $c \in C$, multiplication by $c$ is a bijection $H \to C$, and $G$ is partitioned into cosets.

It is clear to me how to formalize this in ZFC, but I would be lost trying to do that in HTT. I have two kind of doubts:

1) Do all steps work as well? It seems to me that one uses the notion of subset. Is there such a notion in HTT? I guess there are no subtypes, so it would seem no subsets as well. I guess that one can define a subgroup as a triple $(H, f, p)$ where $H$ is a group, $f \colon H \to G$ and $p$ is a proof that $f$ is injective. But eventually we are doing something like "counting elements" - is this justified?

2) Even logic has changed into this new setting: proof are themselves objects of this mathematical universe. I guess I need to have something like a constructive proof to make this work out? Does it matter that I have to choose arbitrary elements $c \in C$ to find a bijection?

Sorry for the vague question: I am trying to understand what it would be like to do mathematics knowning in the back of your head that one can formalize thing into HTT, and it is not obvious to a beginner like me

Answer 1

I know a bit about HoTT and have worked quite extensively with proof assistants, but I am certainly not a HoTT expert. Nonetheless, I think that the story is as follows. We can construct a type $L$ of bijections from $G$ to $\{1,\dotsc,n\}$ (where the inverse is explicitly given as part of the data of the bijection). Given such a bijection, we can use it to select a preferred representative of each coset (the one with the lowest index), and proceed in an obvious way to prove Lagrange's theorem. In other words, we can construct a term of type $L\to P$, where $P$ is the proposition that Lagrange's Theorem holds for $G$. We are assuming that $G$ is finite, which might mean that we are given a term of type $L$, in which case we are done. However, it might instead mean merely that we are given a term of type $\text{nonempty } L$, which is the propositional truncation of $L$. However, that is still enough: it is built into the foundational framework that any map from $L$ to a proposition factors through $\text{nonempty }L$.

Answer 2

The answers and comments on this question show that there is still a ton of misinformation out there about HoTT.

The short answer (but much more time-consuming for you) is that you should read the HoTT Book, which was explicitly written to address this sort of question. To address the specific questions you asked, and the points raised in the other answers:

• HoTT is not a structural set theory. Nor is it a material set theory; it is a type theory, a different kind of beast altogether. For an explanation of the differences, see this blog post of mine.

• There absolutely is a notion of subset type (or subtype). The rules for subset types are explained in that blog post. Subsets of a type $A$ are usually encoded as their characteristic functions $P:A \to \rm Prop$. Given such a subset, one can always take its $\Sigma$-type $\sum_{x:A} P(x)$ which is a type with an injective function to $A$, but often it's easier and better to work directly with subsets than with such things. Of course, when you want a subset of a group to be itself a group, you'll need to consider it as a type in its own right, and you might find it easier to formulate Lagrange's theorem in terms of an arbitrary injective group homomorphism.

• Constructive logic is a red herring if what you're wondering about is what mathematics looks like in HoTT versus in ZFC. It's true that HoTT is "by default" constructive due to its inheritance from type theory, but one can simply add the axioms of excluded middle and choice to obtain a mathematics that looks just like classical mathematics in most respects. (If you do want to be constructive, then as others have pointed out you have to be careful about the meaning of "finite" -- but this would also be true if you were trying to use a constructive set theory like IZF, and is irrelevant to doing mathematics in HoTT+LEM+AC.)

Answer 3

I think your question isn’t really about type theory or homotopy type theory, but instead about constructive mathematics. You’d have similar issues in dealing with picking representatives for an equivalence relation if you were working in a constructive version of ZF. There’s a bit of an art to working constructively. In this case, I suspect that what you need to think about is making sure you’re using the right notion of finite set. (Some notions of finite that agree nonconstructively might not agree constructively.)

Answer 4

HoTT differs from ZFC in several aspects and it is useful to separate them:

1. ZFC is a material set theory while HoTT is a structural one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.

2. HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.

3. The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).