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]] +--{.query} *This page is under construction. - Ali* =-- ## Idea ## A way to specify elements with constructors like an [[inductive type]] but also specify [[paths]] and higher paths. ## Definition ## ## Examples ## ## Properties ## ## References ## [[HoTT book]] category: type theory