Homotopy Type Theory
higher inductive type (Rev #2)

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.

Revision on March 4, 2014 at 01:12:27 by Alexis Hazell?. See the history of this page for a list of all contributions to it.