Zulip Chat Archive

Stream: maths

Topic: 2-categories


view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:19):

How do we want to set up 2-categories in mathlib?
Some time ago I wrote down:

import category_theory.category
import category_theory.concrete_category

universes w v u

namespace category_theory

class two_category (obj : Type u) extends has_hom.{v} obj :=
[hom_cats : Π (X Y : obj), category.{w} (X  Y)]

def CAT := bundled category.{v u}

instance : has_coe_to_sort CAT :=
{ S := Type u,
  coe := bundled.α }

instance str (C : CAT.{v u}) : category.{v u} C := C.str

instance : two_category CAT :=
{ hom := λ X Y, X  Y }

end category_theory

(which should probably be named two_category_struct) - I think the other obvious option gives a bunch of eq_to_homs when you start writing the details, but I could be wrong

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:19):

cc: @Adam Topaz and @Scott Morrison

view this post on Zulip Johan Commelin (Mar 25 2021 at 18:20):

Aren't 2-categories super-duper scary to work with in a formal theorem prover?

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:20):

We also have the option of going straight for enriched categories and deducing 2-categories from there, but I think that's even harder

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:21):

Johan Commelin said:

Aren't 2-categories super-duper scary to work with in a formal theorem prover?

Possibly :) But there are a few places across mathlib category theory where they'd be nice to have, so I think it's worth experimenting if we can get a usable API

view this post on Zulip Johan Commelin (Mar 25 2021 at 18:23):

Related but unrelated: I think we can also define quasicategories (= (,1)(\infty,1)-cats) now that we have simplicial sets.

view this post on Zulip Johan Commelin (Mar 25 2021 at 18:23):

But here it might be good to take a step back, and take very close look at what Riehl--Verity are doing

view this post on Zulip Johan Commelin (Mar 25 2021 at 18:24):

For 2-cats you have multiple versions, right. Strict or not

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:27):

Yeah - I was thinking of going for strict 2-categories because the cases I can think of where it's nice to use this language in mathlib involve strict 2-(co)limits

view this post on Zulip Adam Topaz (Mar 25 2021 at 18:40):

As far as I am concerned, the place where this would be immediately helpful is in the case where we have a pseudofunctor taking values in the 2-category of categories, and we apply some (co)limits on the target of such a pseudofunctor

view this post on Zulip Adam Topaz (Mar 25 2021 at 18:40):

I don't know if this is a silly suggestion, but we could "define" 2-categories as categories enriched over Cat?

view this post on Zulip Adam Topaz (Mar 25 2021 at 18:41):

Does mathlib have the monoidal structure on Cat?

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:45):

Adam Topaz said:

I don't know if this is a silly suggestion, but we could "define" 2-categories as categories enriched over Cat?

I think this is a good suggestion but from what I hear from Scott, enriched categories are hard to get right anyway, so I suspected it would be easier to go straight for this special case

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 18:49):

Bhavik Mehta said:

Yeah - I was thinking of going for strict 2-categories because the cases I can think of where it's nice to use this language in mathlib involve strict 2-(co)limits

I think I was completely wrong here actually - the cases in mathlib are weak 2-(co)limits, for instance this discussion which is about a 2-initial object?

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 20:40):

Alright, I had a go at weak 2-categories (ie bicategories) together with pseudofunctors and it went surprisingly well? https://github.com/leanprover-community/mathlib/blob/two-cat/src/category_theory/category/2-category.lean

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 20:41):

I think the next main test of this would be to figure out the right simp lemmas and define the composition of pseudofunctors, with the hope that tidy takes care of some of the annoying details

view this post on Zulip Scott Morrison (Mar 25 2021 at 21:12):

It may take a few days before I get to this discussion properly, sorry. I don't think strict 2-categories are going to be helpful, because no examples exist. Even the ones we think exist in normal maths will actually be infected with eq.rec when formalised, and will work better as weak 2-categories.

view this post on Zulip Scott Morrison (Mar 25 2021 at 21:14):

Just from a philosophical point of view, I'm fairly prejudiced against thinking of 2-categories as categories enriched in categories, but don't have the time to articulate why right now.

view this post on Zulip Scott Morrison (Mar 25 2021 at 21:14):

I had been thinking much more in terms of copying and pasting the definition of monoidal category and adding in 0-objects. :-)

view this post on Zulip Scott Morrison (Mar 25 2021 at 21:14):

In particular, I'm tempted to parametrise by 0-morphisms and 1-morphisms, and bundle 2-morphisms.

view this post on Zulip Adam Topaz (Mar 25 2021 at 21:32):

Regardless of what happens, can we introduce this notation ASAP?

notation η `  ` f:50 := two_category_struct.right_whisker f η
notation η `  ` f:50 := two_category_struct.left_whisker η f

notation _` := two_category_struct.left_unitor
notation `ρ_` := two_category_struct.right_unitor
notation `α_` := two_category_struct.associator

view this post on Zulip Adam Topaz (Mar 25 2021 at 21:32):

(for functors I mean)

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 21:34):

Scott Morrison said:

It may take a few days before I get to this discussion properly, sorry. I don't think strict 2-categories are going to be helpful, because no examples exist. Even the ones we think exist in normal maths will actually be infected with eq.rec when formalised, and will work better as weak 2-categories.

Yup, I completely agree with this, I think weak 2-categories are absolutely the way to go

view this post on Zulip Scott Morrison (Mar 25 2021 at 21:47):

I'd be perfectly happy adding that notation immediately (presumebly without even mentioning two_category_struct, until we decide what that is) for functors.

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 22:00):

Likewise, though I wonder if we can come up with nicer symbols for the whiskerings

view this post on Zulip Bhavik Mehta (Mar 25 2021 at 22:01):

I just realised I didn't even use the correct triangle opposites :|


Last updated: May 14 2021 at 18:28 UTC