Define a structure made of objects $A, B, C, \dots$ and morphisms $f, g, \dots$. Each morphism has a collection of domain objects and codomain objects. For simplicity we consider the domains and codomains as unordered sets. We require that
- For each $A$ there exists an $f : A \to A$.
- For every $f:B_1, B_2, \dots \to C, D_1, D_2,\dots$ and $g: C, F_1, F_2, \dots \to H_1, H_2,\dots$, there exists a morphism $g \circ f : B_1, B_2, F_1, F_2 \dots \to D_1, D_2, H_1, H_2\dots$.
- For composable $f, g, h$, $(f\circ g) \circ h = f \circ (g \circ h)$.
Note that this is richer than sequent logics, because it is sort of proof relevant; the same sequent have different proofs. If we impose that for each $f,g:\Gamma \to\Delta$ we have $f=g$, then we recover the usual sequent logic, without any connectives. (Of course, this makes axiom three trivial.)
We can then define connectives with universal properties, just as we define products, coproducts and equalizers etc.
My question is: is there any existing literature on such a structure? What's the name for it? Where can I read more about it?
Best Answer
It sounds like you want the notion of a polycategory.