See [[nlab:higher inductive type]] [[!redirects HIT]] [[!redirects HITs]] [[!redirects higher inductive types]] [[!redirects higher inductive definition]] [[!redirects higher inductive definitions]] [[!redirects Higher inductive type]] [[!redirects Higher inductive types]] ## Idea ## A way to specify elements with constructors like an [[inductive type]] but also specify [[paths]] and higher paths. ## Definition ## ## Examples ## ## List of HITs ## * [[circle]] * [[interval]] * [[2-sphere]] * [[suspension]] * [[mapping cylinder]] * [[truncation]] * [[pushout]] * [[set quotient]] * [[localization]] * [[spectrification]] ## Properties ## ## References ## [[HoTT book]] Expositions include * [[Mike Shulman]], _Homotopy type theory IV_ ([blog entry](http://golem.ph.utexas.edu/category/2011/04/homotopy_type_theory_vi.html)) * [[Peter LeFanu Lumsdaine]], _Higher inductive types, a tour of the menageries_ ([blog post](http://homotopytypetheory.org/2011/04/24/higher-inductive-types-a-tour-of-the-menagerie/)) * [[Peter LeFanu Lumsdaine]], _Higher Inductive Types: The circle and friends, axiomatically_ ([pdf](http://pages.cpsc.ucalgary.ca/~robin/FMCS/FMCS2011/Lumsdaine_slides.pdf)) Details of the semantics are in * {#LumsdaineShulman17} [[Peter LeFanu Lumsdaine]] [[Mike Shulman]], _Semantics of higher inductive types_ ([arXiv:1705.07088](https://arxiv.org/abs/1705.07088), talk slides [pdf](http://home.sandiego.edu/~shulman/papers/cellcxs.pdf)) with precurors in * {#ShulmanLumsdaine12} [[Mike Shulman]], [[Peter LeFanu Lumsdaine]], _Semantics of higher inductive types_, 2012 ([pdf](http://uf-ias-2012.wikispaces.com/file/view/semantics.pdf/410646692/semantics.pdf)) * {#ShulmanLumsdaine16} [[Mike Shulman]], [[Peter LeFanu Lumsdaine]], _Semantics and syntax of higher inductive types_, 2016, ([slides](http://home.sandiego.edu/~shulman/papers/stthits.pdf)) Discussion of a a subset of the HITs is in: * [[Kristina Sojakova]], _Higher Inductive Types as Homotopy-Initial Algebras_ [arXiv:1402.0761](http://arxiv.org/abs/1402.0761) * [[Steve Awodey]], [[Nicola Gambino]], [[Kristina Sojakova]], _Homotopy-initial algebras in type theory_ ([arXiv:1504.05531](http://arxiv.org/abs/1504.05531)) * [[Michael Rathjen]], _[Homotopical Inductive Types](http://www2.macs.hw.ac.uk/~cm389/hexmaps/2014/03/epsrc-ict-50/grants/EP-K023128-1.php)_ on [[higher inductive types]] category: type theory