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: deprecated: our papers

Topic: Bifibrations of polycategories and classical MLL

Nicolas Blanco (May 25 2023 at 07:58):

My PhD thesis is now available on the arXiv: Bifibrations of polycategories and classical multiplicative linear logic

Nicolas Blanco (May 25 2023 at 08:00):

This wouldn't have been possible without the support of my advisors @Noam Zeilberger
and @Paul Blain Levy , and the careful reading and suggestions of my examiners @Richard Garner and Uday Reddy and chair Martin Escardo. A lot of thanks to them and all the amazing people I've met during these years.

Nicolas Blanco (May 25 2023 at 08:53):

I chose the title of the thesis during the first year of my PhD and kept it. It actually covers more than bifibrations of polycategories but almost doesn't delve into the logic side. The main two ingredients are representability (in the sense of representable multicategories) and fibrationality.
The idea of representability is that certain structured categories can be equivalently given by generalising the shape of the morphisms of a category. Examples that I looked at in my thesis are multicategories where the morphisms have many inputs, polycategories where they also have many outputs and virtual double categories that can be understood as multicategories colored by a category. There some structures on categories become universal properties: think of the tensor products of vector spaces that is characterised by linearising multilinear maps. The structured categories in question are monoidal (biclosed) categories for multicategories, (lax) linearly distributive/$\ast$-autonomous categories for polycategories and double categories for virtual double categories. Taking this point of view can have numerous advantages: it is more natural for some models (e.g. vector spaces where multilinear maps are easier to define than the tensor product) and it allows one to not have to bother about coherence issues for example.
More important to us, representability is a special case of fibrationality. Opfibrations of multicategories were studied by Claudio Hermida. A pushforward in this context can be understood as a tensor product in the total multicategory parametrised by a (multi)morphism in the base. In particular when the base is representable (has tensors) and the multimorphism chosen is the one expressing universality of the tensor, the pushforward is a tensor in the total multicategory. Similarly pullbacks in a multicategory correspond to parametrised internal homs. So one can use can use fibrationality to lift representability in the base to the total multicategory. In the thesis, I have proved that this extend is also true for polycategories and virtual double categories.
In particular, I have used this on two examples. I have considered how to lift the $\ast$-autonomous structure of the category of finite dimensional vector spaces and linear maps to the category of finite dimensional Banach spaces and non-expansive/contractive maps by looking at the fibrational property of their polycategorical counterpart. Interestingly, while the former is degenerated as a model of linear logic since the conjunction and disjunction are both interpreted by the tensor product, the latter isn't: they correspond to different norms. In fact these norms are the smallest and biggest ones that can be put on the tensor products, which can be explained fibrationally.
The second example was about considering variations of the Grothendieck construction, e.g. the Bénabou-Grothendieck construction that build a functor from a lax normal pseudofunctor into the bicategory of categories and distributors/profunctors. I wanted to show that these constructions are given by pulling back a "universal" functor along the pseudofunctor like it the usual case. However, one cannot easily do so in general: since we consider (non strict) bicategories and lax functors, the (categorical not fibrational) pullback cannot be defined pairwise. More precisely the composition in the pullback cannot be defined pairwise since the functors are lax. To get around this, one can go to virtual double categories, which turns the lax functors into strict ones. So the pullback can be defined. The "universal" functors mentioned above give (op)fibrations of virtual double categories. And since these are closed under pullback, we get fibrational properties for the pullback. This let us lift the composition (of horizontal maps) of the domain of the functor we are pulling along to the pullback. Some more fibrational properties of the universal functors we are pulling ensure that the pullback is a category/bicategory when the base is.

So that was a long teaser... Anyhow, I hope you will enjoy this thesis as much as I have working on the topic for the past few years!

Matteo Capucci (he/him) (May 25 2023 at 10:43):

Wow, it looks really interesting Nicolas! Congrats!!

John Baez (May 25 2023 at 16:05):

Sounds cool! I know 3 of those people. So polycategories are good for multiplicative linear logic?

