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).

Note: this is work in progress.

Created on April 19, 2018 at 17:16:58 by Univalent foundations special year 2012