Higher Inductive Type

Idea

Higher inductive types (HITs) are a generalization of inductive types in homotopy type theory. Like a quotient inductive types, they define constructors, and ‘identity types’ specified by indexed identity equations between terms called path constructors, but extend the notion of path constructors to allow for higher path constructors which spececify identity types between identity types.

Definition

Syntax

An (indexed) higher inductive type $A:I\to \mathrm{Type}$ is specified by a set of constructors of two kinds:

• Point constructors - plain constructors used in inductive types these are specified by a chain of $\Pi$ types that end in $Ai$, for some $i:I$.
• Path constructors - these are constructors for terms of the identity type $s{=}_{A}t$ for $s,t:P$ where $P$ is either a point type ($Ai$) or a path type constructed in a well-founded way given below.

Path types, for a HIT $A:I\to \mathrm{Type}$, are themselved defined inductively like so:

• Given $i:I$ with $s,t:Ai$. Then $s{=}_{Ai}t$ is a path type.
• Given some path type $P$ for $A$, with $p,q:P$ then $p{=}_{P}q$ is a path type.

Semantics

HITs can be thought of in simple cases as adding a higher-quotient to an inductive type, providing the least identification that satisfies the specification¹

Higher inductive types themselves are incompletely understood within HoTT. Cubical type theory provides the most complete existing support for HITs, with models including cubical sets and CCHM. Simplicial Set (Kan complexes) have good support for many HITs but require quotient-inductive or cell presentation.²

See also

Inductive Type Coinductive Type Quotient Type Quotient Inductive Type Inductive-Inductive Type Inductive-Coinductive Type Infinitary (Co)inductive Type Finitary (Co)inductive Type

Duplicate Content 1

Higher inductive types themselves are not well understood within Homotopy Type Theory.

Footnotes

1. TODO: Check. This should be made a lot more precise. ↩

2. TODO: Understand this ↩