Zulip Chat Archive

Stream: maths

Topic: monoidal categories


view this post on Zulip Scott Morrison (Nov 07 2018 at 03:24):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:25):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:25):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:25):

so many axioms...

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:25):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:25):

Ah -- maybe I should address that first.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:25):

You might have said:

view this post on Zulip 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 ...

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:27):

hopefully you prove the equivalence though?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:29):

what's the issue?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:30):

Can you make it a curried functor instead?

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:31):

cat being a CCC and all

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:33):

that's sad...

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:34):

What about an infix functor application operator?

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:34):

like <$> for functor

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:36):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:37):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:38):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:38):

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

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip 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... :-)

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:40):

right, sorry to derail your story. carry on

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:41):

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

view this post on Zulip 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 ...

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:42):

wait, what's a monoidal functor now

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:42):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:45):

What's the alternative?

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:45):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:46):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:46):

F.to_functor.map f?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:46):

Yes.

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:47):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:47):

?

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:47):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:48):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:48):

new

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:48):

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

view this post on Zulip Mario Carneiro (Nov 07 2018 at 03:49):

Is the to_functor in the pp.all term?

view this post on Zulip Scott Morrison (Nov 07 2018 at 03:54):

Yes

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 07 2018 at 04:00):

hm, this is parser magic we can't duplicate

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:07):

I think there still is.

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:07):

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

view this post on Zulip Reid Barton (Nov 07 2018 at 04:07):

T.app (X, Y)?

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:07):

You mean T.obj (X, Y)?

view this post on Zulip Reid Barton (Nov 07 2018 at 04:08):

er, T.obj

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 07 2018 at 04:08):

hm

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:09):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:09):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 07 2018 at 04:11):

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

view this post on Zulip Reid Barton (Nov 07 2018 at 04:11):

I imagine you thought of that already

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:11):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:11):

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

view this post on Zulip Scott Morrison (Nov 07 2018 at 04:11):

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

view this post on Zulip 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....

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 07 2018 at 04:14):

Also: no bicategories?? :upside_down:

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 07 2018 at 08:29):

But I agree it's desirable.

view this post on Zulip Scott Morrison (Nov 07 2018 at 08:29):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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_)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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