System of Equations over a Container

Definition

Let $\Sigma =S◁P$ be a container. A system of containers over $\Sigma$ is specified by:

• A type $E:\mathcal{U}$
• A function $V:E\to \mathcal{U}$
• For each $e:E$, two elements $le,re:T_{\Sigma }(Ve)$

These represent the following notions.

• $E$ indexes the equations.
• $Ve$ indexes variables for each equation.
• $le,re$ represent AST’s in variables for the the left and right side of the equation.

Here $T_{\Sigma }(V)$ is the free $S_{\Sigma }$-algebra¹ on $V$. Specifically, it is the least type that consists of:

• $\eta :V\to T_{\Sigma }V$
• $\sigma :S_{\Sigma }(T_{\Sigma }V)\to T_{\Sigma }V$

References

fiore2022-quotient-inductive (definition 3.2)

Footnotes

1. Free Algebra ↩