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]] category: type theory