higher inductive type (Rev #1)

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 spaces and higher path spaces.

Revision on February 18, 2014 at 12:39:14 by Mike Shulman. See the history of this page for a list of all contributions to it.