Typing context as a monad for multicategories

62 Views Asked by At

In some ways simple type theory matches up nicer with multicategories than with categories.

A hom

$$ f \colon o_1 ; \ldots o_n \rightarrow o'$$

Matches up nicely with a well typed term

$$ x_1 \colon t_1 , \ldots x_n \colon t_n \vdash v \colon t' $$

However, there are some technical difficulties especially with constructively mechanizing things.

A nameless style such as with de Bruijn indices works okay but it'd be nice to have an explicitly named style. Using the definition of generalized multicategories one wants some sort of key value map monad.

You would probably also expect a functor from "named multicategories" to list multicategories.

My intuition says to me you would end up with ordered lists of variable object pairs and list of variables indexed identity (variable reference) and compose (multisubstitution) operations.

$$\text{id}_{[x]} \colon \text{Hom}(x \mapsto A; A)$$

$$\circ_{x, y} \colon \text{Hom}(y_j \mapsto B_j ; C) \rightarrow [y_j \mapsto \text{Hom}(x_i \mapsto A_{ij} ; B_{ij})] \rightarrow \text{Hom}(x_{ij} \mapsto A_{ij} ; C)$$

I think you would need to base things around graded multicategories though and I don't know about those.

Also I think you might need to ban duplicate variables/variable shadowing or use quotients which is icky.

In general this is getting into category theory stuff I don't know or getting ugly.

I wonder if there's been any work on "named multicategories" and if there are nicer ways of doing things.

I've been thinking about this stuff for a while but specifically I have a renewed interest because I suspect it can help illuminate hereditary substitution for me.