Bicategory structure on `Grpd`

Stream: mathlib4

[joseph hua]

I would like to also have a bicategory structure on Grpd, by defining the common generalization of this with the bicategory structure on Cat

def ofCoeSortCategory (B : Type u₁) [CoeSort B (Type u)] [∀ C : B, Category.{v, u} C] :
    Bicategory.{max v u, max v u, u₁} B where
  Hom C D := C ⥤ D
  id C := 𝟭 C
  comp F G := F ⋙ G
  homCategory := fun _ _ => Functor.category
  whiskerLeft {_} {_} {_} F _ _ η := Functor.whiskerLeft F η
  whiskerRight {_} {_} {_} _ _ η H := Functor.whiskerRight η H
  associator {_} {_} {_} _ := Functor.associator
  leftUnitor {_} _ := Functor.leftUnitor
  rightUnitor {_} _ := Functor.rightUnitor
  pentagon := fun {_} {_} {_} {_} {_} => Functor.pentagon
  triangle {_} {_} {_} := Functor.triangle

Then we could also generalize to_app to cover any such bicategory, and also have a Grothendieck construction for any such category (my original motivation)

[Joël Riou]

Arguably, the category of morphisms between two functors between groupoids could be natural isomorphisms (rather than natural transformations).
I am not doing meta-programmation, but I do not see obstacles for generalizing to_app for groupoids.
For the Grothendieck construction, the easier is probably to apply the existing Grothendieck construction to the composition of a pseudofunctor and the "forget" pseudofunctor from Grpd to Cat.

[joseph hua]

Joël Riou said:

For the Grothendieck construction, the easier is probably to apply the existing Grothendieck construction to the composition of a pseudofunctor and the "forget" pseudofunctor from Grpd to Cat.

This is what I am currently working with. I don't like it very much because I have to either have Grpd.forgetToCat bloating the context, or create a new API to hide all the Grpd.forgetToCat, in which attributes like @[simps!] do not work very nicely. (essentially this means either way one has to maintain two copies of the Grothendieck API, rather than just one)

Another thing this would work nicely with is taking the bicategory to be LocallyDiscrete Set, and getting the category of elements as a special case of the Grothendieck construction

[Fernando Chu]

Shouldn't the .forgetToCat bloat disappear after a use of simp?

[joseph hua]

Yes that's right. But my experience is that the simp lemma Grpd.forgetToCat was causing performance issues because it was slowing down checking definitional equalities. I might be wrong about this, but it was certainly a less user-friendly experience

[joseph hua]

Joël Riou said:

Arguably, the category of morphisms between two functors between groupoids could be natural isomorphisms (rather than natural transformations).

that should be a different definition. I wouldn't make this def an instance

[Fernando Chu]

My two cents: I think this should use the existing Grothendieck construction and forgetToCat. While I understand that having one specific construction for each case helps with definitional equalities and therefore typechecking, this would require more glue later on. E.g. if we want to show that the Grothendieck construction has a right adjoint, we would have to make this construction n times for each specific case, in contrast to doing it once and then checking that the right adjoint restricts appropriately.

[Fernando Chu]

I think that the performance issues of .forgetToCat can be mitigated by adding more simp lemmas. So I see the problem as a tradeoff of optimizing code now v.s. writing glue/duplicate code later, and I think that the first approach is the best in the long term. Of course there is a problem of distribution, the glue/duplication can be done at a later time by whoever needs it, while optimizing is hard and would fall mostly on you. I don't know how to solve this, other than offer my help for this specific case :)

[Calle Sönne]

For visibility I opened this PR a while back defining the bicategory structure on Grpd: #30920. However, you both seem to be thinking about this harder than I was, so I am happy to close it if you settle on a better approach.

[joseph hua]

Maybe we should as a first step refactor the bicategory structure on Cat and #30920 through my suggestion, and fixing to_app so that it works in both cases. @Calle Sönne I haven't worked on any tactics before so definitely would like your help on the latter

[Joël Riou]

Which refactor?

[joseph hua]

joseph hua said:

I would like to also have a bicategory structure on Grpd, by defining the common generalization of this with the bicategory structure on Cat

def ofCoeSortCategory (B : Type u₁) [CoeSort B (Type u)] [∀ C : B, Category.{v, u} C] :
    Bicategory.{max v u, max v u, u₁} B where
  Hom C D := C ⥤ D
  id C := 𝟭 C
  comp F G := F ⋙ G
  homCategory := fun _ _ => Functor.category
  whiskerLeft {_} {_} {_} F _ _ η := Functor.whiskerLeft F η
  whiskerRight {_} {_} {_} _ _ η H := Functor.whiskerRight η H
  associator {_} {_} {_} _ := Functor.associator
  leftUnitor {_} _ := Functor.leftUnitor
  rightUnitor {_} _ := Functor.rightUnitor
  pentagon := fun {_} {_} {_} {_} {_} => Functor.pentagon
  triangle {_} {_} {_} := Functor.triangle

