A place for "evil" category theory lemmas

Stream: mathlib4

[Robert Maxton]

Generally speaking, we consider lemmas that involve directly equating objects of categories to be 'evil' in Mathlib, in part for aesthetic reasons (since we try to stick to isomorphisms in pen and paper math as well), and in part for practical reasons (since objects are often essentially types, and type equality is painful to work with in Lean.) Fair enough, most of the time -- but sometimes we're working directly with Cat itself, or some other strict bicategory, where in order to use categorical machinery from the rest of the library we need to talk about the strict equality of functors (which implicitly involves strict equality of objects, as well as introducing DTT issues of their own.) As a guy working on categorical graph theory in Mathlib (via Quiv), I trip over this a lot.

As the resulting lemmas are often quite painful to derive, and it is not always obvious how far their assumptions can be relaxed, I think it would be useful to have a place for 'evil' lemmas -- a StrictCat locale or something along those lines, to be used where lax notions from higher category theory are inappropriate or insufficient.

[Junyan Xu]

Also when working with FundamentalGroupoid you do want to refer to the points (= objects) rather than "identifying" all points in the same path component. A formalization of the Van Kampen theorem is that FundamentalGroupoid.fundamentalGroupoidFunctor is a co-sheaf, for which we do want to consider colimits in Cat/Grpd.

[Joël Riou]

I would like to mention that in my formalization of the homotopy theory of Kan complexes, it was also helpful to consider the fundamental groupoid as a pseudofunctor: https://github.com/joelriou/topcat-model-category/blob/master/TopCatModelCategory/SSet/Pseudofunctor.lean#L48-L57

[Robin Carlier]

I guess the issue pointed by @Junyan Xu comes from the fact that we do not have the (locally groupoidal) bicategory of groupoids, nor a notion of (co)limits in (2,1)-categories. Considering it as a pseudofunctor to Cat (which in facts lands in its subcategory of groupoid) is probably the way to go.

[Robert Maxton]

So, since we seem to have some support for this, do we have a place to put them? My current thought is to just have something like Mathlib.CategoryTheory.Cat.Lemmas and a namespaceStrictCat, with as many of the 'evil' lemmas as we can fit into a low-import file and all relevant simps/instances scoped to StrictCat; does anyone have a preference for a better name?

[Eric Wieser]

I don't have much context here, but if you're tempted to write these lemmas for a particular category, should you instead be writing some lemma that provides equality back in the language of types (eg apply .hom)?

[Robert Maxton]

The "particular category" in this case is Cat itself, primarily. The lemmas would be about equality of categorical objects -- objects themselves and functors, and isomorphisms rather than equivalences of categories. And it's precisely the 'evil'-ness of the lemmas that makes it challenging to write general-case lemmas; in short, we see a lot of rewrite failed, motive is not type correct here

[Robin Carlier]

I’m running into an other case where we might want to perform some rather evil constructions: the Duskin nerve of a bicategory is a construction that allows one to embed the theory of bi-categories into the category of simplicial sets, it has some nice properties, for instance, when the bi-category we give it is locally groupoidal, then the Duskin nerve is in fact a quasicategory (in fact, the Duskin nerve is always an (∞, 2)-category, but we don’t have that yet).

The Duskin nerve requires evil objects such as the 1-category of bicategories (with morphisms strictly unitary lax functors, i.e functors that are unitary "on the nose") and the embedding from the strict 1-category of categories in that category.

I’m not working on the Duskin nerve right now, but I might need it soon. What would be the "canonical place" for this construction?

[Robin Carlier]

(in this particular case, maybe we can do without the 1-category of bicategories w/ strictly unitary lax functor, but we can’t do without said functors and some equalities about them I think)