UF IAS 2012 Archive Homotopy Type System

Here are materials related to Vladimir’s proposal for a type theory with two kinds of equality, called Homotopy Type System (HTS).

• Notes on HTS.
• Slides from a talk given on Joyal’s 70th birthday, 2/25/13.

Note: this is work in progress.