Then we could also generalize to_app to cover any such bicategory, and also have a Grothendieck construction for any such category (my original motivation)

@Joël Riou this definition generalizes both the bicategory structure on Cat and the bicategory structure on Grpd in #30920.

[Joël Riou]

This sounds reasonable!

[Calle Sönne]

Okay if I understand correctly, essentially what's going on here is that given a type of objects you are defining a full sub-bicategory of Cat. In #30925 I define "induced bicategories" which is essentially this in general, with the important difference is that in your case the "inclusion map" is actually a coercion (and injective). Do you think that most of the API you wanted to avoid duplicating could be stated in terms of the inclusion pseudofunctor of an induced bicategory as in my PR?

[Calle Sönne]

And if you think that this approach is strictly superior to one using induced bicategories, could it be possible to generalize your construction further to also deal with other similar full sub-bicategories?

[Calle Sönne]

Is the main advantage to your approach in comparison to using Grpd.forgetToCat that the pseudofunctor gets replaced with a coercion? Could some notation help deal with this? I am just thinking because dealing with full sub-bicategories will be an issue outside of Cat as well.

[joseph hua]

I think induced bicategories is probably better than what I suggested. Though, it is less obvious to me how to_app could be used if the bicategory structure on Grpd were defined using induced bicategory.

[Calle Sönne]

I guess you mean applying to_app to some lemmas about natural transformation between Grpds that do not already hold in Cat? Because I guess applying _app lemmas coming from Cat should be fine I think if we make the right simp lemmas.

[Calle Sönne]

Actually, so to_app specializes a lemma about general bicategories to Cat. If we have the right simp lemmas about the compatibility between forgetToCat and .app maybe we can always reuse the lemmas for Cat? So for example .app applied to a transformation between groupoids should simp to .app applied to the transformation between the images of forgetToCat?

[joseph hua]

Yes this sounds good. Since the 2-cells of the induced bicategory should literally be 2-cells in Cat, we only need the lemmas for 2-cells in Cat

[Calle Sönne]

Okay then as soon as #30132 gets merged I will rewrite my bicategory of groupoids PR to use induced bicategories.

[Calle Sönne]

Are bicategories whose underlying objects are categories some sort of categorification of concrete categories? If so maybe we should take some inspiration from ConcreteCategory to define this (although for now we only need full sub-bicategories which should make things a lot simpler).

[Calle Sönne]

I am doubting the induced category approach for Grpd as in the 1-category library people don't seem to use e.g. FullSubcategory (or InducedCategory) very often. The most popular approach seems to be to just define the category manually and then define the corresponding forgetful functor.

[Joël Riou]

When I manage to finish #26446, I would think that defining full subcategories as an abbreviation for ObjectProperty.FullSubcategory should be the norm rather than the exception.

[Calle Sönne]

Joël Riou said:

When I manage to finish #26446, I would think that defining full subcategories as an abbreviation for ObjectProperty.FullSubcategory should be the norm rather than the exception.

Okay that's good to know. Do you think ObjectProperty.FullSubcategory is preferred to InducedCategory? It seems way more common in Mathlib at least.

Also what's good is that what you do in your refactor is the way I have defined induced bicategories anyways (with Homs and even the 2-homs being structures and not type synonyms).

[Joël Riou]

InducedCategory and ObjectProperty.FullSubcategory should be equally good, as ObjectProperty.FullSubcategory is a particular case of InducedCategory.

[Calle Sönne]

Oh wait, InducedCategory is still a type synonym in your PR? Can this not lead to def-eq abuse? Or is the main problems the morphisms?

[Calle Sönne]

I guess you don't want to be rewriting/adding simp lemmas about objects in a category anyways, so this does not matter? In #30925 I made InducedBicategory its own structure, do you think it is not so bad if it's simply a type synonym?

[Joël Riou]

I feel that introducing a one field structure is important only for morphisms (but I may be wrong!).

[Calle Sönne]

Hmm. Maybe you are right. Since whenever you talk about f.hom (as in your PR) for example it is clear in what category to interpret the domain and codomains.

[Calle Sönne]

So maybe for induced bicategories its only important to have a separate structure for the 2-morphisms. I also like that for 1-categories this approach means that FullSubcategory is a special case of InducedCategory.

Just so I understand properly: the issue with def-eq abuse is really that it can prevent simp from firing when it should, and lead to undesirable erws?

[Joël Riou]

For full subcategories, etc, one of the issues is that when Lean sees a morphism, it may not necessarily know if it is a morphism in the ambient category or in the subcategory: by making very distinct types, no such confusion is possible, and it is a fact that automation works better in #26446 after doing the change.
Then, for induced 2-categories, it is probably not absolutely necessary to use a 1-field structure for objects, but a fortiori, from the experience of ordinary categories, the 1-morphisms should be a 1-field structure. I would also think that 2-morphisms should be a 1-field structure: when we consider these 2-morphisms only as morphisms in the category of morphisms, there should not be issues, but when we want to apply the bicategories operations like whiskerLeft/Right, it may become a problem like "Are we trying to do whiskerLeft in the original bicategory or in the induced one?". @Robin Carlier may have a more definite understanding of this?!

