Inductive-Inductive Type

Idea

In type theory, an inductive-inductive type is a way of constructing a multi-sorted uniform tree structure that is well-founded, where later sorts may be indexed on prior sorts, and all constructors may refer to all other types and constructors.

Like inductive types, these can be encoded using Tarski universe. We model inductive types as the least fixed points of strictly positive endofunctors. This approach relies on a universe of codes (often denoted $U$) describing the grammar of these functors, an interpretation function $[[\_]]$ mapping codes to functors, and a fixed point constructor.

Syntax

Note: For simplicity we only give the definition of 2-sorted IITs. We define the type of codes $U_A:{\mathcal{U}}_1$, $U_B:U_A\to {\mathcal{U}}_1$ inductively, where, crucially codes for $U_A$ do not depend on $U_B$. ¹ A minimal presentation equivalent to W-types with polynomial adjustment includes:

$$\begin{array}{rlr}\mathsf{data}& U_A:(X:\mathcal{U})\to {\mathcal{U}}_1\mathsf{where}& \\ & \dot{1}:U_{A}X& \text{(Identity/Recursive)}\\ & {\dot{\Sigma }}_A^K:(K:\mathcal{U})\to (K\to U_{A}X)\to U_{A}X& \text{(Constant Σ)}\\ & {\dot{\Pi }}_A^A:(K:\mathcal{U})\to U_A(X+K)\to U_{A}X& \text{(Argument K → A)}\\ & {\dot{\Pi }}_A^B:(K:\mathcal{U})\to (K\to X)\to U_{A}X\to U_{A}X& \text{(Argument K → B)}\end{array}$$

TODO: Write the definition for $U_B$ forsberg2013-inductive-inductive-thesis sect 3.2.3.

A code is finitary when $K$ is finite in all instances, otherwise it is infinitiary.

Interpretation

TODO

Semantics

TODO

See also

• Inductive Type
• Quotient Inductive Type
• W Type

References

forsberg2013-inductive-inductive-thesis dybjer1999-inductive-recursive kaposi2019-finitary-induction-induction altenkirch2011-inductive-inductive-semantics sestini2023-inductive-inductive-thesis forsberg2010-inductive-inductive-definition

Footnotes

1. See forsberg2013-inductive-inductive-thesis forsberg2010-inductive-inductive-definition. ↩