10 ms·

Introduction to Homotopy Type Theory

153 points by euler1729 4y ago

paulpauper 4y ago
isn't arxiv for papers, not books/summaries? I am sure it is useful but does not belong there.
- spekcular 4y ago
  People have posted books on arxiv for at least a decade. Their rules state: "Submissions to arXiv should be topical and refereeable scientific contributions that follow accepted standards of scholarly communication."
- Twisol 4y ago
  As I understand it, submissions are moderated (albeit lightly -- not to the degree of formal peer review). So, since it's on the arXiv, we can assume that the moderators felt it belongs there. 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. [1] https://arxiv.org/abs/1803.05316v3 https://arxiv.org/abs/1803.05316v3
  - godelski 4y ago
    To post there you simply need someone to vet you. Typically your advisor, coauthor, or a colleague but they don't check the relationship. The system is rarely abused tbh. Introductions, surveys, and books are actively welcomed. At least I welcome them and find them extremely useful. We want open access (and open source) knowledge, right?
- hyperjeff 4y ago
  fwiw, arxiv has posted book-length works since it started in the early ‘90s.
zmgsabst 4y ago
I haven’t read the textbook, but Egbert did a session at the HoTT 2019 summer school — which was excellent. [1] 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://hott.github.io/HoTT-2019/images/hott-intro-rijke.pdf
- dunham 4y ago
  Also, a draft of book itself was used for the 2022 summer school: https://github.com/martinescardo/HoTTEST-Summer-School/tree/main/HoTT https://github.com/martinescardo/HoTTEST-Summer-School/tree/... https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html 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.)
spekcular 4y ago
I realize it's Christmas Eve, but this post tempts my inner curmudgeon. 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.
- zmgsabst 4y ago
  > So I am skeptical of any approach that wants to blur those distinctions. 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!”
KhoomeiK 4y ago
Here's a short paper that I spent several hours grokking as my first intro to Homotopy Type Theory, and which eventually sent me down a journey learning algebra, topology, and logic in order to fully understand HoTT: https://mathweb.ucsd.edu/~ebelmont/hott.pdf https://mathweb.ucsd.edu/~ebelmont/hott.pdf
throwaway81523 4y ago
Is this supposed to be more accessible than the HoTT textbook that's been maintained on Github for some years? https://github.com/HoTT/book https://github.com/HoTT/book
- turminal 4y ago
  Yes, from the abstract: > The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.

153 points by euler1729 4y ago

paulpauper 4y ago

isn't arxiv for papers, not books/summaries? I am sure it is useful but does not belong there.

spekcular 4y ago
People have posted books on arxiv for at least a decade. Their rules state: "Submissions to arXiv should be topical and refereeable scientific contributions that follow accepted standards of scholarly communication."
Twisol 4y ago
As I understand it, submissions are moderated (albeit lightly -- not to the degree of formal peer review). So, since it's on the arXiv, we can assume that the moderators felt it belongs there. 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. [1] https://arxiv.org/abs/1803.05316v3 https://arxiv.org/abs/1803.05316v3
- godelski 4y ago
  To post there you simply need someone to vet you. Typically your advisor, coauthor, or a colleague but they don't check the relationship. The system is rarely abused tbh. Introductions, surveys, and books are actively welcomed. At least I welcome them and find them extremely useful. We want open access (and open source) knowledge, right?
hyperjeff 4y ago
fwiw, arxiv has posted book-length works since it started in the early ‘90s.

zmgsabst 4y ago

I haven’t read the textbook, but Egbert did a session at the HoTT 2019 summer school — which was excellent. [1] 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://hott.github.io/HoTT-2019/images/hott-intro-rijke.pdf

dunham 4y ago
Also, a draft of book itself was used for the 2022 summer school: https://github.com/martinescardo/HoTTEST-Summer-School/tree/main/HoTT https://github.com/martinescardo/HoTTEST-Summer-School/tree/... https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html 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.)

spekcular 4y ago

I realize it's Christmas Eve, but this post tempts my inner curmudgeon. 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.

zmgsabst 4y ago
> So I am skeptical of any approach that wants to blur those distinctions. 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!”

KhoomeiK 4y ago

Here's a short paper that I spent several hours grokking as my first intro to Homotopy Type Theory, and which eventually sent me down a journey learning algebra, topology, and logic in order to fully understand HoTT: https://mathweb.ucsd.edu/~ebelmont/hott.pdf https://mathweb.ucsd.edu/~ebelmont/hott.pdf

throwaway81523 4y ago

Is this supposed to be more accessible than the HoTT textbook that's been maintained on Github for some years? https://github.com/HoTT/book https://github.com/HoTT/book

turminal 4y ago
Yes, from the abstract: > The book is entirely self-contained, and in particular no prior familiarity with type theory or homotopy theory is assumed.