How to prove equations using diagrams, part 3

The concept of initial functor provides a categorical and operational semantics for equational reasoning with diagrams. So far, we have explored this thesis in the simplest possible setting, that of a bare category, or, in logical terms, of an equational theory with unary function symbols. This is rather restrictive. The standard setting for equational reasoning was historically the starting point of both categorical logic (Lawvere 1963) and e-graphs (Nelson 1980; Nelson and Oppen 1980): a category with finite products, viewed as an algebraic theory.

In this post, we extend the initial functor semantics from bare categories to categories with finite products. Surprisingly, this turns out to be, in a sense, trivial: the definition of initial functor need not be modified beyond asking that it preserve products. We can therefore jump straight into the rules of the formalism and an example calculation. Only in the final section, which is more technical, do we justify why the formalism need not be substantively changed from the unary setting.

For our purposes, a category is cartesian if it has finite products, and a functor between cartesian categories is cartesian if it preserves finite products. A diagram D: \mathsf{J} \to \mathsf{C} in a cartesian category \mathsf{C} is cartesian if its shape \mathsf{J} is a cartesian category and the functor D is itself cartesian.

Cartesian categories and functors are familiar; cartesian diagrams less so, as limits or colimits are not usually indexed by categories assumed to have products. When taking limits in a cartesian category, there is no harm in taking the diagrams to be cartesian too, since a cone over a cartesian diagram is uniquely determined on its leg at a product of objects by its legs at each factor. This follows from the naturality of the cone with respect to product projections. Not only is there no harm in taking the diagram to be cartesian, it is important for us to do so since the diagram’s shape will encode systems of equations involving multiary operations.

The initial functor semantics has the virtue of being invariant: it does not depend on a particular way of presenting cartesian categories or cartesian diagrams. Even so, we often restrict to diagrams whose shapes are freely generated by a combinatorial structure. Such diagrams are syntactical in nature and resemble data structures used by computer scientists.

Recall that a free diagram is a diagram whose shape is a category freely generated by a graph. We say that a free cartesian diagram is a cartesian diagram whose shape is a cartesian category freely generated by a multigraph.1 There are several ways to explicitly describe the free cartesian category generated by a multigraph (see also Walters 1989), but we need not settle on one at this stage. The abstract characterization, given by the free-forgetful adjunction between cartesian categories and multigraphs, says that a free cartesian diagram D: F(M) \to \mathsf{C}, indexed by a multigraph M, is the same thing as a homomorphism2 M \to U(\mathsf{C}) from M into the underlying multigraph of \mathsf{C}. The latter is combinatorial data.

Under the logical perspective—that the objects and morphisms of a cartesian category \mathsf{C} are the types and operations of an algebraic theory—a free cartesian diagram in \mathsf{C} becomes a term graph over the algebraic theory. As formalized here,3 a term graph encodes terms as paths in a multigraph and, simultaneously, equations between terms by two or more multiedges incoming to a vertex. We illustrate this encoding through a toy example. Note that we draw term graphs differently than in the source material, in keeping with our different formalization of the concept.

Let \mathsf{C} be the signature with (i.e., the free cartesian category generated by) a type X and a binary operation {f: (X, X) \to X}. Then the terms f(a, b) and f(f(a, b), b) with free variables a: X and b: X, as well as the equation f(a, b) = a, can be encoded by the term graph (i.e., the free cartesian diagram) in \mathsf{C}:

Due to the equation, the diagram includes redundant data. Later, we will see how to reduce it using congruence closure.

Note that, despite a superficial resemblance, cartesian diagrams are not string diagrams: they have no inputs or outputs, nor a preferred sense of direction.

In the operational semantics, morphisms between cartesian diagrams are more important than the diagrams themselves. Recall that a morphism of diagrams in a category \mathsf{C} is a functor between their shapes forming a commutative triangle over \mathsf{C}. In other words, the category of diagrams in \mathsf{C} is the slice \mathsf{Cat}/\mathsf{C}. A morphism of cartesian diagrams is a morphism of diagrams that is also cartesian as a functor; so, the category of cartesian diagrams in a cartesian category \mathsf{C} is the slice \mathsf{Cart}/\mathsf{C}.

We show how to derive equations using cartesian initial functors by first establishing the rules—themselves examples of cartesian initial functors—and then carrying out a small calculation. As hinted at the outset, a cartesian initial functor is nothing other than a functor that is both cartesian and initial.

We record a few important motifs, extending those in the first post to the cartesian setting. As in the second post, each motif is intended to be a rule of inference for diagrammatic reasoning.

Fix a cartesian category \mathsf{C}. To see that the functors below are initial, notice that pulling back along each one preserves limits; in fact, the limit of each diagram below is the product {X_1 \times \dots \times X_k} in \mathsf{C} (where k=4 in the final example).

Operation introduction: for any morphism f: (X_1, \dots, X_k) \to Y in \mathsf{C}, the map of cartesian diagrams

Congruence reduction: for any morphism f: (X_1, \dots, X_k) \to Y in \mathsf{C}, the map of cartesian diagrams,

sending both y and y' on the left-hand side to y on the right-hand side, is initial.

Equation elimination: for any morphism f: (X_1, \dots, X_k) \to Y in \mathsf{C}, the map of cartesian diagrams

