## Stream: maths

### Topic: monoidal categories

#### Scott Morrison (Nov 07 2018 at 03:24):

@Michael Jendrusch has recently started work on monoidal categories again. (Yay!)

#### Scott Morrison (Nov 07 2018 at 03:24):

I've been looking at what he's written, and I want to resume my rant about how terrible coercions are, as a result.

#### Scott Morrison (Nov 07 2018 at 03:25):

He's defined monoidal categories, and I think these are uncontroversial.

#### Scott Morrison (Nov 07 2018 at 03:25):

https://github.com/mjendrusch/monoidal-categories-reboot/blob/master/src/monoidal_categories_reboot/monoidal_category.lean

#### Mario Carneiro (Nov 07 2018 at 03:25):

so many axioms...

#### Scott Morrison (Nov 07 2018 at 03:25):

However when he gets to monoidal functors the horrors caused by coercions start to creep out...

#### Scott Morrison (Nov 07 2018 at 03:25):

Ah -- maybe I should address that first.

#### Scott Morrison (Nov 07 2018 at 03:25):

You might have said:

#### Scott Morrison (Nov 07 2018 at 03:26):

surely a monoidal category should be described as a category C equipped with a functor C \times C \func C, satisfying ...

#### Scott Morrison (Nov 07 2018 at 03:26):

(this will certainly reduce the number of axioms, at least slightly, because various things are wrapped up in functoriality)

#### Scott Morrison (Nov 07 2018 at 03:27):

However... implementation details forced on us by Lean make this a bad idea (as I discovered when I did monoidal categories previously)

#### Mario Carneiro (Nov 07 2018 at 03:27):

hopefully you prove the equivalence though?

#### Scott Morrison (Nov 07 2018 at 03:28):

Yes, it's easy (and Michael started doing it) to show afterwards that these things assemble into functors, and natural transformations, and so on.

#### Scott Morrison (Nov 07 2018 at 03:29):

The problem with making tensor product a functor first of all is that it becomes really painful to implement notation X \otimes Y and f \otimes' g.

#### Mario Carneiro (Nov 07 2018 at 03:29):

what's the issue?

#### Scott Morrison (Nov 07 2018 at 03:30):

You end up having to define as auxiliary lemmas curried versions of the functor of objects, but even then the elaborator often really struggles.

#### Scott Morrison (Nov 07 2018 at 03:30):

