bicategories

Stream: maths

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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.

[Reid Barton]

Hmm, makes sense...

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Reid Barton]

Right, I think we talked about this briefly in Orsay

[Reid Barton]

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

[Scott Morrison]

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.

[Mario Carneiro]

I think the curried functor should work fine

[David Michael Roberts]

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

[David Michael Roberts]

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?

[Reid Barton]

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