higher inductive type (Rev #4)

A **higher inductive type (HIT)** is an inductive type whose constructors can output not just elements of the type itself, but elements of its path space?s and higher path spaces.

- The circle

- A sketchy note by Mike Shulman and Peter Lumsdaine about semantics of HITs in model categories, including simplicial sets: Semantics of higher inductive types. One day it will become a paper or two.

Revision on May 15, 2014 at 08:32:07 by Mike Shulman. See the history of this page for a list of all contributions to it.