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?

bothsides, the corresponding idea is amulticategoryand is fairly widely used. However, traditionally comma on therightof a sequent meansdisjunction; if you clarify that in your question, I or someone might look up some references for categorical work using that idea. $\endgroup$1more comment