Factorization: for any factorization of a morphism in \mathsf{C}, the map of cartesian diagrams from the diagram indexed by a single morphism to the diagram indexed by the shape of the factorization is initial. For example, given morphisms f: (X_1, X_2) \to Y_1,\quad g: (X_3, X_4) \to Y_2, \quad h: (Y_1, Y_2) \to Z in \mathsf{C}, the map of cartesian diagrams

Returning to the toy example, the morphism of cartesian diagrams,

sending both a and c on the left-hand side to a on the right-hand side, is an initial functor. It is an application of congruence reduction. The diagram on the right cannot be reduced further.

Cyclic term graphs encode infinitely many terms in the same equivalence class. In this case, the terms f(a,b), f(f(a,b),b), f(f(f(a,b),b),b), \dots are all equivalent to a.

As before, we say that two cartesian diagrams D: \mathsf{J} \to \mathsf{C} and D': \mathsf{J}' \to \mathsf{C} are weakly equivalent, denoted D \sim D', if they can be connected by a zig-zag of morphisms, each of which is an initial functor. Weakly equivalent diagrams have the same limit, whenever the limit exists.

We can derive new rules—valid in the sense of preserving weak equivalence—by applying the motifs above in either direction. Particularly important is the equation introduction procedure for an equation between composite morphisms in the base category \mathsf{C}: starting with a discrete cartesian diagram, we apply operation introduction in the forward direction to the common composite; then equation elimination in the backward direction; and finally factorization twice in the forward direction, once for each side of the equation in \mathsf{C}. For example, suppose morphisms f: (X_1, X_2) \to Y, \quad g: Y \to Z, \quad h: (X_1, X_2) \to Z in \mathsf{C} satisfy h = g \circ f. Then there is a weak equivalence of cartesian diagrams:

Let \mathsf{C} be the algebraic theory of a well-behaved lens. Thus, \mathsf{C} is the algebraic theory with signature comprising

A very well-behaved or lawful lens satisfies the further property:

The PutPut law is independent of the other two. However, a special case of the PutPut equation, with v = v', is derivable from the first two laws:

We are going to prove this by diagrammatic reasoning. In fact, the derivation is fairly trivial, but it is a known and noted fact in the lens literature (Fischer, Hu, and Pacheco 2015), and it illustrates the formalism.

Begin with the discrete cartesian diagram on S and V, representing the context s: S,, v: V. Since the right-hand side of the target equation is \mathtt{put}(s, v), a natural first step is to introduce the \mathtt{put} operation:

Recognizing a subterm of the PutGet law, introduce that equation at s and v too:

The morphism of diagrams on the right is a congruence reduction of \mathtt{put} at s and v. (We could have saved a few steps by immediately introducing the PutGet equation, but we wish to emphasize the mechanizability of such reasoning.) Next, we recognize a subterm of the GetPut law (replacing s with s'), so we introduce that equation at s':

The final morphism of diagrams is again a congruence reduction, this time of \mathtt{get} at s'.

The resulting cartesian diagram contains the target equation, though it takes a moment to see that. Since the first and the last cartesian diagrams are weakly equivalent, and since the limit of the first diagram is the product {S \times V}, the limit of the last diagram is the same. Consequently, any two parallel paths in the last diagram starting at s and v compose to equal morphisms in \mathsf{C}. Taking the endpoint s' and following the cycle at s' (for fixed v) either zero times or once, we deduce the PutTwice law:

s: S,, v: V \vdash \mathtt{put}(s, v) = \mathtt{put}(\mathtt{put}(s, v), v).

As explained previously, the foundational theorem about initial functors is the existence of the comprehensive factorization system (Street and Walters 1973), an orthogonal factorization system on \mathsf{Cat} having initial functors and discrete opfibrations as its left and right classes. It turns out that the comprehensive factorization works just as well for cartesian functors as it does for arbitrary functors. This fact, possibly surprising, justifies our claim that the initial functor semantics carries over to the cartesian setting without modification. The precise statement is:

Theorem 1 (Comprehensive factorization on \mathsf{Cart}) The comprehensive factorization system on \mathsf{Cat} restricts to an orthogonal factorization system on \mathsf{Cart}, the category of small categories with finite products and finite-product-preserving functors.

We do not know a source for this theorem in the literature, though we presume it known since it follows straightforwardly from other, well-documented facts. In any case, the purpose of this section is to present a self-contained proof.

To prove the theorem, we show that the explicit construction of the comprehensive factorization, when applied to a cartesian functor, is a factorization in which the intermediate category and both functors are cartesian, without further assumptions. The analysis of the right class—discrete opfibrations—is simpler, so we start there.

Discrete opfibrations correspond to copresheaves via the elements construction. A simple result says that the elements construction preserves cartesianness.

Lemma 1 Let X: \mathsf{C} \to \mathsf{Set} be a cartesian set-valued functor on a cartesian category \mathsf{C}. Then its category of elements, \mathop{\mathsf{El}}(X), is cartesian, and its canonical projection, the discrete opfibration {\pi_X: \mathop{\mathsf{El}}(X) \to \mathsf{C}}, preserves and reflects finite products.

Proof. The product of objects (c_i, x_i)_{i \in I} in \mathop{\mathsf{El}}(X) is given, in its first component, by the product in \mathsf{C}, and, in its second comp