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

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