Several links related to the type-theoretic formalization

of mathematics:

  1. Programming languages course taught in Princeton in the fall of 2009 using Coq:

In particular look at “schedule” which contains links to the lecture notes.

  1. Homepage of Steve Awodey who pioneered the study of the connections

between Martin-Lof identity types, homotopy-theoretic factorization axioms and omega-categories.

  1. Homepages of Thomas Streicher and Martin Hofmann.