Andrew J. Blumberg

Associate professor of mathematics, University of Texas at Austin
(blumberg(at)math.utexas.edu)

Sample menu:

• Home
• Research
  • Algebraic topology
  • Computational topology
  • Security and privacy
• Teaching
  • Homotopy type theory
• Locational privacy
  • The Jones case
  • FAQ
  • Writing
  • Press

Homotopy type theory

This is the homepage for Math 392, homotopy type theory.
Office hours are by appointment.

The syllabus is available here.

The first problem set is available here.
The second problem set is available here.
The third problem set is available here.
The fourth problem set is available here.
The fifth problem set is available here.

Two more good Coq tutorials are here and here.

References for simplicial sets:

• Riehl's leisurely introduction to simplicial sets
• Friedman's illustrated introduction to simplicial sets
• May's Simplicial objects in algebraic topology (which is still the best comprehensive reference)

References for homotopy theory and model categories:

• May's A concise course in algebraic topology
• Hatcher's Algebraic topology
• Dwyer and Spalinski's notes

A good reference for base-change functors (in the context of spaces):
May and Sigurdsson's Parametrized homotopy theory

References for the connection between dependent type theory and locally cartesian-closed categories:

• Seely's original paper
• Hofmann's fix via fibrations
• Curien's fix via relaxing the substitution rule
• Curien, Garner, and Hofmann's perspective on the fixes

The best reference for the correspondence between cartesian-closed categories and the untyped lambda calculus:
Scott and Lambek's book Introduction to higher order categorical logic.

References for lambda calculus and logic:

• Barendregt's "The lambda calculus: Its syntax and semantics"
  (brief notes.)
• Cori and Lascar's "Mathematical logic"

Some references for the first part of the class:

• The homotopy type theory website.
• Leinster's notes on topos theory.
• Mac Lane's "Categories for the working mathematician".
• Leinster's version of Lawvere's categorical set theory.
• Lawvere's paper on categorical set theory
• The Coq tutorial.