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

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.

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