Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Internalizing "structural" operations in multicategories

Shea Levy (Oct 18 2020 at 15:44):

A multicategory might admit of various "structural" operations on arrows, e.g. adding in the "exchange" rule makes it a symmetric multicategory, or we might have some function $weaken : ([\Gamma_1 ; \Gamma_2] \to X) \to ([\Gamma_1 ; Y ; \Gamma_2] \to X)$. Is there a way to "internalize" these functions in the metatheory into some categorical entity that captures the appropriate equivalences? I almost want to say they're 2-cells, but we don't have matching domains (but what even are 2-cells in multicategories?).

Reid Barton (Oct 18 2020 at 15:50):

I'm not sure what you mean by words like "metatheory" or "internalize". How does your question relate to just saying something along the lines of, for example,
Definition. A multicategory with weakening is a multicategory equipped with operations $w_i : \mathrm{Hom}((X_1, \ldots, X_{i-1}, X_{i+1}, \ldots, X_n), Y) \to \mathrm{Hom}((X_1, \ldots, X_n), Y)$ such that [...]

Shea Levy (Oct 18 2020 at 15:54):

Right, so what I'd like to understand is whether there's some (possibly higher) multi-categorical construct corresponding to that operation. In the same way that (from my rough understanding) you can treat the equivalence of $(f \circ g) \circ h$ and $f \circ (g \circ h)$ as a 2-cell (2-isomorphism?) between those arrows.

Reid Barton (Oct 18 2020 at 16:00):

Well in a general multicategory there might not be any such operation (e.g. $\mathrm{Hom}((X_1, X_3), Y)$ might be nonempty while $\mathrm{Hom}((X_1, X_2, X_3), Y)$ might be empty). I'm also pretty sure there is no way to characterize the weakening operations in terms of just the multicategory structure, in case that's what you mean.

Reid Barton (Oct 18 2020 at 16:01):

So if you want to have a multicategory with weakening operations, it seems best to simply define what that is.

Shea Levy (Oct 18 2020 at 16:02):

Oh, yeah, it's definitely extra structure. I think I'm not framing my question well :smile:

Reid Barton (Oct 18 2020 at 16:03):

In my extremely biased opinion, it's a lot easier to understand this subject starting from the semantics side, since things like multicategories are just ordinary mathematical objects with ordinary definitions, and then try to see how to interpret some construction in logic as giving an "internal language" of these objects.

Reid Barton (Oct 18 2020 at 16:13):

I still don't understand the question but one thing I think I can say is that 2-cells should correspond to something like reduction rules: something that, when you forget it, corresponds to equality between terms/morphisms.

Reid Barton (Oct 18 2020 at 16:15):

But weakening is something that produces a new judgment from an old judgment; it is not like an equation

Reid Barton (Oct 18 2020 at 16:17):

And what does "equivalences" in the original question refer to?

Shea Levy (Oct 18 2020 at 16:24):

Reid Barton said:

And what does "equivalences" in the original question refer to?

E.g. if I have some $f : \Gamma \to A$ and $g : \Gamma_1 ; \Gamma_2 \to B$, then I want $weaken_A(g) \circ f \equiv weaken_{\Gamma}(g)$, where weaken_l puts l between $\Gamma_1$ and $\Gamma_2$.

Reid Barton (Oct 18 2020 at 16:29):

That condition would be part of the omitted [...] in the definition of a "multicategory with weakening"

Reid Barton (Oct 18 2020 at 16:31):

If you want 2-cells, then you can consider a multicategory enriched in Cat, or a "weak 2-multicategory" in which composition is only associative up to a 2-cell; and then impose these equations on weakening up to a 2-cell.

Shea Levy (Oct 22 2020 at 00:29):

Reid Barton said:

I still don't understand the question but one thing I think I can say is that 2-cells should correspond to something like reduction rules: something that, when you forget it, corresponds to equality between terms/morphisms.

I assume the reduction rule follows the arrow? So if e.g. I'm working in a multicategory of expressing typing judgments (so $\Gamma \vdash e : T$ is a multiarrow from $\Gamma$ to $T$), a 2-cell $e \Rightarrow e'$ means we can reduce $e$ to $e'$?

Nathanael Arkor (Oct 22 2020 at 09:14):

Yes.

Nathanael Arkor (Oct 22 2020 at 09:16):

A reference for this sort of thing is Seely's Modelling computations: A 2-categorical framework.

John Baez (Oct 22 2020 at 16:30):

I like that paper.

Philip Saville (Oct 22 2020 at 17:07):

if you want something a bit more fleshed out, there's also Hilken's 2-lambda calculus, which has strict products but lax exponentials, and Hirschowitz's 2-dimensional type theory for cartesian closed 2-categories. Tooting my own horn a bit, there's a fully pseudo version for cartesian closed bicategories in this paper and my thesis.

In each case you can read off the type theory as the internal language (in the sense of Lambek) of a suitable kind of 2-dimensional cartesian multicategory (aka multi-sorted clone) -- you need the cartesian-ness because your substitution isn't linear. You could then use the fact operations like weakening arise from substitution / variable renamings. So, for example, weakening becomes the functor $\mathcal{C}(\Gamma; B) \to \mathcal{C}(\Gamma, A; B)$ induced by the renaming of variables $\Gamma \hookrightarrow \Gamma, x : A$, ie it sends $t$ to $t[x_i \mapsto x_i]$ when $\Gamma = (x_i : A_i)_{i=1, \dots, n}$. (In the strict setting this substitution is invisible as it's the identity; in the strict setting it's made explicit.)