Idea
In type theory, an indexed inductive type is a generalization of (simple) inductive types, providing a way of constructing a uniform well-founded tree structure in which each node depends on an index.
Inductive types can be encoded using Tarski universe. We model inductive types as the least fixed points of strictly positive endofunctors. This approach relies on a Tarski universe (often denoted ) describing the grammar of these functors, an interpretation function mapping codes to functors, and a fixed point constructor.