monoidal categories

Stream: maths

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

so many axioms...

[Scott Morrison]

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

[Scott Morrison]

Ah -- maybe I should address that first.

[Scott Morrison]

You might have said:

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

hopefully you prove the equivalence though?

[Scott Morrison]

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]

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]

what's the issue?

[Scott Morrison]

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]

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

[Mario Carneiro]

Can you make it a curried functor instead?

[Mario Carneiro]

cat being a CCC and all

[Scott Morrison]

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]

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.)

[Mario Carneiro]

that's sad...

[Scott Morrison]

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

[Mario Carneiro]

What about an infix functor application operator?

[Mario Carneiro]

like <$> for functor

[Scott Morrison]

@[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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

right, sorry to derail your story. carry on

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

wait, what's a monoidal functor now

[Mario Carneiro]

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

[Scott Morrison]

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]

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]

What's the alternative?

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

F.to_functor.map f?

[Scott Morrison]

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

[Scott Morrison]

Yes.

[Scott Morrison]

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

[Mario Carneiro]

?

[Mario Carneiro]

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

[Scott Morrison]

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]

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

[Scott Morrison]

new

[Scott Morrison]

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

[Mario Carneiro]

Is the to_functor in the pp.all term?

[Scott Morrison]

Yes

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Mario Carneiro]

hm, this is parser magic we can't duplicate

[Reid Barton]

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]

I think there still is.

[Scott Morrison]

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

[Reid Barton]

T.app (X, Y)?

[Scott Morrison]

You mean T.obj (X, Y)?

[Reid Barton]

er, T.obj

[Reid Barton]

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]

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

[Reid Barton]

hm

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Reid Barton]

I imagine you thought of that already

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

@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]

Also: no bicategories?? :upside_down:

[Reid Barton]

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

[Reid Barton]

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]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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]

@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]

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]

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]

But I agree it's desirable.

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

@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.