Zulip Chat Archive

Stream: maths

Topic: bicategories


view this post on Zulip Reid Barton (Oct 09 2018 at 22:00):

@Scott Morrison have you by any chance done or thought about formalizing bicategories?

view this post on Zulip Reid Barton (Oct 09 2018 at 22:01):

I know you have monoidal categories somewhere which is in approximately the same direction

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:10):

Yes, I'd like to, but have done nothing.

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:11):

I've been meaning to rewrite the work on monoidal categories for a while now, as it's an excellent playground for my student Keeley Hoek's "rewrite_search" algorithms.

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:12):

I think the lesson I eventually learnt there is that defining a monoidal category as a category C equipped with a functor C x C to C is actually a bad idea, mostly for syntactic reasons! I think it will work much better if you have have operations tensor_obj and tensor_hom, and laws for them, etc, then have a theorem that packages these as a functor when needed.

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:13):

The basic problem is just that if you think of tensor as a functor out of C x C, then its argument is a pair, and you'd really really prefer the curried version of these for parsing, pattern matching, etc. Dealing with the pairs causes lots of pain.

view this post on Zulip Reid Barton (Oct 09 2018 at 22:14):

Hmm, makes sense...

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:14):

It is a bit sad though that this is a significant consideration.

view this post on Zulip Reid Barton (Oct 09 2018 at 22:15):

https://ncatlab.org/nlab/show/bicategory#detailedDefn

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:16):

The point is not that one would want to write out the definition in such elementary terms (although apparently I just did anyway) but rather that one can.

view this post on Zulip Scott Morrison (Oct 09 2018 at 22:17):

In a different direction, I would love to do (have someone do?) quasi-strict categories (according to Vicary), as a foundation for hooking up Lean and Globular.

view this post on Zulip Reid Barton (Oct 09 2018 at 22:23):

Right, I think we talked about this briefly in Orsay

view this post on Zulip Reid Barton (Oct 09 2018 at 23:40):

I suppose a possible alternative to C x C -> C is a curried functor C => (C => C), though I don't have a clear sense of the issues here yet

view this post on Zulip Scott Morrison (Oct 09 2018 at 23:56):

I suspect, although haven't actually checked, that this is just as bad. Because F X is handled via a coercion, rather than merely notation, I suspect we could never get T X Y to work for a curried functor.

view this post on Zulip Mario Carneiro (Oct 10 2018 at 00:40):

I think the curried functor should work fine

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:28):

Why not use the dependently-typed definition of bicategory a la an enriched category?

view this post on Zulip David Michael Roberts (Oct 10 2018 at 05:31):

As in, something like obj1:Obj obj2:Obj |- Hom_obj1_obj2 : Cat and then apply whatever solution makes the monoidal case work, modulo adapting to multiple objects?

view this post on Zulip Reid Barton (Oct 10 2018 at 09:59):

I think the issue is that we don't have a nice solution for monoidal categories, that doesn't require a structure with ~30 fields


Last updated: May 14 2021 at 18:28 UTC