Equality expressions

The syntax system needs expressions for representing equality between morphisms or other terms. In a bicategory of relations, we also need expressions for subsumptions.

Both equalities and subsumptions can be thought of as 2-morphisms in a locally posetal 2-category. Thus, it's natural to reuse the existing GAT and syntax machinery. The main issue to address is that the 2-morphisms are "unnamed": there exists at most one equality between two terms.