Higher inductive types (HITs) are a generalization of inductive types which allow the constructors to produce, not just points of the type being defined, but also elements of its iterated identity types.

HITs are usually used along with the Path type in Cubical Type Theory.

Resources

history | excerpt history