Nicolas Blanco (May 25 2023 at 17:44):

Thank you both.
@John Baez Yes, they are perfect for it. It is Lambek that first saw a connection between multicategories and intuitionistic logic (more precisely Gentzen's sequent calculus) in the 70s. Then Szabo, Lambek's student, introduced polycategories to study classical logic in the 80s. In the 90s, Cockett, Seely and others showed that they were in fact better suited for multiplicative linear logic.
I would argue that polycategories more naturally model MLL than $\ast$-autonomous categories. The same is true for multicategories vs monoidal closed categories for Intuitionistic MLL. Why is that? The short answer is: it is closer to the syntax. The shape of the polymaps/multimaps correspond to the shape of the sequents. The connectives can then by derived as universal properties. The usual approach using structured categories assumes the existence of (the interpretation of) the connectives and use them for the interpretation of the sequents.
I think an example might be better than a long explanation. Let's just consider the sequent calculus for IMLL. A sequent looks like that

$$A_1, \dots, A_n \vdash B$$

The multiplicative conjunction $\otimes$ is defined via a left rule saying that from a sequent

$$\Gamma_1, A, B, \Gamma_2 \vdash B$$

one can derive a sequent

$$\Gamma_1, A \otimes B, \Gamma_2 \vdash B$$

and a right rule saying that from sequents

$$\Gamma_1 \vdash A$$

$$\Gamma_2 \vdash B$$

one can derive a sequent

$$\Gamma_1, \Gamma_2 \vdash A \otimes B$$

Now we want to use vector spaces as models of this logic. The monoidal categorical way of doing so is by saying: to each formula $A$ I assign a vector space $\llbracket A\rrbracket$. And to each sequent

$$A_1, \dots, A_n \vdash B$$

a linear map

$$\llbracket A_1\rrbracket \otimes \dots \otimes \llbracket A_n \rrbracket \to \llbracket B \rrbracket$$

Then the right rule is tensoring the linear maps and the left rule is just trivial!

One the other hand, the multicategorical point of view is the following: we interpret a formula by a vector space and a sequent by a multilinear map

$$\llbracket A_1 \rrbracket, \dots, \llbracket A_n \rrbracket \vdash \llbracket B \rrbracket$$

Now the right rule is given by postcomposing the two multilinear maps by $\llbracket A \rrbracket, \llbracket B \rrbracket \to \llbracket A \rrbracket \otimes \rrbracket B \rrbracket$, and the left rule takes a multilinear map

$$\llbracket A \rrbracket, \llbracket B \rrbracket \to\llbracket B \rrbracket$$

and linearise it

$$\llbracket A \rrbracket \otimes \llbracket B \rrbracket \to\llbracket B \rrbracket$$

(I got rid of the $\Gamma_i$ for simplicity but it is the same)
So this interpretation has way more content.
Even more: they are so-called $\beta$-equivalence and $\eta$-equivalence that govern the interaction of the connective rules with the cut rule. In the multicategorical interpretation, these correspond to the fact that a multilinear map factors through its linearisation and that the linearisation is unique! So taking the tensor product is the only way to get a model of the multiplicative conjunction that is closed under $\beta\eta$-equivalence.

The same story is true for polycategories: all the connectives of MLL are given by objects with universal properties in a polycategory akin to the one for tensor products. In fact something stronger is true. One can define a unifying notion of universal object in a polycategory: it is define by a polymap having it in his domain or codomain such that any polymap (that has the right typing) factors through the polymap with composition happening along the universal object. Then all the connectives are universal, but also they generate all universal objects.
So there is a strong connection between polycategories and MLL. This has been extended to full LL by @Mike Shulman via LNL-polycategories.

Jean-Baptiste Vienney (May 25 2023 at 18:20):

Woh thanks @Nicolas Blanco , so multicategories and polycategories kinda answer the same concern I had and that you explained about how to interpret differently the commas and the tensors! There are now clearly research projects to understand if what @Mike Shulman did can be extended to the graded and differential extensions of LL ie. if we can define graded, differential or graded differential LNL-polycategories.

Nicolas Blanco (May 25 2023 at 18:27):

Jean-Baptiste Vienney said:

Woh thanks Nicolas Blanco , so multicategories and polycategories kinda answer the same concern I had and that you explained about how to interpret differently the commas and the tensors! There are now clearly research projects to understand if what Mike Shulman did can be extended to the graded and differential extensions of LL.

Yes! At some point I wanted to see if it can be used for DiLL, but I never found the time to do so. It is worth mentioning that @Christine Tasson and Martin Hyland have been working on a concept of LNL-multicategory with the goal to use it to study models of intuitionistic DiLL. Their paper predates Mike's one, but it doesn't have the full description of a LNL-multicategory in it yet. It is conjectured in Mike's paper that these are special cases of its LNL-polycategories. This gives hope that LNL-polycategories could be used to have some insights into models of DiLL.

Jean-Baptiste Vienney (May 25 2023 at 18:36):

Ok nice! So, I think nobody tried for graded linear logic ie. linear logic with an exponential $(!_{r})_{r \in R}$ graded by some (ordered) semiring.

Jean-Baptiste Vienney (May 25 2023 at 18:38):

The idea is that a proof $!_{r}A \rightarrow B$ is a proof that produces something of type $B$ by using at most (or exactly if you chose a trivial order) r units of $A$.

Jean-Baptiste Vienney (May 25 2023 at 18:41):

But that's weird because $\mathcal{C}[!_{r}A,B]$ can't be a cartesian closed category but would be a kind of graded category ie. something with hom-sets $\mathcal{D}_{r}[A,B]$ of morphisms from $A$ to $B$ of degree $r$.

Jean-Baptiste Vienney (May 25 2023 at 18:44):

An obvious choice is $R=\mathbb{N}$ and $!_{n}A = A^{\otimes n}$

Jean-Baptiste Vienney (May 25 2023 at 18:45):

The second less obvious is to symmetrize $A^{\otimes n}$ and takes $!_{n}A$ equal to the equalizer of $n!$ permutations $A^{\otimes n} \rightarrow A^{\otimes n}$

Jean-Baptiste Vienney (May 25 2023 at 18:46):

So, like this you could add a notion of symmetry to your polycategories maybe

Jean-Baptiste Vienney (May 25 2023 at 18:46):

ie. looks at the symmetric polymaps

Jean-Baptiste Vienney (May 25 2023 at 18:47):

just some ideas

Jean-Baptiste Vienney (May 25 2023 at 18:55):

In fact symmetric polycategories/multicategories already exist.

Nicolas Blanco (May 25 2023 at 19:09):

I don't think anyone looked at a "graded" multicategories yet.

Nicolas Blanco (May 25 2023 at 19:13):

Beware, I think you are confusing two notions of symmetric there. A multicategory/polycategory is symmetric in the same sense that a monoidal category is. This means that there is a symmetry isomorphism $s \colon A \otimes B \to B \otimes A$. For the interpretation of $!_n$ it is the object that is symmetric in the sense that $a \otimes b = b \otimes a$. Or more categorically, that the symmetric power object is a (co?)equaliser of the identity map and the symmetry map.

Nicolas Blanco (May 25 2023 at 19:14):

I don't know enough about graded linear logic to make an educated guess about what would a graded multicategory/polycategory would look like though.

Jean-Baptiste Vienney (May 25 2023 at 19:51):

Yeah I don't know either although I know what is graded linear logic, I'm just combining words together and see if it makes sense but that's not the best way to do research.

Matteo Capucci (he/him) (May 26 2023 at 07:55):

One might try to define T-multicategories for graded T to find the answer

Nicolas Blanco (May 27 2023 at 09:54):

That's a good idea! Christine Tasson and Martin Hyland attempt to define a LNL-multicategory is similar. In fact their paper is about defining a LNL-monad that would encode the inputs of the multicategory. Mike Shulman's work is more "ad hoc". LNL-polycategories are defined directly. What is a generalised polycategories is still an open question :)