# Practical example in using (homotopy) type theory

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

• As discussed below this isn't really about group theory, it's about finite sets. There's a paper on finite sets in HoTT that you might like. cs.ru.nl/~nweide/FiniteSetsInHoTT.pdf – Noah Snyder Jul 18 '19 at 18:57
• Alternatively, if you don't care about working constructively, you can see Lagrange's theorem fully proved in code in a type theory with LEM in the Lean Mathlib where I think it's the lemma "card_subgroup_dvd_card". – Noah Snyder Jul 18 '19 at 19:57

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

• With this notion of finite, you also need that the range of $H$ is a decidable subgroup, otherwise finding "the one with lowest index" doesn't work. Equivalently, you can assume that $H$ is finite in the same sense ($H$'s appropriate $L$ is nonempty). – François G. Dorais Jul 18 '19 at 17:10
• Many good answers here, but I have chosen this one, as it actually address how one would go on about proving the theorem I presented as an example, even though for a particular choice of definition of finite sets – Andrea Ferretti Jul 19 '19 at 13:51

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

• What do you mean exactly when you say "a structural set theory"? I think type theory is much closer to structural set theories than to material ones, actually so close that I can call it a structural set theory, but it seems you disagree with this point of view. Is the internal language of a topos a type theory or a structural set theory? I think it might be just a matter of terminology, so could you explain what's the difference between structural a set theory and a type theory precisely? – Valery Isaev Jul 18 '19 at 19:37
• @TimothyChow Yes, I did, but ETCS is not the only structural set theory (in the same way that ZFC is not the only material one). This is why I want to know what is the definition of "a structural set theory". The ncatlab page is somewhat vague about this and it even mentions type theory (or rather setoids in it, but assuming we have quotients this does not seem relevant) as an example of a structural set theory. – Valery Isaev Jul 18 '19 at 20:18
• @ValeryIsaev To me, a structural set theory is a theory in which the "elements" of a set are featureless points that are only given meaning by the "structure" on that set. That structure could consist of functions, as in ETCS, or relations, as in SEAR, or potentially something else I guess. By contrast, in a type theory the elements of a type do have intrinsic structure: the elements of a function type are functions, the elements of a product type are pairs, the elements of a universe are types, etc. – Mike Shulman Jul 19 '19 at 2:58
• As for "the" internal language of a topos, it's not as if the categorical structure of a topos uniquely determines one formal system that can be interpreted in a topos that we could then use the definite article for. The traditional choice of such a formal system is intuitionistic higher-order logic, which is a type theory. Versions of dependent type theory can also be used. So can structural set theories, as I sketched in arxiv.org/abs/1004.3802. For that matter, so can material set theories (e.g. doi.org/10.1016/j.apal.2013.06.004). – Mike Shulman Jul 19 '19 at 3:02
• There are also formal differences between structural set theories and type theories. Structural set theories are first-order theories, specified by a set of axioms formulated in a first-order (perhaps dependently typed) logic. A type theory is its own deductive system, existing ontologically at the same level as first-order logic, often with no need for any axioms at all. – Mike Shulman Jul 19 '19 at 3:30

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

• @AndreaFerretti Choice is not the issue, you need to correctly define "finite". There are several different ways to do this in HTT, but they all coincide assuming excluded middle and choice. Once you investigate what "finite" means, you will notice that "finite choice", "subtypes of finite types are finite", "quotients of finite types are finite" are (independently of each other) provable in HTT for some but not all variations of "finite". For Lagrange's Theorem, you need all three of these to work simultaneously, or you need to restrict what you mean by "subgroup". – François G. Dorais Jul 18 '19 at 16:35
• No, these are all definitions of finite sets. It is even less clear how to define finite types. Let me note once again, this problem is the problem of constructive mathematics. It will be the same in other constructive theories such as CZF and IZF. – Valery Isaev Jul 18 '19 at 16:43
• @AndreaFerretti No, even sets are a problem. The issue with choice is decidable equality, for example. – François G. Dorais Jul 18 '19 at 16:45
• Are these things easy in classical foundations? You still need to define what a finite set is, and you still need to prove finite choice, subsets of finite sets are finite, and quotients of finite sets are finite. Working constructively makes things harder, but if you throw in excluded-middle and choice, then it doesn't seem to me that the difficulty is much different in classical foundations or in type theoretic foundations (none of this is about homotopy types). Either way you have to think a bit about why finite sets work the way you think they do. – Noah Snyder Jul 18 '19 at 18:15
• FWIW, choice is irrelevant for most purposes when dealing with finiteness; excluded middle is enough to make most definitions of "finite" coincide and behave the way a classical mathematician expects. The only exception I'm aware of is the notion of "Dedekind-finite set" which requires a small amount of choice (even less than countable choice) to prove equivalent to all the other notions of finiteness; but that definition is I think very rarely used in practice. And, as Valery has stressed, this is an issue of constructiveness that is completely orthogonal to HoTT vs ZFC. – Mike Shulman Jul 18 '19 at 19:23

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