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
Best Answer
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$.