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