Indexed Functor

Definition

Given an index type $I:\mathcal{U}$, an indexed functor is an endofunctor on the category of $I$-indexed families. In type theory, it is specified by a mapping on objects:

$$F:(I\to \mathcal{U})\to (I\to \mathcal{U})$$

Along with a mapping on morphisms, which are natural transformations between families:

$$F_1:\prod _{X,Y:I\to \mathcal{U}}\left(\prod _{i:I}X(i)\to Y(i)\right)\to \left(\prod _{i:I}F(X,i)\to F(Y,i)\right)$$

The mapping $F_1$ must preserve identity and composition either definitionally or propositionally.

Examples

$$\begin{array}{rl}(F_{\mathrm{Fin}}A{)}_n& :=\Sigma m:\mathbb{N}.(n=\mathrm{suc}m)\text{texttimes}(1+A_m)\\ (F_{\mathrm{Lam}}A{)}_n& :=\mathrm{Fin}n+A_n\text{texttimes}{A}_n+A_{\mathrm{suc}n}\end{array}$$

See also

• Functor

References

• altenkirch2009-indexed-containers