Higher Inductive Types (HITs)
Overview
Higher inductive types extend Martin-Löf–style inductive types by allowing constructors not only for points of a type but also for paths and higher paths between them. In homotopy type theory they encode spaces synthetically: e.g. the circle has a base point and a loop (path from the base to itself); pushouts, suspensions, and truncations are other standard HITs. Elimination principles generalize induction and recursion to respect these path constructors. Together with univalence, HITs support synthetic homotopy theory and constructive mathematics inside type theory.
Era: 2011–2013
Proposed at: Princeton, USA / Institute for Advanced Study
Formal structure
Domain: Type T; point constructors c : T; path constructors p : Id_T(a, b) or higher identity types
Example: S¹ with base : S¹ and loop : base =_{S¹} base; induction S¹-elim : Π(P : S¹ → Type). P(base) → (transport_P(loop) = id) → Π(x:S¹). P(x)
Constraints: Coherence of higher-dimensional constructors; cubical and related type theories provide canonicity and computation rules
Objective: Define homotopy types, colimits, and truncations without a separate topological model; basis for formalization in Coq, Agda, Lean (cubical), etc.