Indexed Container

Definition

An indexed container generalizes standard the standard notion container to represent dependent inductive families. Given an index type $I$, an indexed container is specified with three components:

1. $S:I\to \mathcal{U}$, the family of shapes or constructors for each index.
2. $P:(i:I)\to Si\to \mathcal{U}$, the family of arities or positions for each constructor.
3. $J:\forall i\to (a:Ai)\to Pia\to I$, the function assigning an index to each recursive subtree.

Definition

An indexed container over $I$ is given by a record, written $S{◁}_{J}P$, where:

1. $S:I\to \mathcal{U}$ specifies shapes.
2. $P:(i:I)\to S(i)\to \mathcal{U}$ specifies positions.
3. $J:(i:I)\to (s:S(i))\to P(i,s)\to I$ specifies child indices.

Indexed Container Functor

Every indexed container freely generates an Indexed Functor $[[S{◁}_{J}P]]$. The action on an indexed family $X:I\to \mathcal{U}$ is given by:

$$[[S{◁}_{J}P]]Xi\equiv \sum _{s:Si}\prod _{p:Pis}X(Jisp)$$

The action on morphisms $f:{\prod }_{i}X(i)\to Y(i)$ applies $f$ post-compositionally to the subtree assignment:

$$[[S{◁}_{J}P]]fi(s,k)\equiv (s,\lambda p.f(Jisp),kp))$$

Initial Algebra

We define the indexed W-type ${\mathsf{IW}}_C$ as the carrier of the initial Indexed Algebra for the functor $[[S{◁}_{J}P]]$. The introduction rule is the algebra structure map:

$$\mathsf{isup}:\prod _{i:I}[[S{◁}_{J}P]]\mathsf{IW}i\to \mathsf{IW}i$$

The dependent elimination principle for ${\mathsf{IW}}_C$ states that for any displayed family $M:(i:I)\to {\mathsf{IW}}_{C}i\to \mathcal{U}$ equipped with a displayed algebra structure ${\alpha }_M$, there exists a unique section in the category of algebras:

$$\mathsf{elim}:\prod _{i:I}\prod _{w:{\mathsf{IW}}_C(i)}M(i,w)$$

The displayed algebra structure ${\alpha }_M$ corresponds exactly to the inductive step function, requiring that the motive holds for the parent node $\mathsf{isup}(i,(s,k))$ given that it holds for all recursive children at indices $J(i,s,p)$.

References

• Indexed Functor
• Indexed Algebra

• IW-type
• W-type
• Indexed Inductive Type

References

altenkirch2009-indexed-containers