A **higher inductive type (HIT)** is an inductive type whose constructors can output not just elements of the type itself, but elements of its [[path space]]s and higher path spaces. [[!redirects HIT]] [[!redirects HITs]] [[!redirects higher inductive types]] [[!redirects higher inductive definition]] [[!redirects higher inductive definitions]]