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

Showing changes from revision #9 to #10: Added | Removed | Changed

See higher inductive type

This page is under construction. - Ali


A way to specify elements with constructors like an inductive type? but also specify paths and higher paths.



List of HITs



HoTT book

Expositions include

Details of the semantics are in

with precurors in

Discussion of a a subset of the HITs is in:

category: type theory

Revision on October 10, 2018 at 09:31:05 by Ali Caglayan. See the history of this page for a list of all contributions to it.