# Homotopy Type Theory higher inductive type

## Idea

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

## 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