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. Unlike plain inducA stive types, we can’t model inductive types as the least fixed points of strictly positive endofunctors, since there are no longer a single sort. 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.

Codes

The syntax of inductive-inductive types is defiend in forsberg2010-inductive-inductive-definition.

It was extended, with initial algebra semantics to finitary and infinitary QIITs in Theory of Codes and Theory of Signatures.

Signature

An inductive-inductive type signature $\Sigma$ consists of:

• Sort symbols ${\dot{A}}_i$ for each $i\in [s]$.
• Sort signatures ${\Theta }_i[{\dot{A}}_{<i}]$ specifying the index type of ${\dot{A}}_i$, and referring only to previously defined sorts. The intended sort is $A_i:{\Theta }_i[A_{<i}]\to \mathcal{U}.$
• For each constructor $i\in [m]$:
  • a target sort ${\mathrm{sort}}_i\in [s]$;
  • a strictly positive telescope ${\Phi }_i[{\dot{A}}_{\ast }];$
  • a target index expression ${\tau }_i:{\Phi }_i[A_{\ast }]\to {\Theta }_j[A_{<j}],j:={\mathrm{sort}}_i.$

This generates a point constructor $c_i:(\phi :{\Phi }_i[A_{\ast }])\to A_j({\tau }_i(\phi )),j:={\mathrm{sort}}_i.$

Algebras

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

$$c_i:{\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{Q}]$ and each

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

the interpreted endpoints agree:

$$l_j(\psi )=r_j(\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.

Introduction rules

Let $Q$ be the type being defined. A quotient inductive definition consists of

• point constructors

  $$\frac{\psi :{\Phi }_i[Q]}{c_i\psi :Q}(i\in [m])$$

• path constructors

  $$\frac{\psi :{\Psi }_j[Q]}{p_j\psi :l_j(\psi ){=}_Q{r}_j(\psi )}(j\in [n])$$

where each ${\Phi }_i$ and ${\Psi }_j$ is a strictly positive telescope, and

$$\psi :{\Psi }_j[Q]⊢l_j(\psi ),r_j(\psi ):Q.$$

To ensure you get a set-level QIT and one is working outside of a UIP setting, then one also includes a truncation constructor asserting that $Q$ is a set.

Recursor

Let $A$ be a $\Sigma$-algebra. Then there is a unique function

$${\mathsf{rec}}_A:X\to A$$

such that for each point constructor $c_i$,

$${\mathsf{rec}}_A(c_i\psi )=c_i^A({\Phi }_i[{\mathsf{rec}}_A]\psi ),$$

Reduction to inductive types

It is known that inductive types reduce to inductictive types. Kaposi et al. showed that in the finitary case ¹ inductive-inductive types reduce to indexed inductive types using a erased mutually inductive type, which is filtered by a well-formedness predicate. Sestini later extended this to the infinitary case, giving a general reduction using the same approach as Kaposi et al. ²

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. kaposi2019-finitary-induction-induction ↩

2. sestini2023-inductive-inductive-thesis ↩