Pictures are essential to conveying proofs and definitions (Pinto and Tall, 2002), and are thus common in traditional pen and paper mathematics. While proof assistants offer several benefits over pen and paper mathematics, proofs and definitions in proof assistants are entirely textual (i.e. lack images), and are thus often harder to convey than their traditional equivalents. This blog post changes this unsatisfactory situation by showing how to write pictorial definitions in a proof assistant. Specifically, this blog post shows how to write commutative diagrams for category theory in Coq.

Commutative diagrams are at the heart of category theory.

Category theory starts with the observation that many properties … can be unified and simplified by a presentation with diagrams of arrows [commutative diagrams].

– Mac Lane, “Categories for the Working Mathematician”

Yet, despite the importance of commutative diagrams, formalizations of category theory in proof assistants (of which there are many) do not support them. Until now! This project’s source code can be downloaded from GitHub.

This blog post starts by showing how to use commutative diagrams in Coq, and
then explains how they are implemented. In this blog post I won’t be able to satisfactorily explain category theory, but there are good explanations out there such as Milewski’s blog. The definition of `Category`

that I will use here is:

```
Class Category := {
object : Type;
morphism : object -> object -> Type;
id {A} : morphism A A;
composition {A B C} : morphism A B -> morphism B C -> morphism A C;
leftId {A B} {f:morphism A B} : composition id f = f;
rightId {A B} {f:morphism A B} : composition f id = f;
assoc {A B C D} {f:morphism A B} {g:morphism B C} {h:morphism C D} :
composition (composition f g) h = composition f (composition g h)
}.
Notation "A → B" := (morphism A B) (at level 45).
Notation "f ∘ g" := (composition f g).
```

Note that `∘`

’s arguments are flipped in comparison to the usual mathematical definition. Also, morphisms use the unicode `→`

arrow which is different from the function arrow `->`

.

Following is the definition of a category theoretical `Product`

using this notion of `Category`

to create a commutative diagram in Coq.

```
Class Product `{Category} := {
bundle : object -> object -> object;
factor {a b c:object} (p:c → a) (q:c → b) : c → bundle a b;
projL {a b:object} : bundle a b → a;
projR {a b:object} : bundle a b → b;
productOk {a b c} {p:c → a} {q:c → b} : denote (parse [
" ";
" p c q ";
" +--------o--------+ ";
" | | | ";
" | |factr | ";
" | | | ";
" v prjL v prjR v ";
" o<-------o------->o ";
" a bundle b ";
" "
] c a (bundle a b) b p (factor p q) q projL projR);
pairUnique {a b c} {p:c → a} {q:c → b} f :
f p q ∘ projL = p -> f p q ∘ projR = q -> f p q = factor p q
} % string.
```

The definition of `Product`

is standard, except the `productOk`

field. The `productOk`

field is defined using the ASCII art representation of a commutative diagram, which is first `parse`

d and then `denote`

d. The labels on the diagram (e.g. `factr`

and `prjR`

) are just decoration, the real labels (e.g. `(factor p q)`

and `projR`

) are passed as arguments to the `parse`

function. Can you guess why the labels have their `o`

’s removed? You can use Artist Mode to draw these diagrams in emacs.

Despite the definition of `productOk`

in terms of a commutative diagram, the `Product`

behaves just as you would expect. Consider for example the proof that Coq’s inductive definition of a product `prod`

in the standard library is a `Product`

in the category of `Coq`

.

```
Instance prodIsProduct : @Product Coq := {|
bundle := prod : @object Coq -> @object Coq -> @object Coq;
factor a b c p q x := pair (p x) (q x);
projL := fst;
projR := snd
|}.
```

The above construction is standard. But the proof of `productOk`

that follows is not. The initial goal is (to nobodies surprise):

```
forall (a b c : object) {p:c → a} {q:c → b} : denote (parse [
" ";
" p c q ";
" +--------o--------+ ";
" | | | ";
" | |factr | ";
" | | | ";
" v prjL v prjR v ";
" o<-------o------->o ";
" a bundle b ";
" "
] c a (bundle a b) b p (factor p q) q projL projR);
```

To prove this goal, we first introduce the variables, and then run the diagram parser and denote the result with `compute`

. It is instructive not to expand any definitions particular to `prod`

or the `Coq`

category.

```
Opaque morphism object composition id fst snd.
intros.
compute.
```

The resulting goal is the following.

```
q ∘ id = (fun x : c => pair (p x) (q x)) ∘ snd ∘ id) /\
(fun x : c => pair (p x) (q x)) ∘ fst ∘ id = p ∘ id
```

This goal is identical in meaning to the formula one would use instead of a commutative diagram, namely:

```
(fun x : c => pair (p x) (q x)) ∘ snd = q /\
(fun x : c => pair (p x) (q x)) ∘ fst = p
```

The remaining proofs that `prod`

is a `Product`

are trivial.

The rest of this blog post is structured as follows. The *Parsing* section explains how the `parse`

function turns the pictorial representation of the diagram into an internal representation, and how it asks for the right objects and morphisms for the vertexes and arrows of the diagram. The *Denotation* section explains how the `denote`

function translates the internal representation of the diagram into a formula.

The ultimate goal of the parser is to turn the pictorial representation of a diagram into an internal representation dubbed `Diagram`

. This internal representation is defined below.

```
Class Diagram `{Category} := {
Vertex : Type;
vertexObject : Vertex -> object;
Arrow : Vertex -> Vertex -> Type;
arrowMorphism {a b} : Arrow a b -> (vertexObject a) → (vertexObject b)
}.
```

