Homotopy Type Theory
higher inductive type (Rev #5, changes)

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

A Seehigher inductive type (HIT)higher inductive type 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 June 25, 2018 at 11:47:32 by Bas Spitters. See the history of this page for a list of all contributions to it.