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. ## Semantics * A sketchy note by [[Mike Shulman]] and [[Peter Lumsdaine]] about semantics of HITs in model categories, including simplicial sets: [[hit-semantics.pdf:file]]. One day it will become a paper or two. [[!redirects HIT]] [[!redirects HITs]] [[!redirects higher inductive types]] [[!redirects higher inductive definition]] [[!redirects higher inductive definitions]]