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 three 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 Constructor - these are constructors for terms of the identity type $s{=}_{P}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.²

Examples

Circle ($S^1$)

Definition

The circle $S^1$ is a Higher Inductive Type with one point and one non-trivial path from that point to itself.

Constructors:

• $\mathrm{base}:S^1$
• $\mathrm{loop}:\mathrm{base}=\mathrm{base}$

The circle is the simplest non-trivial Higher Inductive Type, representing the topological circle as a type with a single basepoint and a loop.

Link to original

Interval

Definition

The interval $I$ is a Higher Inductive Type with two distinct points and a path connecting them.

Constructors:

• $i0:I$
• $i1:I$
• $\mathrm{seg}:i0=i1$

The interval represents the unit interval $[0,1]$ from topology as a type with two endpoints and a path between them.

Link to original

Propositional Truncation

Definition

The propositional truncation $\parallel A\parallel$ is a Higher Inductive Type that truncates a type $A$ to a proposition (a (-1)-Type).

Given a type $A$, the propositional truncation $\parallel A\parallel$ has the following constructors:

• $|\_|:A\to \parallel A\parallel$
• $\mathrm{squash}:\forall x,y:\parallel A\parallel .(x=y)$

The first constructor embeds elements of $A$ into the truncation. The second constructor ensures that any two elements of $\parallel A\parallel$ are equal, making it a proposition.

Link to original

Pushout

Definition

The pushout $A{\bigsqcup }_{C}B$ is a Higher Inductive Type that serves as the general colimit form in homotopy type theory.

Given types $A$, $B$, $C$ and functions $f:C\to A$ and $g:C\to B$, the pushout $A{\bigsqcup }_{C}B$ has the following constructors:

• $\mathrm{inl}:A\to A{\bigsqcup }_{C}B$
• $\mathrm{inr}:B\to A{\bigsqcup }_{C}B$
• $\mathrm{glue}:\Pi (c:C).(\mathrm{inl}(f(c))=\mathrm{inr}(g(c)))$

The pushout glues together copies of $A$ and $B$ by identifying $f(c)$ in $A$ with $g(c)$ in $B$ for each $c:C$.

Link to original

Suspension

Definition

The suspension $\Sigma A$ of a type $A$ is a Higher Inductive Type defined as the pushout of the terminal maps $1\leftarrow A\to 1$.

Constructors:

• $N:\Sigma A$ (north pole)
• $S:\Sigma A$ (south pole)
• $\mathrm{merid}:A\to (N=S)$ (meridian)

The suspension can be visualized as taking a type $A$ and placing it as the “equator” between two poles, with paths (meridians) connecting the north pole to the south pole through each point of $A$.

Link to original

Spheres

Definition

The n-dimensional spheres $S^n$ are higher inductive types defined recursively using the suspension operation and the boolean type.

• $S^0=2$ (the boolean type)
• $S^{n+1}=\Sigma S^n$ (suspension of the n-sphere)

This recursive definition constructs spheres of arbitrary dimension, where each sphere is obtained by suspending the previous one.

Link to original

Torus

Definition

The torus $T^2$ is a Higher Inductive Type with a 2-dimensional path constructor, representing the topological torus.

Constructors:

• $b:T^2$ (basepoint)
• $p:b=b$ (first loop)
• $q:b=b$ (second loop)
• $s:p\cdot q=q\cdot p$ (surface witnessing commutativity)

The torus is defined natively as a HIT with a basepoint, two loops through that point, and a 2-dimensional path (surface) witnessing that the two loops commute.

Link to original

Set Quotient

Quotient

Definition

The set quotient $A/R$ is a quotient inductive type that quotients a type $A$ by a relation $R:A\to A\to \mathcal{U}$ and truncates the resulting type to a hSet.

Given a type $A$ and a relation $R:A\to A\to \mathcal{U}$, the set quotient $A/R$ has the following constructors:

• $|\_|:A\to A/R$
• $\mathrm{eq}:\Pi (x,y:A).Rxy\to |x|=|y|$
• $\mathrm{isSet}:\Pi (x,y:A/R).\Pi (p,q:x=y).(p=q)$

The first constructor embeds elements of $A$ into the quotient. The second constructor identifies elements that are related by $R$. The third constructor ensures that the quotient is a set by requiring that all parallel paths are equal.

Properties

Effectiveness: If $R$ is an equivalence relation, then $|x|=|y|$ implies that $Rxy$. Truncation: The set quotient is a hSet (set) by construction, due to the $\mathrm{isSet}$ constructor which is a truncation constructor.

Remarks

The set quotient does not require $R$ to be an equivalence relation a priori, though in practice it is often used with equivalence relations.

Without the set truncation, it is not garunteed that there is a unique path between any two elements, instead you get the free infinity groupoid.

Related Concepts

Higher Inductive Type Quotient Inductive Type hSet Truncation (HoTT) Equivalence Relation

Link to original

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

Footnotes

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

2. TODO: Understand this ↩