[Calle Sönne]

Yes but in some sense lean does know if it is in the ambient category or in the subcategory! Because currently various implementations of categories using InducedCategory does compile, even with this ambiguous notion of morphism. I understood that we do not have issues writing lemmas about the 1-morphisms the way they are now, since lean will be able to infer in what category they should be interpreted (I might be wrong about this though). It is the automation that breaks due to this def-eq abuse, but I have not fully grasped exactly in what way the automation breaks. That was more what I meant by my question. So e.g. is the main problem that simp is not working the way it should for InducedCategories currently?

[Calle Sönne]

I am not convinced that there will be issues with whiskering in that setting, since if we have a separate structure for 2-morphisms then lean should be able to infer from the 2-morphism in what bicategory we are whiskering. But possibly this will be an issue for simp.

[Calle Sönne]

Could a type synonym for objects not bring issues when talking about the yoneda functors Hom(-, x) for x in the subcategory? As a priori it will not be clear if x is taken to be an object of the subcategory or of the category itself.

[Joël Riou]

What I was trying to say is that 2-morphisms should also be made a 1-field struture, because otherwise it would not be clear in which bicategory we are doing whiskerLeft/Right.

[Calle Sönne]

Ah okay, this I definitely agree with.

[Calle Sönne]

But it seems to me that if it is fine to not make objects a 1 field structure for categories, then similarly it should be fine to not make 1-morphisms a 1 field structure for bicategories. As we should not be rewriting/simping equalities of 1-morphisms anyways.

[Joël Riou]

I am not convinced by this argument: we certainly want that dsimp works.

[Robin Carlier]

I most definitely agree that we at least want the 2-morphisms to be their own 1-field structure.

For 1-morphisms, my general experience is that things just work better with categories that have type aliases as objects (e.g Paths, Core, etc.) when we wrap the objects in 1-field structures: it’s not strictly necessary, and adds arguably some verbosity, but makes it so that we can’t have a term that has x : C where it should be x : Alias C by accident (and this can happens when relying on type inference as well), as it simply refuses to type check.

It’s certainly possible to have things working without 1-field structures in setup like this, by providing functions from the original type to the alias and in the other direction as well, and insert them carefully to guide type inference, but IMO this pattern is just trying to emulate (in a way that can still leads to accidental errors) what a 1-field structure gives for free (a constructor and a projection).

So my gut feeling for the bicategorical case would be that sticking to "1-morphisms are objects of a category", we can probably get away with not making 1-morphisms their own 1-field structure here but that we should be on the much safer side (as in: probably we’ll have less user error/things to think about when reviewing stuff about them) by just doing so.

[Calle Sönne]

Thanks for the extensive reply! In my induced bicategory PR, I also make the objects a 1-field structure. Given that we will not be doing this for 1-categories, do you think maybe its better to copy that approach and have the objects (only) as a type synonym?

[Robin Carlier]

Sorry, I’m not sure I’m getting the full proposal (do you mean that only objects are 1-field structs, say and then we have x.out ⟶ y.out as the category of 1-cells from x to y?), can you link some code doing this so that I can be sure of what you mean?

[Robin Carlier]

(In the two 1-categorical cases I cited, Paths and Core, the homs are not 1-field structure because there was a priori no way for lean to confuse x.as ≅ y.as or Paths x.as y.as as homs in some other categories. For DayFunctor, a similar type alias in which the hom-types are already hom-type in other categories, I made the hom-types 1-field structures as well. Quite frankly, I can’t remember if this was purely out of "let’s be safe" or if I ran into problems by not making it so...)

[Calle Sönne]

Here is the code: https://github.com/leanprover-community/mathlib4/pull/30925/files#diff-0ddf37b723590b6164533af42dc286d2dcf2f5db569873af30cbf12cf668abe5

There, the objects are a 1-field structure. I am wondering if I should make it into a simple type synonym to better match the 1-categorical case. (Also note that the 2-morphisms are not yet a 1-field structure in that PR, I have not gotten around to fixing this yet since its blocked by other PRs anyway). So to be clear I want 1-homs and 2-homs to be 1-field structures, but not the objects.

[Robin Carlier]

I think that in the end it depends on how we intend to use InducedBicategory.

It seems like the common usage of the 1-categorical pattern InducedCategory is to use as a step when defining instance on types which are their own structures/wrappers/aliases (e.g ObjectProperty.FullSubcategory, CommMon), instead of working directly with x : InducedCategory foo or phrasing things in terms of InducedCategory directly.

For this usage, I agree that it would perhaps make less sense to have its objects be a one-field struct as this might just add extra steps/indirection at the wrongs place (instead, when defining a bicategory structure using InducedBicategory, if the type of objects needs to be an alias, then we can make that type a 1-field struct and induce along the projection just fine).