Machine Checkable Pictorial Mathematics for Category Theory

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 parsed and then denoted. 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.

Parsing

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 indexes into the os list. The set of arrows is the set of indexes 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.

Denotation

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.

Exercises

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.