UF IAS 2012 Archive
Higher Inductive Types

Notes and code from Mike Shulman’s Nov. 14 talk on a proposed general formulation of higher inductive types that could be implemented.

Notes from Mike Shulman’s Feb. 27 talk on semantics of higher inductive types in model categories (such as simplicial sets).

Some blog posts about: truncations, 1-HITs

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