Homotopy Type Theory higher inductive type > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

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.

Examples

Semantics

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.