How to prove equations using diagrams, part 3

This post continues the exploration of initial functor semantics for equational reasoning with diagrams, extending the concept from bare categories to categories with finite products. The initial functor remains invariant, not relying on a specific presentation of cartesian categories or diagrams. However, diagrams are often restricted to those whose shapes are freely generated by certain combinatorial structures, resembling data structures in computer science.

A free cartesian diagram is one whose shape is a cartesian category freely generated by a multigraph. The abstract characterization of free cartesian diagrams is given by a free-forgetful adjunction between cartesian categories and multigraphs. This allows a cartesian diagram in a cartesian category C to be viewed as a homomorphism from the multigraph to the underlying multigraph of C. In logical terms, a free cartesian diagram becomes a term graph over the algebraic theory, encoding terms as paths in a multigraph and equations by multiple multiedges arriving at a vertex.

An example is provided to illustrate this encoding, using a signature with a binary operation on a type X. Morphisms between cartesian diagrams are important in the operational semantics and the category of cartesian diagrams in a cartesian category is the slice Cart/C. Cartesian initial functors are defined as functors that are both cartesian and initial, preserving limits and serving as examples of rules of inference for diagrammatic reasoning.