Introduction to Homotopy Type Theory
arxiv.org
arxiv.org
I do not understand why homotopy type theory posts are so popular on this website. My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play. Further, the "practical" arguments in terms of facilitating formalization are not so compelling given the HoTT people haven't actually (as far as I know) formalized much mathematics - whereas (seemingly) less ideological communities like users of Lean have made great progress.
To expand on the comment about the philosophical arguments: take for example the abstract of this article. It states:
> It is common in mathematical practice to consider equivalent objects to be the same, for example, to identify isomorphic groups. In set theory it is not possible to make this common practice formal. For example, there are as many distinct trivial groups in set theory as there are distinct singleton sets. Type theory, on the other hand, takes a more structural approach to the foundations of mathematics that accommodates the univalence axiom. This, however, requires us to rethink what it means for two objects to be equal.
It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.
Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
HoTT doesn’t blur those distinctions — it formalizes the distinction.
The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
> ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
Counterpoint: no it doesn’t, because almost every working mathematician uses a higher level type theory in their work that “compiles” to ZFC and will run away screaming if you try to make them compile their work down to formal ZFC statements because set theory is a garbage foundation — the worst of the three options.
“My axioms do everything but formalize proofs!” is the equivalent of “my car does everything but drive!”
A good analogy is the idea of a Turing machine in theoretical CS. It's an idealized model for studying the theory of computation. To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
> The key idea of univalence is an axiom that says equivalence is equivalent to equality; and that if we only want equivalence as our standard, that we can substitute proofs of equivalence for proofs of equality.
I just said I don't want equivalence to be equivalent to equality!
> The main insight is that topology of diagrams determines the semantics of your logic; which helps us explore concepts like abstraction and proof simplification. (This relates to topos theory — which creeps up in CS fairly often.)
OK, so what are the concrete fruits of this? What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
I would argue that type theory does a better job at this than set theory. With set theory, you need to believe in two separate things: (1) the language of first-order logic (or some other logic) with its inference rules, (2) the set theory axioms. With type theory, there is only the language of lambda terms. And the rules for type theory are straightforward and intuitive for programmers, e.g., you can only call a function on an argument if the function's domain matches the type of the argument. Contrast that with set theory, where you have highly counterintuitive and seemingly arbitrary axioms like the axiom of separation.
Further, in ZFC, the only basic notation is that of a set. In something like the calculus of constructions, there are five fundamental notions (if I remember correctly). From the standpoint of ontological parsimony, that's a win for ZFC.
Axiom of separation just says we can make subsets of things - I think this is not so hard to swallow. I'm curious what you find counterintuitive about it.
Compared to CoC, first order logic is a model of simplicity, and I think it's reasonable to argue that adding the inductive types to get to CiC is as complex as adding a handful of axioms to Fol to obtain ZFC. And don't forget to pick a flavor of universe polymorphism or cumulativity to make it usable. That's not exactly simple.
I think there's a good case for CiC or HoTT being nice and usable for mathematicians. I don't think they're simple or more appealing to programmers. A kernel for metamath is the simplest, and it has more independent implementations than any other system.
I came to a different conclusion: they very much meant to ground mathematics in ZFC formalisms — and went to the effort of projects like Principia trying to achieve that. ZFC was a failure in this regard, almost immediately replaced by category theory and type theory.
> To object that it's impractical to write a complicated program like a computer algebra system using the Turning machine formalism misses the point.
No — it’s exactly the point.
That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.
> OK, so what are the concrete fruits of this?
Translating a type theory into a AST; translating an AST into bytecode. White boarding to design software. Formalisms for Feynman diagrams and similar.
Then you have that sheaves are the natural language for data fusion and sensor integration - which doesn’t apply to people who don’t know the topic, but is an industrial reason to learn it.
On the purely mathematical side, topos theory is what has shown relationships between many areas of mathematics, by showing when you translate those theories from their own language into categories you get equivalent structures.
> What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?
This is also a weird demand while leading off with how people don’t actually work in ZFC.
Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.
https://zmichaelgehlke.com/images/curry-howard-square-graphi...
- you can’t provide a solid basis for all math (though, ZFC is useful to prove that)
- you can’t use it to produce papers of increased assurance, eg to remove the issues that had arisen with contrary calculus proofs
Category theory was intended to solve a shortcoming of ZFC: the lack of tools to reason about “large” similarity and classes — such as algebra and geometry being the same topic. Category theory formalized those notions.
Ah, this is super interesting. Are there any good introductions to this topic, especially ones accessible to people who know some basic category theory and a bit about topoi, but who are weak at topology?
ZFC hasn't been "replaced" by anything. The standard line in all published textbooks that I'm aware of is that ZFC is the accepted (by the professional mathematical community) foundation for doing mathematics (assuming this question is even raised). Even the type theorists admit this!
> That’s why we replaced Turing machines with type theories, lambda calculus, automata, etc. Our modern research uses these formalisms because they’re outright better.
The Turing machine is a fundamental concept in theoretical CS that isn't going anywhere. Consider that the standard textbook on the theory of computation (Sipser's) has three parts, and the second is entirely devoted to studying computability using the Turing machine concept. Or that the strength of pushdown automata is usually explained in relation to Turing machines.
> OK, so what are the concrete fruits of this?
The first two things you listed are not metamathematical statements. I'm not sure what you mean by the third. (Sure, many things can be recognized as special cases of category-specific concepts. But that's a claim about category theory, not HoTT.)
> This is also a weird demand while leading off with how people don’t actually work in ZFC.
People do not write their papers in first order logic starting from the ZFC axioms, that's true. But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
> Nevertheless, topos theory is what explains the algebra-geometry duality: you have two languages (type theories) that map to isomorphic categories. You can then extend that idea to things like the Curry-Howard square.
OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
My experience is the opposite: ZFC hasn’t been “replaced” in the sense that it never was - we always used an intermediate language of established theory which we compiled to ZFC. ZFC never formalized all of mathematics, as the high level congruences that drove category theory were always developed on an independent framework. Further, computers always were grounded in type theory and diagram equivalence (literally, the correspondence between circuit diagrams and type theories).
> But the study of set theory has led to large number of metamathematical successes, such as forcing and the independence of the continuum hypothesis.
Are there any which don’t exclusively apply to the mechanics of set theory itself?
> The first two things you listed are not metamathematical statements.
I noted fruits ranging from applied mathematics (eg, computer products) to meta mathematics; I think it’s important to understand applications as well.
> OK, so what's the actual concrete statement an ordinary mathematician should be interested in?
That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
- we can encode proof engines as difference equations to run in GPUs
- we can extract some “effective type theory” from difference equations interpreted as diagrams, which preliminary results suggest also relates to convolutions
> Are there any which don’t exclusively apply to the mechanics of set theory itself?
Forcing has been applied to a variety of statements, including those about "normal" mathematics. The first example that comes to mind is the question of whether all automorphisms of the Calkin algebra are inner (Farah, 2011). There are many, many others.
> That the equivalence of algebra/geometry commutes with the equivalence of proof/computation has two practical effects:
You have still not given a statement an ordinary mathematician should be interested in! Type theory might good for engineering things - I'm totally on board with that. But if you claim HoTT has meta-mathematical interest, you need to give a meta-mathematical justification. That is, you need to prove something new (and interesting).
You told me your personal experience with textbooks and I told you mine. That’s how conversations work — why are you upset?
You’re also factually wrong: I was pointing out areas of mathematics that (contrary to your claim) were never formalized in ZFC.
> You have still not given a statement an ordinary mathematician should be interested in!
I don’t think you’re being sincere at this point: the formalisms to accelerate reasoning engines and to extract semantic content of DNNs is of clear interest to many working professionals.
- - - - -
I think both threads have something in common:
You’re dressing up your personal feelings (and ignorance) as grand statements about the field.
Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem. Again, I'll happily admit type theory can be good for engineering stuff. But you claimed it was good for metamathematical inquiry. I'm looking for a statement about things like consistency, independence, shapes, numbers, etc. Set theoretical inquiry gave us tons of those, as I pointed out above.
This is factually untrue — there a portions of mathematics never formalized on ZFC and there’s not consensus around that. I listed the areas that weren’t formalized on ZFC already.
You’re making bullshit up to make your personal biases sound grander than they are.
- - - -
> But you claimed it was good for metamathematical inquiry.
No — you claimed that, as a strawman of my position.
But you’re welcome to answer yourself: how do you formalize that equivalence is equivalent to equality without univalence?
You’re on a huff, but never addressed the original point. From my very first post.
> Extracting semantic content of DNNs is not a pure mathematical or metamathematical problem; it is an applied problem.
Wrong.
We lacked the meta mathematical framework outlining what semantics is to enable us to do that — until HoTT told us that the semantics of a system are in its topology. In that sense, HoTT is merely a fact about topos theory: the topology of your semantic model is the interesting part.
Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?" You proceeded to give examples that did not fit this description. If you agree that HoTT is not good for metamathematical inquiry, then great, we agree on something!
Also, DNNs are (definitionally) not a topic in pure mathematics.
I understand your ego doesn’t let you separate your experience from that others may have — and so anyone who doesn’t share your view is “objectively” wrong. That flaw in thinking is common in STEM personalities — but what you’re calling “objective” is your subjective bias.
> Also, re: the mathematical point, I asked above: "What new metamathematical statements - recognizable to an ordinary mathematician with no particular interest in topos theory or HoTT - has this led to?"
I answered in my very first post and reiterated it in the last one, but you still haven’t addressed that:
Equivalence is equivalent to equality.
How do you formalize that meta mathematical notion in other frameworks? — or are you going to ignore that a third time because you don’t have an answer?
> Also, DNNs are (definitionally) not a topic in pure mathematics.
Definitionally, the question “what is semantics?” is meta mathematics — even if you apply the answer.
My challenge to you: find a single book written in the last, say 50 years, where the answer to this question is not ZFC (or ZF with some equivocation about whether we should accept choice).
Re: "Equivalence is equivalent to equality," first of all, most mathematicians would take this to be false. Like, if "x" stands for cartesian product, they would say (A x B) x C and A x (B x C) are different objects. (This is a point commonly made in undergraduate algebra classes, and the reason they would say this is of course they they implicitly think of everything as sets, since set theory is the standard foundation!) They are isomorphic objects, but not equal ones. Second, to the extent that mathematicians suppress isomorphisms like this in their writing, this is not a new observation. We've known that mathematicians do this for decades, and in principle we could always unravel such isomorphisms when writing things down carefully if we needed to. This is not some special insight of HoTT. Compare to the forcing example I gave - this is a genuinely new insight about the Calkin algebra facilitated by "classical" methods of mathematical logic.
Re: DNNs, the question of what is a semantics for DNN does not count as an example, no. What would count: statements about things like consistency, independence, shapes, numbers, etc. It's cool that you can use HoTT for engineering things but it's not an application to discovering new pure mathematics or the consistency/proof strength/independence/etc. of that mathematics. The latter is the usual definition of "metamathematics."
Here's an example of a (true) metamathematical statement: HoTT is consistent if ZFC plus two inaccessible cardinals is consistent. (Interestingly, this is the best argument I'm aware of for the claim that HoTT is consistent, and its power derives largely from the fact that ZFC is the Gold Standard for foundations.)
Facilitating metamathematical inquiry of this kind is perhaps the primary reason mathematicians are still interested in set theory and classical logic. (I include here large cardinals, model theory, etc. For further discussion, see the books I mentioned above.)
Currently moving shape types to digital image transforms; next up is Zn.
https://www.zmgsabstract.com/whitepapers/shapes-as-digital-i...
https://www.zmgsabstract.com/whitepapers/shapes-have-operati...
There's tons of juice left on the CPU side. Again I recommend Metamath Zero (which is somewhat of an opposite direction as HoTT), as it's able to check the entire Metamath proof database in a few hundred milliseconds. This is orders of magnitude faster than most other proof systems.
If you did want to manipulate trees on the GPU, then my stack monoid work[1] might be a good basis for it.
Of course, a whole nother direction is to use AI to develop proofs, which is a fascinating and growing area (see Holophrasm[2] and DeepMind work[3]). That of course runs on the GPU.
[1]: https://arxiv.org/abs/2205.11659
[2]: https://arxiv.org/abs/1608.02644
[3]: https://www.deepmind.com/publications/proving-theorems-using...
It does? Where? I'm not huge in theoretical CS, but I have never seen topos theory show up in CS. Maybe I just didn't notice?
Of course I admit that Lean is pretty much cleaning everybody else's clock, but it's not clear to me that's because of the inherent superiority of type theory over set theory. It's equally plausible that it's just well engineered, and there's been a lot more attention on automating type theory by computer scientists.
The type theoretic approach is ultimately more elegant; the basic foundation is a bit more complex than material set theory, but the complexity is of a kind that's used basically everywhere in a practical formalization. It avoids the pattern of building complicated stuff on top of an overly simple axiomatic basis.
It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least compared to type theory. Automation of first-order logic is MUCH further and MUCH easier than automation of type theory, which is usually not much automated at all apart from a few tactics here and there.
Furthermore, the prevalent use of type theory for mechanised interactive theorem proving is based on the work of Church on simple type theory, and extensions of that into dependent types. Computer scientists like the lambda calculus and types, and it gives a nice and general way for implementing binding. It also is straightforward to compute in it, but that is also easy to implement for set theory if you are interested in it (most people doing set theory are not).
Ultimately, though, both set theory and type theory are just specific mathematical theories. This became apparent to me after I discovered what is probably the best foundational logic, Abstraction Logic (AL) [1], in which you can represent both as mathematical theories. AL is like first-order logic, but plus operators (and therefore binding), and like higher-order logic, but minus static types.
What is missing for AL is an actual system implementing it, but that is in the works.
[1]: https://obua.com/publications/philosophy-of-abstraction-logi...
There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.
To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.
Nevertheless, first-order logic is not the last word when it comes to formalising set theory, I think Abstraction Logic (AL)[1] is. When you start formalising set-like and type-like things in AL, the border between sets and types disappears. That border is just an artefact of history, useful for foundational studies, but will lose its importance for anything practical.
[1]: https://obua.com/publications/philosophy-of-abstraction-logi...
Martin-Löf type theory (and, therefore, homotopy type theory) is like an idealized programming language that is capable of expressing both programs and proofs, such that you can prove your code correct in the same language. Hacker News is a mostly technical community that often likes to geek out on programming languages.
Homotopy type theory is an especially cool flavor of type theory that finally gives a satisfying answer to the question of when two types should be considered propositionally equal.
One of my fondest memories was listening to Walid Taha debate Jeremy Siek, Todd Veldhuizen, and others, over beers, about the best way to define type equivalence in nontrivial type systems. It seemed so abstract, until I had to debug a template instantiation issue in GCC.
> So I am skeptical of any approach that wants to blur those distinctions.
The HoTT approach does not blur this; it says that isomorphism is equivalent to sameness, so there are ways to regard isomorphic objects as "much like the same" in some contexts while "not the same" in others.
It's easy. When you don't know a lot of math beyond college, but you see a post like this one, voting it up lets you pretend that you're in-the-know. "Oh yeah, I'm competent enough to upvote this. I know math." You may even end up fooling yourself into believing it. Same thing happens with physics, chemistry, linguistics... posts.
I do formalized mathematics as a hobby and I can not see any basis for that opinion.
Freek Wiedijk wrote an interesting paper [0] where he compared the complexity of various foundations as encoded in Automath.
Mizar, which is based on Tarski–Grothendieck set theory (an extension of ZFC) is a proof assistant whose library was the largest for a couple of decades, only recently surpassed by Lean's Mathlib (perhaps). Metamath is mentioned below in comments and of course my favorite Isabelle/ZF are also based on ZFC.
[0] [Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics] (https://www.sciencedirect.com/science/article/pii/S157086830...)
That might well be true for advanced mathematics, but in practical software engineering, TLA+, which uses ZFC for its "data" portion (its computational portion is based on a linear temporal logic called TLA), is not only the most popular of the "deep" specification languages (although that's not saying too much), but one of the most successful practical applications by ordinary practitioners (i.e. not logicians or other academic researchers) of deep formal logic in the history of formal logic. True, most users don't bother writing deductive proofs in the TLA+ proof assistant and prefer using model checkers available for TLA+ because they have a higher ROI, but still.
> My view is that all the "philosophical" arguments in favor of it (vs. the standard set theory foundations) misunderstand the issues at play.
Perhaps ironically, it is precisely the power of the notion of isomorphism that means it is often simpler and more practical to keep it in the meta-logic and work with a particular representative with a particular equality rather than baking the very notion of isomorphism into the heart of the logic itself (which is very interesting from a logician's perspective, but doesn't necessarily lead to better pragmatic results for practitioners). I.e. it is because isomorphism is so fundamental that we don't need it in the logic, and it can serve as the foundation for a foundation rather as the foundation itself. Of course, logicians enjoy exploring taking as much of the meta-logic and philosophy and putting it into the logic. That's pretty much what logicians are meant to do. Unfortunately, not too many of them are also interested in the question of how to make a logic more friendly to practitioners.
HoTT lets you do this when such a canonical representative exists. The point is to be able to generalize beyond that.
Of course, putting more meta-theory into the logic should be explored, and it's even possible that it may turn out to have other desired effects. However, a foundation is usually not of interest to practitioners for the same reasons it is of interest to logicians, and it is that point that logicians sometimes miss. They try selling a particular theory on the basis of things that are of interest to them (we've put isomorphism in the language) rather than things that are of interest to practitioners (proofs are shorter, written in a more natural way, easier for machines to assist with etc.). The reasons to research a topic are often not those that best sell it to others. In other words, would it also be "the point" for a practitioner "to be able to generalise beyond that"?
I think this question can easily be answered in the affirmative. A key point of HoTT and univalence is that being able to work with isomorphism as if it was equality, and freely transport proofs and functions 'across' isomorphisms, makes for more intuitive proofs that get less bogged down in issues of logical formalism and closer to what a practitioner would want to write.
(I don't know, and I don't have a dog in this fight, being neither a practitioner nor a logician. I'm asking because, following the thread of the discussion, I could easily see a logician saying "Of course this will make it easier for the practitioners" about something that, in actual practice, the practitioners don't care about at all.)
[1]: A computer can formally apply meta-logical transformations as a proof tactic, too. Why not put that into the logic if it can be done formally? To keep it simpler and easier for practitioners to learn. (Some systems, like TLA+, allow you to specify and prove higher order theorems that aren't expressible as formulas in the logic; so while you might not be able to express the general notion of an isomorphism in this way, you can express a theorem that can then be used by the proof assistant to transfer proofs based on isomorphisms with respect to some specific number of operators with some specific arities)
Come to think of it, there's another aspect I don't understand. The validity of a theorem depends only on the assumptions used in the proof (so, for example, if I have a formal set theory proof that depends only on group axioms, then it applies to all groups). That is not a property that is usually expressible in the the logic -- it's a property of the proof theory of the logic -- but it is nevertheless true. Not being a logician, I'm not interested in writing proofs about my logic's proof theory, I don't need to define new proof rules as I don't develop new logics, and my logic's proof assistant is free to rely on theorems about the logic's proof theory. What do I, as a practitioner, gain by making the proof theory part of the logic?
Rather, set theory lets us say that questions about 7 are equivalent to other questions about sets. So, 7 is prime if and only if some claim about sets holds, stuff like that. We do indeed usually pick some particular set to represent the number 7 for the purpose of this translation, but that isn't a claim that 7 is that set (since, e.g., there are many ways to choose a set to represent 7). So one cannot ask questions like 'is the number 7 equal to the trivial group?' within ZFC but only questions like 'is the set I've chosen to represent 7 equal to the set I've chosen to represent the trivial group,' which - while strange - shouldn't cause any philosophical worries.
You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held.
There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically.
> You're very dogmatic about what people should accept from a foundation. You seem happy to accept an approach that has very little to say about practice, which is certainly an opinion, but not universally held.
> There is a point of view that foundations should reflect and inform practice - or maybe even challenge practice - and are not just there to make you feel more comfortable philosophically.
I don't understand this comment. Studying set theory has said a lot about mathematical practice - for instance, about what we can and can't hope to prove in certain systems, or about what axioms are needed for what statements. That's important stuff!
More generally, there's the question of what you hope to accomplish by supplying a foundation for mathematics. Any value claim about some foundational system is contingent on what goal you have. As I said above, if that goal is actually writing down computer-checkable formalized versions of complex proofs, then ZFC is perhaps not the foundation you want to use.
But, historically speaking, that was not what people had in mind. There was a desire to reduce mathematical reasoning to a few philosophically basic concepts so that we could be confident in its coherence and consistency. And a desire for providing a framework for studying mathematical reasoning itself. I think it's really important to understand this historical context, otherwise you end up with misleading claims like "ZFC is a bad foundational system because it doesn't help me formalize my research papers."
Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics (or even exist on equal footing, creating a plurality of foundational systems). If you take the goal of a foundational system to be practically formalizing proofs, we have no evidence HoTT is particularly suited for this, and (as far as I know) no serious movement by the HoTT community to actually realize this vision (relative to what the Lean community is doing). I'm not claiming the first mover in some space should always dominate, just that if the HoTT people want to arguing for their foundational system on the grounds that it assists in formalizing math, maybe they should actually demonstrate their superiority by formalizing some math. For a longer comment on this, see: https://xenaproject.wordpress.com/2020/02/09/where-is-the-fa....
So if we disregard formalization, the arguments in favor of HoTT that remain are philosophical ones. But, as I've explained elsewhere in this thread, I find them all misguided. They all basically seem like arguments about aesthetics but don't actually tell me why HoTT is better than ZFC for the philosophical goals mentioned above.
> But, historically speaking, that was not what people had in mind.
You have opinions about what you'd like from foundations. They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc.
> Further, the reason I get grumpy when HoTT stuff is posted here is that the postings are rarely explicit about just why, exactly, they think HoTT should supplant ZFC as the accepted foundation of mathematics
Nobody's really saying that. That's your own combative fanatasy or confusion. You're not a logician; you don't know foundations; and you're ignorant of logic-in-CS, based on your inability to understand some of the terms used and the following remark you've made:
> It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.
That word salad alone should make people stop listening to you. But this is HN, so *shrug*.
You are right maybe about combinatorics, but in this sort of maths, you are useless and oddly narrow-minded.
1) I haven't written anything about constructive logic because I don't care for it, and other issues seemed more interesting to discuss. Further, the law of excluded middle has a robust presence in modern mathematical practice. A foundational system without LEM essentially by definition cannot replace ZFC for the purpose that ZFC is used for within modern mathematics. I understood the discussion to be about what should be used to ground mathematical practice.
2) "You have opinions about what you'd like from foundations." Not really. Rather, there are different goals one might want a foundational system to achieve, and we can discuss the merits of systems based on how well they meet our desired goals. I have already said, for example, that if your goal is the practical formalization of complex proofs, then type theory might very well be suitable for achieving that goal (as demonstrated by Lean).
My objections in this thread have always been that HoTT proponents are not always precise about what goals they want to achieve, and why they think HoTT is best for achieving them. That is true even if I don't care for the stated goals.
3) "They are dogmatic and are not the opinions of those mathematicians working on foundations. Those mathematicians are interested in constructive logic, computability, the computational meaning of mathematics, replacing sets with topological spaces, replacing sets with objects closer to mathematical practice, etc." The work you've just characterized is not mainstream within the community of mathematicians working on foundations and logic. Go look at what gets published in the Journal of Mathematical Logic, for example. It's just a sociological fact that the constructivist stuff (in particular) is somewhat niche (outside of say reverse mathematics, which is different than what you noted). The views I express are fairly widespread, though I put them a bit more sharply than others.
Here's a question to illustrate this point: Who at an R1 math department works primarily on the issues you mentioned? Who got hired or got tenure on the basis of this work? I can't think of anyone off the top of my head. There are at best a few topologists who got hired for their topological work who branched out into these things later. I don't doubt that if you search you can find a handful of examples - but that number is going to be much smaller than the equivalent number of people doing "classical" set theory and logic.
4) What's so wrong with not wanting the univalence axiom in my foundational system? Or thinking that this axiom is in fact a negative? It's not very ontologically primitive, after all.
But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group". You're saying that set theory doesn't even attempt to do this, so it seems that this is one thing that type theory does a better job of addressing. Mathematicians commonly engage in what are formally abuses of notation, mixing up equivalence classes and their representatives, or neglecting distinctions between sets that are defined quite differently and related by an injection, e.g. the natural numbers and the integers. These arguments need some fixing before they can be made logically rigorous, and type theory helps with that.
> But the whole point is how to keep track of what questions one is evidently allowed to ask - what questions are demonstrably not as ill-posed as "is the number 7 equal to the trivial group".
I don't understand what you mean by "questions one is evidently allowed to ask." You can ask any questions you want. In particular, as long as we agree that whatever question you want to ask can be translated into a question about sets, we can resolve that question by answering the analogous question in the framework of ZFC. All I object to is the claim that some set is, ontologically speaking, the same as the number 7, and hence that set theory proves "junk theorems."
Here's a silly analogy. Suppose we work at NASA and we want to fly a rocket to the moon. We agree that the answer the question of how much fuel we need, we can write a computer simulation with a representation of the rocket, the earth, the moon, and so on. We run the simulation and answer our question in that simulation, and if the simulation is a good representation of reality that also answers our question in reality, and then we go to the moon and everyone is happy. However, nowhere in this process do we believe that the rocket in the simulation is the same thing as the rocket IRL.
But how can you know this? You're starting from reasoning in natural language that, by your own admission, sometimes engages in "sloppy" abuses of notation, such as treating isomorphism as if it could be equated with identity. Whenever mathematicians argue that "this can be written down formally in ZFC" they're essentially using a sloppy, informal, ad-hoc version of type theory and higher-level logic in the process; they're merely in denial about this point.
Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?
Genius! I'm reading your comment in my best Boris Karloff (Grinch) voice. You just improved my already-nice Christmas morning :)
HoTT serves as a good foundation for constructive logic; perhaps better than any other. Set theory (like ZFC) makes doing constructive logic very awkward, as the very idea of an infinite set (which can be union'd and intersected with any other infinite set) is unnatural in such a logic (but can be made to work if you accept some pain). Martin-Lof Type Theory isn't "good enough", because it handles equality quite poorly, which is fundamental to logic. For instance, how would you state the Axiom Of Unique Choice in Martin-Lof Type Theory?
The idea behind HoTT (over Martin-Lof TT) is that path-connectedness in a topological space is somehow more fundamental than equality. Equality is recovered when that space becomes discrete. Everything that's possible in set theoretic foundations is possible in HoTT, because a set is just a discrete topological space. Equivalence relations are constructed by simply building bridges between points, and then contracting connected components down to points.
The idea behind Martin-Lof TT is that there is a rough duality between how you prove things and how you program things. Propositions correspond to types in MLTT, and proofs correspond to programs. In MLTT, this is taken to be an isomorphism between proofs->programs and propositions->types. In HoTT, this is usually not taken to be an isomorphism, as propositions are instead understood as only some of the types (the subsingletons).
In MLTT, the whole point of constructive logic becomes clear. The proposition "There are infinitely many prime numbers" is a type (like in some programming languages) whose elements are programs which take integers as input and produce larger primes as output. If you look at the standard proof of "There are infinitely many prime numbers", you'll see that it determines an algorithm. This is not the best example, as the resulting algorithm is rather naive, but there are plenty of better examples.
> It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.
It's called inverting a surjective function. You can do that in HoTT, or any foundation. In fact, this remark shows you're dangerously over-opinionated.
> Also, more to the point: ZFC does everything we need a foundation to do extremely well, except serve as a basis for practical formalization of proofs.
What does ZFC really do? The axioms are pretty obtuse, abstract, divorced from mathematical practice (who the hell needs to know that an integer is an infinite set), infinitary and non-constructive and hostile to computers.
How so? How, specifically, does computing need the absence of the Law of Excluded Middle?
Admittedly, I exaggerated a bit because my comments were already too long. You can always prove an algorithm correct by using LEM somewhere. It's just nice to have a mathematical universe where "everything is computable" which immediately rules out LEM.
This paragraph betrays that you have not done much work at all with HoTT. Type theory would be inconsistent if distinguishable objects could be substituted. It is not accurate to say that they are treated as "literally the same". Indeed the whole point of HoTT is that substitutive equality is not the only useful kind.
Lisps are very different than non-lisps, but… what’s contrarian about that?
This book looks to be based on those notes (which themselves came from a course a year earlier).
I’d definitely recommend this book on the strength of that experience.
[1] - https://hott.github.io/HoTT-2019/images/hott-intro-rijke.pdf
https://github.com/martinescardo/HoTTEST-Summer-School/tree/... https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_su...
I didn't really have time for the school, but I'm working through the book to learn MLTT. (Although I took a break to work through PLFA and do advent of code.)
> The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.
I've seen a number of other book-length items on the arXiv before, including e.g. Seven Sketches in Compositionality [1], so this isn't a particularly new trend, either.