# Coend calculus as a deductive system

I've always had in the back of my head the feeling that co/end calculus, regarded as a set of rules allowing to mechanically prove nontrivial statements as initial and terminal points of a chain of deductions, can indeed be regarded as a deductive system.

I must admit I have no grip on the issue, but as far as I can justify this analogy with the only deductive system I've seen in my ife (Gentzen natural deduction), I'd say that elimination and introduction rules resemble very much elimination and introduction of integrals in formulas like $$Nat(F,G) \cong \int_C \hom(FC,GC)$$ or $$\text{Lan}_GF(A) = \int^X \hom(GX,A)\times FX$$ These equalities allow one to deduce the validity of more complex statements, like for example the fact that profunctor composition is associative, or that pointwise right extensions in the bicategory of profunctors are indeed exhibited by a certain end.

How far am I from being right? I there a way to turn this intuition into something more formal? Is there a way to actually prove that {co/end calculus}, by which I mean the set of elementary theorems regarding natural transformations, the Yoneda lemma,etc. as suitable co/ends, all taken as "manipulation rules", indeed forms a deductive system?

This kind of question has been taken very seriously in the past, and I am surprised to discover it only now. You should definitely check Sec. 3 in:

Cáccamo and Winskel, A Higher-Order Calculus for Categories. Boulton R.J., Jackson P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg.

Is it any meaningful to wonder what a Haskell implementation of this paper would look like?

• Yes it would be meaningful, given the authors of the article, I wouldn't be surprised if they, or someone close to them, already did it. Feb 1 '20 at 9:53