(Sorry, it's been a year or so since I last fought with this issue... give me a moment.)

#### Mario Carneiro (Nov 07 2018 at 03:30):

Can you make it a curried functor instead?

#### Mario Carneiro (Nov 07 2018 at 03:31):

cat being a CCC and all

#### Scott Morrison (Nov 07 2018 at 03:32):

You could make it a curried functor, but I don't think it would help. If T was your tensor product functor, you still couldn't write T X Y and have the elaborator successfully introduce both coercions.

#### Scott Morrison (Nov 07 2018 at 03:33):

Neither T (X, Y), if T : C \times C \func C, or T X Y, if T : C \func (C \func C) will elaborate reliably. (In fact, I think they won't ever elaborate.)

#### Scott Morrison (Nov 07 2018 at 03:34):

You can see examples of this all over my (no-longer-compiling) earlier attempt at monoidal categories.

#### Mario Carneiro (Nov 07 2018 at 03:34):

What about an infix functor application operator?

#### Mario Carneiro (Nov 07 2018 at 03:34):

like <\$> for functor

#### Scott Morrison (Nov 07 2018 at 03:35):

@[ematch] definition interchange (f : U ⟶ V) (g : V ⟶ W) (h : X ⟶ Y) (k : Y ⟶ Z) :
(f ≫ g) ⊗ (h ≫ k) = (f ⊗ h) ≫ (g ⊗ k) :=
@Functor.functoriality (C × C) _ C _ (tensor C) ⟨U, X⟩ ⟨V, Y⟩ ⟨W, Z⟩ ⟨f, h⟩ ⟨g, k⟩


should really just be proved by (tensor C).map_comp (f, h) (g,k), but instead we need to use @, and specify way too many implicit arguments.

#### Scott Morrison (Nov 07 2018 at 03:35):

Yes --- so this is what I had long ago.

#### Scott Morrison (Nov 07 2018 at 03:35):

I had +> for obj, and &> for map, although I really don't care what the symbols are.

#### Scott Morrison (Nov 07 2018 at 03:35):

I would _love_ to move back to this model, which would let us get rid of lots of coercions.

#### Mario Carneiro (Nov 07 2018 at 03:36):

I've heard this story before, and I don't disagree with you

#### Mario Carneiro (Nov 07 2018 at 03:36):

I really want coercions to work, and in principle they could, but lean's coercion model is not extensible enough

#### Mario Carneiro (Nov 07 2018 at 03:37):

it should be a parser extension rather than being tied to coe in core

#### Scott Morrison (Nov 07 2018 at 03:37):

If we were in a situation where modifying the coercion mechanism was on the table, I would absolutely support struggling on with coercions, essentially to gain data about what we really want.

#### Scott Morrison (Nov 07 2018 at 03:38):

But I'm not sure whether :four_leaf_clover: gives us this prospect, or not.

#### Mario Carneiro (Nov 07 2018 at 03:38):

I think it might, at least it should not be far from the areas under development

#### Scott Morrison (Nov 07 2018 at 03:39):

If my fighting with coercions is not significantly likely to result in better coercions later, I just want the suffering to go away. :-)

#### Mario Carneiro (Nov 07 2018 at 03:39):

the fact that simp doesn't work under coercions is something we might be able to fix in lean 3

#### Scott Morrison (Nov 07 2018 at 03:39):

I haven't even started explaining the difficulties coercions are causing in the design of monoidal_functor... :-)

#### Mario Carneiro (Nov 07 2018 at 03:40):

right, sorry to derail your story. carry on

#### Scott Morrison (Nov 07 2018 at 03:41):

Essentially: if we want monoidal_functor to extend functor, we need new coercions so we can still write F X, when F is a monoidal functor. Now however none of the lemmas involving F X will apply when F is a monoidal functor, because the coercion won't be the right one.

#### Scott Morrison (Nov 07 2018 at 03:41):

So we'll have to reproduce all the lemmas...

#### Scott Morrison (Nov 07 2018 at 03:41):

And we'll have to do this again for braided_functor, and then again for additive_functor, and then again for ...

#### Mario Carneiro (Nov 07 2018 at 03:42):

wait, what's a monoidal functor now

#### Scott Morrison (Nov 07 2018 at 03:42):

monoidal functor doesn't exist yet, beyond Michael's first cut at https://github.com/mjendrusch/monoidal-categories-reboot/blob/master/src/monoidal_categories_reboot/monoidal_functor.lean

#### Scott Morrison (Nov 07 2018 at 03:42):

and you can see at the bottom of that file the problems waiting for us as soon as we define composition of monoidal functors.

#### Mario Carneiro (Nov 07 2018 at 03:45):

What's the alternative?

#### Scott Morrison (Nov 07 2018 at 03:45):

well, if all the coercions were gone, our problems would mostly disappear.

#### Mario Carneiro (Nov 07 2018 at 03:46):

if the coercions were gone, it wouldn't typecheck. Are you writing explicit functions now?

#### Scott Morrison (Nov 07 2018 at 03:46):

Instead of having functor.map', the structure field, which doesn't use the coercion, and functor.map, the same, as a lemma written using the coercion, we'd just have the structure field.

#### Mario Carneiro (Nov 07 2018 at 03:46):

F.to_functor.map f?

#### Scott Morrison (Nov 07 2018 at 03:46):

So we wouldn't have to define a new version of map for monoidal functors, so all the lemmas about functor.map would still apply

Yes.

#### Scott Morrison (Nov 07 2018 at 03:47):

But you wouldn't have to write the .to_functor explicitly.

?

#### Mario Carneiro (Nov 07 2018 at 03:47):

what's the magic sauce you are using in place of coercions

#### Scott Morrison (Nov 07 2018 at 03:47):

Am I wrong? I thought that's how the extension mechanism works -- you can refer directly to the fields of the parent structure.

#### Mario Carneiro (Nov 07 2018 at 03:48):

It depends on whether you are using the old structures or new

new

#### Scott Morrison (Nov 07 2018 at 03:48):

but this certainly works, I just double checked :-)

#### Mario Carneiro (Nov 07 2018 at 03:49):

Is the to_functor in the pp.all term?

Yes

#### Scott Morrison (Nov 07 2018 at 03:55):

The to_functor is in fact there even without pp.all. You just don't need to write it.

#### Scott Morrison (Nov 07 2018 at 03:58):

As far as I can see the parser is doing this. There's no monoidal_functor.obj field at all, but you can nevertheless write F.obj X when F is a monoidal functor, and when you pp the resulting term it shows as F.to_functor.obj X.

#### Scott Morrison (Nov 07 2018 at 03:59):

The essential problem is that because of coercions, we have all this duplication: functor has both map' and map, and map_comp' and map_comp, etc.

#### Scott Morrison (Nov 07 2018 at 03:59):

