Homotopy Type Theory higher inductive type > history (Rev #12)

See higher inductive type

Idea

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

Definition

Examples

List of HITs

Properties

References

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 February 13, 2022 at 20:49:52 by Anonymous?. See the history of this page for a list of all contributions to it.