Indexed W-Type

Idea

Minimal form of indexed inductive types, formed as the initial algebra over an indexed containers.

Definition

An indexed W-type generalizes standard W-types to represent dependent inductive families. Given an index type $I$, an indexed W-type is specified by a Polynomial Functor over the slice category over $I$. We define it using four parameters:

1. $I:\mathcal{U}$, the type of indices.
2. $A:I\to \mathcal{U}$, the family of shapes or constructors for each index.
3. $B:(i:I)\to A(i)\to \mathcal{U}$, the family of arities or positions for each constructor.
4. $C:(i:I)\to (a:A(i))\to B(i,a)\to I$, the function assigning an index to each recursive subtree.

The indexed W-type $W_I^{A,B,C}:I\to \mathcal{U}$ is defined by the following rules.

Formation

$\frac{I:\mathcal{U}A:I\to \mathcal{U}B:(i:I)\to A(i)\to \mathcal{U}C:(i:I)(a:Ai)\to Bia\to I}{W_I^{A,B,C}:I\to \mathcal{U}}$

Introduction

The canonical constructor $\sup$ takes an index $i$, a shape $a$, and a function producing subtrees of the correct recursive indices prescribed by $C$.

$\sup :{\prod }_{i:I}{\prod }_{a:A(i)}\left({\prod }_{b:B(i,a)}{W}_I^{A,B,C}(C(i,a,b))\right)\to W_I^{A,B,C}(i)$

Elimination

To eliminate into a motive $P:(i:I)\to W_I^{A,B,C}(i)\to \mathcal{U}$, we require an inductive step function.

\text{ind} : & \prod_{i:I} \prod_{a:A(i)} \prod_{f:\prod_{b} W(C(i,a,b))} \left( \prod_{b:B(i,a)} P(C(i,a,b), f(b)) \right) \to P(i, \sup(i, a, f)) \\ & \to \prod_{i:I} \prod_{w:W_{I}^{A,B,C}(i)} P(i, w) \end{aligned}$$ ### Computation The computation rule states that eliminating a canonical $\sup$ term applies the step function to the recursive inductive applications. $$\text{ind}(\text{step}, i, \sup(i, a, f)) \equiv \text{step}(i, a, f, \lambda b. \, \text{ind}(\text{step}, C(i,a,b), f(b)))$$ ## See also * [[Homotopy Type Theory]] * [[W Type|W-type]] * [[Indexed Inductive Type]] ## References [[altenkirch2009-indexed-containers]]