Every time we extend functor (or anything similar), we will need to reproduce all this duplication again.

#### Mario Carneiro (Nov 07 2018 at 04:00):

hm, this is parser magic we can't duplicate

#### Reid Barton (Nov 07 2018 at 04:05):

Sorry, so to go back to the start, if we forgot about coercions entirely, is there still an issue with defining the tensor product to be a functor from C x C to C?

#### Scott Morrison (Nov 07 2018 at 04:07):

I think there still is.

#### Scott Morrison (Nov 07 2018 at 04:07):

The basic question is how to implement X \otimes Y.

#### Reid Barton (Nov 07 2018 at 04:07):

T.app (X, Y)?

#### Scott Morrison (Nov 07 2018 at 04:07):

You mean T.obj (X, Y)?

#### Reid Barton (Nov 07 2018 at 04:08):

er, T.obj

#### Reid Barton (Nov 07 2018 at 04:08):

I can see that writing down the functors which the associator is supposed to be a natural isomorphism between is going to be ugly

#### Scott Morrison (Nov 07 2018 at 04:08):

The problem there is that for reasons I don't totally understand, even having the pair construction in there gums up the elaborator.

hm

#### Scott Morrison (Nov 07 2018 at 04:09):

My old monoidal-categories repository didn't use any coercions.

#### Scott Morrison (Nov 07 2018 at 04:09):