A `Diagram`

consists of a set of vertexes (`Vertex`

), a set of arrows between any two vertexes (`Arrow`

), and two functions that map vertexes to objects (`vertexObject`

) and arrows to morphisms (`arrowMorphism`

) in a given category.

The first step toward translating pictorial diagrams to a `Diagram`

is to find all vertexes of the image `ps`

and all arrows along with their start and end vertexes `es`

. The function that does this is `(ps,es) = parseImage (img:list string) : list (Z*Z) * list ((Z*Z)*(Z*Z))`

. The function isn’t particularly interesting and I won’t explain its implementation.

The next step is to map the vertexes and arrows to objects and morphisms (remember that the labels on the commutative diagram are just decorative). To this end, the `parse`

function requires its caller to pass an object for each vertex, and a morphism for each arrow — i.e. the number of arguments to the function depends on the commutative diagram (compare this to `printf`

). Consequently, the type of the `parse`

function is a complex dependent type, that we will take a look at right now.

```
Definition parseType (img:list string) : Type.
```

`parseType`

first parses the diagram, resulting in a list of vertexes `ps`

and a list of arrows `es`

.

```
destruct (parseImage img) as [ps es].
```

Next, `parseType`

recurses over the vertexes `ps`

. For every vertex in `ps`

, the recursion adds an additional function parameter `forall o:object, _`

.

```
revert ps.
refine ((fix rec os (om:(Z*Z) -> option (index os)) ps :=
match ps with
| [] => _
| x::ps' => forall o:object, _
end) [] (fun _ => None)); revgoals.
```

The recursion also maintains two data structures. `os`

is the list of objects collected as parameters. `om`

is a function that maps each vertex to the `index`

of its corresponding object in `os`

. The following code keeps these data structures up to date.

```
{
refine (rec (o::os) _ ps').
refine (fun x' => if x =? x' then Some found else (om x') >>= _).
exact (fun oi => Some (next oi)).
}
```

Once `parseType`

has processed all vertexes, it recurses over the arrows `es`

.

```
clear rec ps.
revert es.
refine (fix rec es :=
match es with
| [] => Diagram
| (s,d)::es' => (fun T => _) (rec es')
end).
```

For every arrow, the recursion looks at the source `s`

and destination `d`

in the map from vertexes to objects `om`

. If that `lookup`

fails, the recursion simply ignores the arrow (which should make debugging very annoying). If the lookup succeeds, the recursion adds an additional function parameter with `forall m : ...`

. This concludes the definition of `parseType`

.

```
destruct (om s) as [si|]; [|exact T].
destruct (om d) as [di|]; [|exact T].
refine (forall m : lookup si → lookup di, T).
Defined.
```

Note that the order of the vertexes and arrows returned by `parseImage`

determines the order of the parameters required by the parser. The vertexes (i.e. `ps`

) are ordered from top to bottom, breaking ties from left-to-right (red). The morphisms (i.e. `es`

) are ordered in the order of their source vertex, breaking ties in a circle from left to top (blue). This is depicted for the product example in the following diagram.

Following is the actual implementation of the parser `parse`

which is of type `parseType`

.

```
Definition parse (img:list string) : parseType img.
unfold parseType.
```

The `parse`

implementation mirrors that of `parseType`

. This means that Coq can actually infer quite a bit of code (remember the three lines of code that keep `om`

and `os`

up to date? that’s `_`

now!). Note the `fun o:object => _`

in the parser which corresponds to the `forall o:object, _`

in the type.

```
destruct (parseImage img) as [ps es].
match goal with
|- _ ?os ?om ?ps => revert ps; generalize om; generalize os
end.
refine (fix rec os om ps {struct ps} :=
match ps with
| [] => _
| x::ps' => fun o:object => rec _ _ _
end)
```

Because the parser actually has to keep track of the passed morphisms, the recursion over the arrows `es`

is more complex than `parseType`

’s recursion over `es`

.

