This is a list of texts I ended up reading to learn about HoTT and related subjects, with summaries of what they provide.
-
"Propositions as Types" - Wadler (12 pages): The best introduction to the Curry-Howard correspondence.
-
On the Interpretation of Intuitionistic Logic - Kolmogorov (1932, 7 pages): The Brouwer-Heyting-Kolmogorov interpretation is the basis for the Curry-Howard isomorphism. It states that we can reinterpret intuitionistic logic as related to "problems" and proofs as their "solutions" (programs).
-
A Brief Introduction to the Intuitionistic Propositional Calculus - Stuart A. Kurtz (8 pages): A concise introduction to the Curry-Howard isomorphism from the point of view of IPL.
-
The works of Per Martin-Lof:
-
"An Intuitionistic Theory of Types" (1972, 45 pages): His first paper describing what we now call dependent type theory.
-
"Constructive Mathematics and Computer Programming" (1982, 18 pages): His attempt to dumb things down for us computer scientists :) Real meat starts on page 4 of the PDF (page 170 of the text). Mostly a less formal summary of the 1972 paper.
-
Intuitionistic Type Theory (1980, 55 pages): This is a complete introduction to the theory. Surprisingly readable! Uses old terminology (calls types "sets" to make it more palatable for mathematicians).
-
-
Surveys:
-
"Type Theory and Homotopy" - Awodey (20 pages): A survey article on all of the above. Gets into model categories, etc. Not very accessible.
-
"Homotopy Type Theory and Voevodsky's Univalent Foundations" - Warren : Another survey. Long Coq tutorial at the end.
-
-
The HoTT Book aka The Book: This is the main text from which I've studied. Provides a comprehensive overview of the type theory before beginning on the homotopy, and really the 2nd chapter doesn't rely on much/any algebraic topology.
Naturally, I didn't read the entirety of each of these, I mostly picked and chose what was helpful at the moment.
-
Topological Manifolds - Lee
-
Algebraic Topology - Hatcher
-
Topology and Groupoids - Ronald Brown: An elementary introduction to the fundamental groupoid. Requires no previous knowledge of the fundamental group or category theory. Non-standard notation/terminology (interval groupoid, path category).
-
Categories for the Working Mathematician - Mac Lane: I don't forsee reading too much of this, but would enjoy it :)
-
Category Theory - Awodey: I'm mostly reading this on the side.
- "Just Kidding: Understanding Identity Elimination in Homotopy Type Theory" - Dan Licata: A great summary of the J rule, or as the HoTT book calls it, "path induction". Explains why we can always assume equalities with no/one fixed endpoint(s) are
refl.
Many of these didn't directly contribute to my understanding of HoTT so much as provide ideas for topics, and re-contextualize ideas that you see in The Book.
-
"Pattern Matching Without K": Dependent pattern matching requires axiom K, which is incompatible with univalence. Can we come up with a restricted version which doesn't use/require K?
-
"A Cubical Approach to Synthetic Homotopy Theory" - Daniel Licata: Using "cubical" ideas to simplify proofs. HoTT issue #689 is a feature request from Mike Shulman to add this. Might be a good topic!
-
"A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading" - Matthieu Sozeau: Readable even if you haven't heard of unification before. Good intuition behind how Coq fills in those
_s. -
"Homotopy Type Theory: A synthetic approach to higher equalities" - Michael Shulman: This one is a great complement to the HoTT book, it discusses the philosophical implications for the use of HoTT as a foundations, with a lengthy and accessible discussion of so-called "identifications".
-
"A Proposition is the (Homotopy) Type of its Proofs" - Steve Awodey: Short, non-mathematical introduction to HoTT. Talks about a "two dimensional universe" of mathematics, where one dimension is universe level ("size") and the other is h-level ("complexity"). Talks about the interval groupoid. Discusses "impredicative encoding" of HITs.
-
"100 years of Zermelo’s axiom of choice: what was the problem with it?" - Martin-Lof: Talks about the axiom of choice in type theory. Great Bishop quote.
-
- "Categorical Programming with Inductive and Coinductive Types": A thesis on initial algebras and final coalgebras for functors.
- "Recursive Types for Free!" - Wadler: An accessible introduction to initial algebras and final coalgebras for functors.
-
"An introduction to univalent foundations for mathematicians" - Grayson
-
"Non-wellfounded Trees in Homotopy Type Theory": The main inspiration for this thesis.
-
"Representing inductively defined sets by wellorderings in Martin-Lof's type theory" - Dybjer: "We prove that every strictly positive endofunctor on the category of [extensional types] has an initial algebra", and that these are W-types. Gives a breakdown of how to turn strictly positive functors into the form
Σ (a : A) (B a → X), and a few remarks on the intentional side. -
"Inductive Types in Homotopy Type Theory" - Awodey, Gambino, Sojakova: A great review of the status of W-types in extensional theories. Proves certain rules about W-types with propositional computation rules equivalent to the existence of an initial algebra for a polynomial functor.
-
"Containers: Constructing strictly positive types" - Abbott, Altenkirch, Ghani: Takes W-type thinking into the categorical setting, derives M-types from W-types.
-
Intuitionistic Type Theory (1980, 55 pages): One of the later sections is on W-types. Not nearly as accessible as the other papers mentioned here.
-
Learn Type Theory: A resource guide. This list overlaps a lot with that one.
-
Open problems in HoTT: On the HoTT wiki, which might prove useful.
- "Show that the Klein bottle is not orientable. (This requires defining 'orientable'.)"
- "Calculate more homotopy groups of spheres."
- "Can we verify computational algebraic topology using HoTT?"
-
Wiki: References: I should read through this list to see if there's anything that we should read.