and the sequents dinatural transformations.
That LL can be construed as a logic of both proofs (Girard's
application) and mathematics (the application I'm promoting) gives a
hint of just how tightly modern proof theory has managed to wrap itself
around mathematics, giving both essentially the same form (or at least
dual forms).
Vaughan Pratt