```
clear rec ps.
revert es.
refine ((fix rec (ms:list {s:index os & {d:index os &
lookup s → lookup d}}) es {struct es} :=
match es with
| [] => _
| (s,d)::es' => _
end) []); revgoals.
```

The recursion maintains `ms`

. `ms`

is the list of the morphisms collected as parameters along with the `index`

of each morphisms source `s`

and destination `d`

. The following code keeps `ms`

up to date. As in `parseType`

, morphisms are silently ignored if their source or destination is not an object.

```
{
destruct (om s) as [si|]; [|exact (rec ms es')].
destruct (om d) as [di|]; [|exact (rec ms es')].
refine (fun m => rec ([si & [di & m]]::ms) es').
}
```

Lastly, the parser uses the `os`

and `ms`

list to build a Diagram. The set of vertexes in the Diagram is simply the set of `index`

es into the `os`

list. The set of arrows is the set of `index`

es into the list of morphisms `ms`

, filtered with `section`

to contain only morphisms starting at `s`

and ending in `d`

. The mapping of vertexes to objects, and arrows to morphisms is then simply the `lookup`

of an index.

```
clear rec es om.
refine {|
Vertex := index os;
vertexObject := lookup;
Arrow s d := index (section ms s d);
arrowMorphism x y := lookup
|}.
Defined.
```

The parser translated the ASCII art representation of a diagram into a `Diagram`

. The next step is to denote (assign meaning) to this diagram, i.e. what does it mean for a diagram to commute? Wolfram has the answer:

[A diagram commutes iff all] compositions starting from the same [object] A and ending with the same [object] B give the same result.

This can be translated into Coq as follows:

```
Definition commutes `(Diagram) :=
forall s d (P Q:Path s d), composePath P = composePath Q.
```

In English: a diagram commutes iff for any two paths `P`

and `Q`

with the same source `s`

and destination `d`

, the compositions of the morphisms along these paths are equal. Note that the `Diagram`

is passed around implicitly using the type class mechanism.

A path between two vertexes is the reflexive transitive closure of arrows between two vertexes:

```
Inductive Path : Vertex -> Vertex -> Type :=
| refl {a} : Path a a
| step {a b c} : Arrow a b -> Path b c -> Path a c.
```

The composition of the morphisms along a path is defined as the identity `id`

for the trivial reflexive path, and the composition `∘`

of two morphisms for each arrow of the path.

```
Fixpoint composePath {s d} (p:Path s d) : vertexObject s → vertexObject d :=
match p in Path s d return vertexObject s → vertexObject d with
| refl => id
| step a p' => arrowMorphism a ∘ composePath p'
end.
```

The `commutes`

function effectively denotes a `Diagram`

in Coq’s logic. Unfortunately, this denotation is hard to work with directly because it requires a proof for all vertexes and paths. This where the `denote`

function comes in. In the case of a finite, non-cyclic diagram the `denote`

function enumerates all sources, all destinations, and all paths (`P`

, `Q`

) between them. This enumeration leads to a (possibly large) conjunction where each conjunct is of the form `composePath P = composePath Q`

. This post does not go into detail of how `denote`

is implemented.

Following is a list of exercises and potential future work that can be done to improve this formalization of commutative diagrams. If you solve any of these exercises, please send me a pull request.

0) Use commutative diagrams to define more constructions (like `Product`

).

1) Extend the parser to support diagonal lines. The parser should be able handle the following.

```
[" ";
" c ";
" o ";
" /|\ ";
" / | \ ";
" / | \ ";
" v v v ";
" o<--o---o ";
" a b ";
" "]
```

2) Proof the bi-implication between `denote`

and `commutes`

as outlined in the *Denotation* section.

3) Identify a specification for the parser, and prove the parser correct according to this specification. This likely means formalizing declaratively what the vertexes and arrows are in a diagram.

4) Improve performance.

5) Support uniqueness arrows. E.g. the `factor`

morphism has to be unique in a `Product`

. This is currently enforced, unsatisfactorily, using the `pairUnique`

field. Unique morphisms are usually represented with a dotted line, for the `Product`

the parser should thus support:

```
[" ";
" p c q ";
" +--------o--------+ ";
" | : | ";
" | :factr | ";
" | : | ";
" v v v ";
" o<-------o------->o ";
" a bundle b ";
" "]
```

6) Parse objects and morphisms from the labels on a diagram, instead of having them passed as arguments to the `denote`

function. Some Ltac magic might be in order for this exercise.

7) Use pictorial definitions to improve proof automation. Somehow pictorial definitions make it easier for humans to do reasoning; can one use pictorial definitions to make it easier for computers to do reasoning? Diagram chasing might be an example of this.

8) Support image (e.g. SVG or PNG) based commutative diagrams. It might be challenging to efficiently parse such large amounts of data in Coq. This might require an extension to proof general that renders the bits of an image in Coq as an actual image in emacs.