Formal proof of Coherence Theorem for Monoidal Category

Coherence property for a certain category means that we know that diagrams of a certain class commute.

First theorem of this class was the proved by S. Mac Lane for monoidal categories (see [Mac Lane 71, pp.161-165]) His proof was based on normalisation of object expressions, but involved many other ingredients and was far from elementary.

Peter Dybier has shown in [2] that the proof could be get almost for free from the analisys of normalisation of free monoid. Ilya Beylin has formalised this proof in Martin-Löf type theory using proof assistant ALF.

The ALF development:

Version 5

The current version, using two categories M and N, as in [2]. (Directory, Zip, Description). Version 5a is also contained here: just rename NMC-5a.alf to NMC.alf.

Version 5aa

One category, as in [1]. Generated from version 5 some time ago. (Zip)

Version 4

which used natural numbers for the interpretation. Unfinished (the mult case is missing). (Zip, Description)

The HOL development

The same proof has been formalized in HOL by Sten Agerholm at IFAD. His experience shows that use of tactics can greatly faciliate the task of chasing categorical diagrams. It can be said that proofs written in HOL are as laconic as the correspondent diagrams, while the ALF proofs are entire proof terms where all rewriting is left explicit. On the other hand lack of dependent types make some definitions (for instance, composition of arrows) quite unnatural.  

The HOL proof as a  tar-file . It is mirrored from Sten's ftp directory.

See [1] for comparison of the two formalisations.

And what is ALF?

• B.Nordström. The Alf Proof Editor. (dvi)
• T.Altenkirch, V.Gaspes, B.Nordström, and B.von Sydow. User's Guide to ALF (html), (ps.Z)).
• B.Nordström, K. Petersson, and J.M. Smith. Martin-Löf's Type Theory. A chapter in Handbook of Logic in Computer Science, written in 1994, forthcoming. (ps.gz).
• B.Nordström, T.Coquand, J.Smith, and B.von Sydow Type theory and Programming. (ps.gz) The EATCS bulletin, February 1994.
• Download Window ALF (for Sun Solaris 2 under X-Windows).
• Other experiments in ALF

Related Work on Formalisation of Category Theory

• Sten Agerholm. Experiments in Formalizing Basic Category Theory in Higher Order Logic and Set Theory. /HOL/
• Peter Dybier, Veronica Gaspes. Implementing a category of sets in ALF
• Gerard Huet, Amokrane Saibi. Consructive Category Theory. /Coq/
  See also Saibi's thesis and book draft (both in French) on Formalisisng Category theory in Calculus of Constructions.
• Takahisa Mohri. On Formalization of Category Theory. (abstract) (ps file)
• Michael Fleming and Ryan Gunther: Programming of finite categories. (User's guide) (C sources)
  
• MIZAR articles

References:

1. Sten Agerholm, Ilya Beylin, and Peter Dybier.
   A Comparison of HOL and ALF: Formalizations of a Categorical Coherence Theorem,
   in proceedings of TPHOL'96, LNCS 1125, pp 17-32.
2. Peter Dybjer, Ilya Beylin.
   Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids
   Proccedings of TYPES'95, LNCS 1158, pp 47-61.
3. Sten Agerholm. Formalizing a Proof of Coherence for Monoidal Categories. Manuscript, January 1996.
4. Ilya Beylin. An ALF Proof of MacLane's Coherence Theorem. Comments to the Implementation . Draft, Version 4, Version 5.