(unfortunately I don't have a compiling version of it anymore...)

#### Scott Morrison (Nov 07 2018 at 04:10):

But I found myself having to use

-- Convenience methods which take two arguments, rather than a pair. (This seems to often help the elaborator avoid getting stuck on prod.mk.)
definition tensorObjects (X Y : C) : C := (tensor C) +> (X, Y)

infixr  ⊗ :80 := tensorObjects -- type as \otimes


#### Reid Barton (Nov 07 2018 at 04:11):

Another question: how about using isos for the associator/unitors instead of four fields each?

#### Reid Barton (Nov 07 2018 at 04:11):

I imagine you thought of that already

#### Scott Morrison (Nov 07 2018 at 04:11):

but then there's an extra layer of folding and unfolding tensorObjects

#### Scott Morrison (Nov 07 2018 at 04:11):

Actually, the question of using isos is a good one.

#### Scott Morrison (Nov 07 2018 at 04:11):

and I'm not sure that I did think about it carefully.

#### Scott Morrison (Nov 07 2018 at 04:12):

I suspect I wrote my initial monoidal categories library before I'd actually ironed out a usable implementation of isomorphisms....

#### Scott Morrison (Nov 07 2018 at 04:13):

@Michael Jendrusch, next time you're around, how about we try this idea out: using isomorphisms as the fields for associators and unitors, rather than the four separate fields?

#### Reid Barton (Nov 07 2018 at 04:14):

Also: no bicategories?? :upside_down:

#### Reid Barton (Nov 07 2018 at 04:16):

I kind of want to formalize (bi)limits in bicategories, since I feel the literature on them is kind of spotty.

#### Reid Barton (Nov 07 2018 at 05:00):

but, I might want to do it less if it is going to look like https://ncatlab.org/nlab/show/bicategory#detailedDefn. How would I even know that I got the definition correct?

#### Scott Morrison (Nov 07 2018 at 06:49):

@Reid Barton, I've been considering trying to talk @Michael Jendrusch into doing bicategories. :-) I would like them, too.

#### Scott Morrison (Nov 07 2018 at 06:49):

But I think it makes sense to sort out the issues we're having here first, and if they are all solvable it might be a cheap rewrite to generalise...

#### Scott Morrison (Nov 07 2018 at 06:50):

@Michael Jendrusch, I just added two new commits that package associators, unitors, and tensorators as isos. I think it is nicer.

#### Johan Commelin (Nov 07 2018 at 07:52):

Yesterday one of my colleagues walked in to have a quick look at the workshop. He is working on derivators and such stuff. He explained how we might want to use multicategories for this. But I'm not sure how much work it would be to set up all the basics. He said it would help us get rid of the pentagon axiom in some sense. But I'm not sure if it means that the carpet won't fit in another corner... (is this an English idiom?).
@Scott Morrison Are you familiar with this multicategorical approach?

#### Michael Jendrusch (Nov 07 2018 at 07:59):

@Michael Jendrusch, I just added two new commits that package associators, unitors, and tensorators as isos. I think it is nicer.

It's merged! I would kind of like to have bicategories, too, but this looks painful (https://ncatlab.org/nlab/show/bicategory#detailedDefn).

#### Michael Jendrusch (Nov 07 2018 at 08:02):

On another note, making µ an iso in the definition of a monoidal functor makes that a _strict_ monoidal functor according to nLab, where I would also want _lax_ monoidal functors. Maybe we can define a _lax_ monoidal functor and then extend it to a _strict_ monoidal functor?

#### Scott Morrison (Nov 07 2018 at 08:28):

Ah, it's a little subtle. If you want lax monoidal functors, then I want oplax ones (this is a serious request, actually: <https://arxiv.org/abs/1701.00567>. So if we want to do it via inheritance we'll be dealing with a diamond.

#### Scott Morrison (Nov 07 2018 at 08:29):

But I agree it's desirable.

#### Scott Morrison (Nov 07 2018 at 08:29):

(But you certainly can't use the name monoidal functor if you mean a lax one. :-)

#### Scott Morrison (Nov 07 2018 at 08:34):

Regarding multicategories --- I'm not opposed to someone also introducing these, but I'm pretty confident it's all blind men describing an elephant. Now if we want to talk about disklike categories <https://arxiv.org/pdf/1108.5386.pdf>, then we'd be cooking with gas.

#### Reid Barton (Nov 07 2018 at 15:04):

Actually, maybe bicategories won't be that bad at all. Shouldn't it just be a matter of asking for Pi a b. category (C a b), then adding a bunch of type indices everywhere in the definition of monoidal category?

#### Scott Morrison (Nov 07 2018 at 20:18):

Yes, that sounds right. It's a pity you can't mix variables syntax with structures; you could almost leave out all those extra type indices!

#### Michael Jendrusch (Nov 08 2018 at 10:01):

Ah, it's a little subtle. If you want lax monoidal functors, then I want oplax ones (this is a serious request, actually: <https://arxiv.org/abs/1701.00567>. So if we want to do it via inheritance we'll be dealing with a diamond.

It seems that a lot of things in category theory result in diamonds when using inheritance (e.g. with strict monoidal categories). Is there another standard way of treating this without inheritance, and what are the actual problems one gets with diamonds in Lean?

#### Michael Jendrusch (Nov 08 2018 at 12:58):

would it make sense to try and work around inheritance (and thus diamonds) by not having a classes lax_monoidal_functor, oplax_monoidal_functor both inheriting from functor (and getting a diamond from defining monoidal_functor as inheriting from both), instead opting to have functor_is_lax_monoidal, functor_is_oplax_monoidal together with an instance functor_is_monoidal for every functor which is both lax and oplax, like this?

class functor_is_lax_monoidal
(C : Type u) [monoidal_category.{u v} C]
(D : Type u') [monoidal_category.{u' v'} D]
(F : C ⥤ D) :=
-- definition of lax monoidal functor here.

class functor_is_oplax_monoidal
(C : Type u) [monoidal_category.{u v} C]
(D : Type u') [monoidal_category.{u' v'} D]
(F : C ⥤ D) :=
-- definition of oplax monoidal functor here.

class functor_is_monoidal
(C : Type u) [monoidal_category.{u v} C]
(D : Type u') [monoidal_category.{u' v'} D]
(F : C ⥤ D) :=
-- definition of monoidal functor here.

instance lax_and_oplax
(C : Type u) [monoidal_category.{u v} C]
(D : Type u') [monoidal_category.{u' v'} D]
(F : C ⥤ D) [functor_is_lax_monoidal C D F] [functor_is_oplax_monoidal C D F] :
functor_is_monoidal C D F := by obviously


#### Scott Morrison (Nov 08 2018 at 22:05):

This is an interesting approach; I wonder if we should re-explore making functor a typeclass right from the beginning.

#### Scott Morrison (Nov 08 2018 at 22:05):

My concern is that functor_is_monoidal carries data (the tensorator), so it's a little scary making it a typeclass.

#### Scott Morrison (Nov 08 2018 at 22:06):

However in my experience it's extremely rare that one considers two different tensorators for the same functor. (Although not _never_)

#### Scott Morrison (Nov 08 2018 at 22:06):

But if we're going to carry this data in a typeclass, why aren't we carrying the data of functor.map in a typeclass?

#### Scott Morrison (Nov 08 2018 at 22:07):

I have tried this, ..., but it was a long time ago and I don't really remember why I didn't like it then.

#### Scott Morrison (Nov 10 2018 at 21:32):

@Michael Jendrusch, I started adding the monoidal structure on any category with products, that should subsume your initial example of Type u. It's not there yet, but I think it's a fun test of our limits library to make sure this is doable with no more effort than in the Type u case.

Last updated: May 12 2021 at 08:14 UTC