# 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?