About

Higher inductive types (HITs) are a generalization of inductive types to higher dimensions. HITs are generated inductively by elements of itself and its iterated identity types. (from nLab)