Multicategory

A multicategory is a generalization of the notion of Category where the morphisms can have multiple inputs. This allows one to work with things like Multilinear Maps without passing to representing objects like Tensor Products.

Explicitly, a multicategory $\mathcal{C}$ consists of

• A type of objects $\mathcal{C}_{0}:\mathsf{U}{}$
• A type of multimorphisms $\mathcal{C}_{1}(-,-):\mathcal{C}_{0}^{*}\to\mathcal{C}_{0}\to\mathsf{U}{}$
• A unary identity multimorphism $mathrm{id}{ifx..lse\par i}:\mathcal{C}_{1}([X],X)$
• Composition of multimorphisms: $f\circ[g_{1},\ldots,g_{n}]$

Already, we are starting to see the cracks: the combinatorics of composition is downright awful. Things only get worse when you try to state the laws; most sources resort to just writing dots.

We can do a bit better by working with length-indexed vectors, which induces a sort of grading. However, this is essentially the same as working with functions $[n]\to\mathcal{C}_{0}$. If we zoom out further, we can notice that we are essentially using the natural numbers as a Tarski Universe that is closed under Sigma Types; EG, a Regular Cardinal.

However, this does not work either, as the laws quickly become unbearable. Another option is to try and use an ordered Partition of $[n]$; EG, a map in the Demisimplex Category. This would let us partition the objects in the output type: this lets us remember how composites were formed, and also has the potential to make type inference a bit better?

This does lead to the following cool type of a block vector:

data BlockVec {ℓ} (A : Type ℓ) : Nat → Nat → Type ℓ where
[] : BlockVec A 0 0
_∷_ : ∀ {m n} → A → BlockVec A (suc m) n → BlockVec A (suc (suc m)) n
_❚_ : ∀ {m n} → A → BlockVec A m n → BlockVec A (suc m) (suc n)

If we Displayed over the Demisimplex Category, then we get something that starts to resemble the starting pieces of a Polycategory: the type of objects $\mathcal{E}_{[n]}$ provides the right type to start talking about finite sequences of objects, and the morphisms $f:[n]\twoheadrightarrow[k]$ describe precisely how to "chunk up" the inputs.

However, polycategories only let us compose along a single object at once, ala

This doesn't quite capture what we need to do; we are trying to pass from a heterogenous notion of square to something homogenous like

The Demisimplex Category almost does the right thing here, and ensures that each cell picks out a collection of objects that will be its inputs. Surjectivity could be a bit problematic though: we don't have a way to have nullary inputs. I think we need the full-blown (augmented) Simplex Category

When drawn without proarrows this becomes more clear:

EG: the notion of substitution we are looking for is Simultaneous Substitution, not Single Substitution. Moreover, our identities should look more like a Mix Rule.

Next, we need to impose some sort of typing discipline to avoid composing complete trash. Actually, does this just do the right thing? The typing discipline imposed by displayed objects like $\mathcal{E}_{[n]}$ ought to do it?

A multi-morphism would then be a displayed morphism $\mathcal{E}_{!}(\overline{X},Y)$, where $!:[n]\to[1]$. However, I don't think we can compose correctly yet; consider a pair of maps $g,h$ over $[1]\to[1]$; we will need to be able to "formally tensor" these together to get a map $g\otimes h:[2]\to[2]$, which we can then compose with a map $f:[2]\to[1]$.

If you put this into fibred terms, I think what you get is a Strict Monoidal Functor from $\mathcal{E}$ to the Augmented Simplex Category, or alternatively as a Displayed Monoidal Category over $(\Delta_{a},\oplus,0)$

There is still one lingering problem: we need a way to go from a formal horizontal composite like

to a single map

In terms of displayed categories, we need to go from a map over $f:[4]\to[3]$ to one over some $[3]\to[1]$, where the value $[3]$ depends on the map $f$. This feels like it should be some sort of pullback?