# Zulip Chat Archive

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

s 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):

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

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