7
$\begingroup$

I've been reading Andrej Bauer's blog post on "Univalent foundations subsume classical mathematics," which explains how Univalent Foundations and Homotopy Type Theory (HoTT) extend classical mathematics by incorporating types stratified by homotopy-theoretic complexity. The post discusses that logic and sets are seen as lower-level types in this extended framework, but it also introduces higher types such as groupoids and beyond.

My question pertains to the necessity and utility of these higher types in HoTT:

  1. Redundancy concern: In traditional set theory, particularly within Zermelo-Fraenkel (ZF) or Zermelo-Fraenkel with the Axiom of Choice (ZFC), we are able to construct a vast array of mathematical structures. Given this capability, what additional structures or benefits do higher types in HoTT (beyond logic and sets) provide? Are they not redundant since every mathematical construction achievable in HoTT seems also constructible in ZFC?

  2. Unique constructions: Are there specific examples of mathematical structures that cannot be constructed within the ZF or ZFC framework but can be realized using the higher types in HoTT? If so, what are these structures, and how do higher types facilitate their construction?

Thank you for your insights.

$\endgroup$
4
  • 2
    $\begingroup$ As someone almost completely ignorant of type theory, my understanding is that we have an array of equiconsistency/interpretability results between set theories and type theories which imply that anything one can do, the other can do better. (mama mia!) But I would be interested to hear from someone less ignorant. $\endgroup$
    – Alec Rhea
    Commented Jul 23 at 15:10
  • $\begingroup$ On (2), it's always worth considering the constraints of the underlying logical framework; ZFC is first-order, and there are several classes of structures which aren't first-order-izable. The "necessity and utility of these higher types" is not specific to HoTT. $\endgroup$
    – Corbin
    Commented Jul 24 at 16:08
  • 1
    $\begingroup$ I find the following analogy helpful: Comparing HoTT and ZFC is akin to comparing two different programming languages. In any sufficiently powerful programming language, you can do anything that you can do in any other language. Nevertheless, different programming languages have different merits. Some goals are easier to achieve in one language than another, and some kinds of bugs are more likely to occur in one language than another. So "redundancy" and "uniqueness" are in some sense beside the point. $\endgroup$ Commented Jul 25 at 12:57
  • 1
    $\begingroup$ @AlecRhea See for example Mariano Carneiro's master's thesis (it deals with Lean and not HoTT, but I think it is still pertinent). Roughly speaking, it shows that Lean is "equivalent" to ZFC + infinitely many inaccessibles. $\endgroup$ Commented Jul 25 at 12:59

1 Answer 1

8
$\begingroup$

The blog post was written in the context of HoTT having just come out and some people were assuming it was a form of hard constructivism (see the mailing list discussions linked to in the blog post), so I tried to explain that:

  1. HoTT is agnostic with respect to excluded middle and the axiom of choice. One can assume these principles if so desired, and thereby incorporate set-level classical mathematics.

  2. In HoTT the usual conception of set appears naturally as one level of a richer hierarchy of types. In this sense HoTT is a generalization of set theory. Moreover, the hierarchy is quite relevant to mathematical practice and has significant explanatory power.

Regarding the second point, note that it is not at all unusual to have sets appear in a larger universe. For example, every Grothendieck topos contains sets as a full subcategory, as well as any realizability topos.

The two foundations, ZFC and HoTT, paint different pictures of how mathematics can be organized, they serve different purposes, and they are used diffrently (see Penelope Maddy's What Do We Want a Foundation to Do?).

To demonstrate the difference, let us consider the circle. There are several mathematical manifestations of the idea:

  1. The circle as a raw set $C$ of all points in a plane at unit distance from the origin.

  2. The circle as a topological space $(C, \tau)$, with the standard topology $\tau$.

  3. The circle $(\{z \in \mathbb{C} \mid |z| = 1\}, 1, {}^{-1}, {\times})$ as the multiplicative subgroup of non-zero complex numbers.

The above manifestations are constructed in ZFC from sets as structure, as indicated above.

In HoTT we can also define all the manifestations in the exact way, as structures. But in addition, there is a fourth manifestation of the circle: the homotopical circle $S^1$ that is built as a higher-inductive type. This type is not the result of any set-theoretic construction carried out in HoTT.

One can of course build a model of HoTT in ZFC and observe that the homotopical circle $S^1$ is an object in this model, namely a certain Kan simplicial set, therefore it is the result of a set-theoretic construction carried out in ZFC.

I would hope that the above remarks are completely obvious. And let me be explicit: I do not think that one foundation is "better" than the other.

Now, let me finally address OP's questions.

The way I understand the first questions is this: what are the higher types appearing in HoTT good for if they already can be constructed from sets? I hope the above discussion clears this up. So long as we work inside HoTT, there are going to be types that are not sets, not can they be constructed from sets. The homotopical circle is an example.

The second question asks about structures that exist in HoTT but not in ZFC. Again, we can use the homotopical circle $S^1$ as an example. This is a pointed type, with a base point $b : S^1$, such that the monoid of all maps $S^1 \to S^1$ that fix $b$ is isomorphic to the additive group $\mathbb{Z}$ (in HoTT paralance we would say that the loop space of $S^1$ is equivalent to $\mathbb{Z}$). No set has this property, for cardinality reasons.

And let me reiterate: of course one can build groupoids in ZFC and observe that there is a pointed groupoid whose loop space is equivalent to $\mathbb{Z}$. However, this does not falsify the claim that in HoTT $S^1$ exhibits a phenomenon that no set can.

$\endgroup$
25
  • 4
    $\begingroup$ @Andrej: Isn't this just cherrypicking an interpretation to make the argument? This is like saying that since I can encode strings as vectors in Javascript, they are inherently distinct from integers. Even though that residing in your memory, even a vector is just a big number... $\endgroup$
    – Asaf Karagila
    Commented Jul 24 at 7:08
  • 4
    $\begingroup$ @AsafKaragila: what I am trying to get across (but not very well) is that building a model $M_X$ of foundation $X$ in foundation $Y$ doesn't really count as "doing $X$-things in $Y$". It's "doing $X$-things in $M_X$". Abstraction matters, also in your javascript example: vectors may appear as big numbers outside Javascript, but so long as we work in Javascript, we don't have direct access to those numbers. (And also, they're really voltages in a digital circuit.) $\endgroup$ Commented Jul 24 at 7:16
  • 4
    $\begingroup$ @NaïmFavier: I'm glad for you. I'm proving theorems by writing proofs. I enjoy programming, and I enjoy doing maths the way I do it. I'd say it's a hobby, but I do have a permanent job as a mathematician and programming is just a side hobby. If you don't mind, I'll keep doing it this way. $\endgroup$
    – Asaf Karagila
    Commented Jul 24 at 11:52
  • 4
    $\begingroup$ Why do people feel like they need to defend set theory? $\endgroup$ Commented Jul 24 at 14:48
  • 6
    $\begingroup$ Andrej, I don't know about other people. But when you go like "Ugh, I'm gonna get comments about this being a thing, because I choose to present my argument in a specific way" it elicit responses, exactly of the kind you're anticipating. Nobody feels the need to defend ZFC. I think I'm just a bit confused with the exasperated tone, and I imagine other people are too. $\endgroup$
    – Asaf Karagila
    Commented Jul 24 at 22:01

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .