Indexed Algebra

Definition

Let $F$ be an indexed functor over $I$. An indexed algebra for $F$ is a pair $(X,\alpha )$ consisting of an $I$-indexed family $X:I\to \mathcal{U}$ and an evaluation map $\alpha$:

$$\alpha :\prod _{i:I}F(X,i)\to X(i)$$

Displayed Algebra

To perform dependent elimination, we define a displayed algebra (See Displayed Algebra) over a base algebra $(X,\alpha )$. Let $P:(i:I)\to X(i)\to \mathcal{U}$ be a displayed family over $X$.

A displayed algebra structure on $P$ requires lifting the functor action to the displayed family, typically denoted $\hat{F}P$, and providing a dependent map:

$${\alpha }_P:\Pi i:I.\Pi z:FXi.\hat{F}Piz\to Pi(\alpha iz)$$

The specific formulation of $\hat{F}$ depends on the internal structure of $F$, such as when $F$ is an indexed container.

References

• Algebra
• Initial Algebra