A way to specify elements with constructors like an inductive type? but also specify paths and higher paths.
Expositions include
Mike Shulman, Homotopy type theory IV (blog entry)
Peter LeFanu Lumsdaine, Higher inductive types, a tour of the menageries (blog post)
Peter LeFanu Lumsdaine, Higher Inductive Types: The circle and friends, axiomatically (pdf)
Details of the semantics are in
with precurors in
Mike Shulman, Peter LeFanu Lumsdaine, Semantics of higher inductive types, 2012 (pdf)
Mike Shulman, Peter LeFanu Lumsdaine, Semantics and syntax of higher inductive types, 2016, (slides)
Discussion of a a subset of the HITs is in:
Kristina Sojakova, Higher Inductive Types as Homotopy-Initial Algebras arXiv:1402.0761
Steve Awodey, Nicola Gambino, Kristina Sojakova, Homotopy-initial algebras in type theory (arXiv:1504.05531)
Michael Rathjen?, Homotopical Inductive Types on higher inductive types