Higher Inductive Type

Idea

Higher inductive types (HITs) are a generalization of inductive types in homotopy type theory. Like quotient inductive types, they are specified by point constructors together with ordinary path constructors, but HITs also allow higher path constructors, that is, constructors whose targets are iterated identity types.

They were introduced to construct types corresponding to homotopy-theoretic cell complexes. ¹

Signature

A HIT signature consists of:

• A sort symbol $\dot{A}$.
• ${\Phi }_i[\dot{A}],{\Psi }_j[\dot{A}]$ be strictly positive telescopes for $i\in [m],j\in [n]$
• for each $j\in [n]$, specify , $d_j:\mathbb{N}$ as well as two terms,

$$\begin{array}{rlrlrlr}& \psi :{\Psi }_j[\dot{A}]& ⊢& l_j^0(\psi ),r_j^0(\psi )& :& \dot{A}& \\ & \psi :{\Psi }_j[\dot{A}]& ⊢& l_j^{k+1}(\psi ),r_j^{k+1}(\psi )& :& l_j^k(\psi )=r_j^k(\psi )& \forall k\in [d_j]\end{array}$$

specifying the two sides of the $j$th path constructor at level $d_j$.

From this signature, one generates point constructors

$$c_i:{\Phi }_i[\dot{A}]\to \dot{A}$$

and path constructors, where $k$ is the dimension the path is operating at,

$$p_j:(\psi :{\Psi }_j[\dot{A}])\to l_j^{d_j}(\psi )=r_j^{d_j}(\psi ).$$

Then for $d_j=0$, $p_j$ defines an ordinary path constructors, while for $d_j>0$, $p_j$ defines a higher path constructors.

Semantics

See lumsdaine2018-higher-inductive-types.

A full general syntax and semantics for HITs is still subtle, and not every proposed HIT is known to have a model in every setting.

Simplicial Set (Kan complexes) have good support for many HITs but require quotient-inductive or cell presentation.²

Algebras

An algebra for a HIT signature $\Sigma$ consists of a carrier type $A$ together with, for each point constructor arity ${\Phi }_i[-]$, an operation

$$c_i^A:{\Phi }_i[A]\to A.$$

These operations induce interpretations of all formal terms. The algebra satisfies the quotient part of the signature when, for each equation context ${\Psi }_j[\dot{A}]$³ and each

$$\psi :{\Psi }_j[A],$$

the interpreted endpoints agree:

$$l_j^A(\psi )=r_j^A(\psi ).$$

When the arities ${\Phi }_i$ are strictly positive, they usually assemble into a functor

$$S_{\Sigma }(X)=\sum _i{\Phi }_i[X],$$

so that a QIT algebra may be viewed as an $S_{\Sigma }$-algebra satisfying the specified equations.

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

Set 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 Set Quotient Quotient Inductive Type Inductive-Inductive Type

References

• hott2013-book
• lumsdaine2018-higher-inductive-types

Footnotes

1. hott2013-book ↩

2. kapulkin2012-simplicial-model-univalent ↩

3. Note that $\dot{A}$ is a symbol standing in for a type, whereas $A$ is a type itself. ↩