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.

• Lecture notes (significantly expanded from the talk itself)
• Coq code axiomatising “1-dimensional W-types” along the lines of this proposal (due to Peter L.)

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

• A rather dense note describing in some more detail the construction of semantics sketched in the talk, including indices, parameters, and coherence.

Some blog posts about: truncations, 1-HITs