## Stream: maths

### Topic: 2-categories

#### 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

#### Bhavik Mehta (Mar 25 2021 at 18:19):

cc: @Adam Topaz and @Scott Morrison

#### Johan Commelin (Mar 25 2021 at 18:20):

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

#### 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

#### 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

#### Johan Commelin (Mar 25 2021 at 18:23):

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

#### 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

#### Johan Commelin (Mar 25 2021 at 18:24):

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

#### 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

#### 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

#### 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?

#### Adam Topaz (Mar 25 2021 at 18:41):

Does mathlib have the monoidal structure on Cat?

#### Bhavik Mehta (Mar 25 2021 at 18:45):

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

#### 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?

#### 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

#### 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

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

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

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

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

#### 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


#### Adam Topaz (Mar 25 2021 at 21:32):

(for functors I mean)

#### 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

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

#### Bhavik Mehta (Mar 25 2021 at 22:00):

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

#### 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