2-categories

Stream: maths

[Bhavik Mehta]

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]

cc: @Adam Topaz and @Scott Morrison

[Johan Commelin]

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

[Bhavik Mehta]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Bhavik Mehta]

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]

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]

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

[Adam Topaz]

Does mathlib have the monoidal structure on Cat?

[Bhavik Mehta]

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]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Adam Topaz]

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]

(for functors I mean)

[Bhavik Mehta]

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]

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]

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

[Bhavik Mehta]

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