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

Showing changes from revision #1 to #2: 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 spaces and higher path spaces.path space?s and higher path spaces.