Algebraic tricategories in Lean

Stream: maths

[Fernando Chu]

Just wondering out loud, how could one formalize tricategories a la Gurski in Lean in a way that is manageable and potentially useful? The Bicategory approach is extending CategoryStruct and then deciding on a simp normal form for 2-cells; are there other alternatives?

[Robin Carlier]

My gut feeling is that yes, for tricategories the "same approach" as bicategories (a CategoryStruct on top of which a Bicategory instance is added on the quiver homs) would work. However, as 2-cells would be objects of a category (as 1-cells in a bicategory), trying to rely on simp will run into the usual problems (rewriting in 2-cells will lead to bad typing whenever there are 3-cells lying around).

As for making it "potentially useful", as for categories and bicategories, we can’t define tricategorical concepts in bicategories as the corresponding concept in the tricategory of bicategories, this would not have enough universe polymorphism (think e.g how equivalences of categories are defined in mathlib: it is not defined as an equivalence in the bicategory of categories). IMO what would be more useful (at least, for mathlib as it is now) would be to define the tricategorical concepts that we are missing on bicategories (bi-equivalences, bi-adjunctions, monoidal/braided/sylleptic/symmetric monoidal bicategories...) first before trying to have a formal theory and definition of tricategories.

[Robin Carlier]

(note that for bi-equivalences in bicategories, I think @Judah Towery is already working on them)

[Fernando Chu]

Robin Carlier said:

...this would not have enough universe polymorphism

I had not realized about this problem. That is quite unfortunate. Thanks for the insights!