Yes, I too see the proof as equations between words. The question is what does the diagram add, and what form should it take in order to add whatever it does. For you it may add nothing, but diagrams are so pervasive that there must be some reason people resort to them instead of simply writing equations. When I first took CT in 1964 from Max Kelly, exactly this point bothered me greatly: I couldn't see the point of writing compact equations as huge diagrams. To some extent I still don't, yet somehow I've come to accept them as a language for equations. Vaughan Peter Selinger wrote:

Vaughan Pratt wrote:

...

Peter Selinger wrote:

...

Hi Vaughan, [private reply]:

is there any other proof of Lambek's lemma? This is the only one I have ever known. I think it's a nice proof-theoretic question what the second square contributes to the proof. I was arguing against it but PTJ was arguing for it, very reasonably.

Viewed as a purely equational argument the second square is x=x which contributes nothing. As a diagrammatic proof however PTJ claims it clarifies the argument and I agree with him. Mathematically the point is trivial, proof-theoretically it is of some interest.

But isn't it the same proof, whether you write it with 5, 7, or 0 arrows?

...

...

I think I can prove the same theorem with a much smaller diagram, consisting of 0 arrows. Simply replace the diagram by the sentences "Let f be the unique T-homomorphism from the initial T-algebra a to the T-algebra Ta. By definition of T-homomorphism, this satisfies fa=TaTf." How do you get from fa=TaTf to af = 1, fa = 1? You could leave out even more and simply say Lambek's lemma is self-evident.

In the same way you did, of course. By functoriality, fa = T(af). By composition, afa = a T(af). Therefore af is a T-algebra homomorphism from a to itself, and by uniqueness, af = 1. Therefore fa = T(af) = T(a) = 1.

I am simply stating the obvious fact that you can write the whole proof without writing any diagram, yet without leaving out any step. Does this count as a proof "with 0 arrows"? Forgive me for the frivolous question, but I guess I am completely missing your point!

-- Peter