Bundled in CategoryTheory

Stream: mathlib4

[Calle Sönne]

Bundled seems to be used only 4-5 times in mathlib, and both BundledHom and UnbundledHom are used 0 times outside of the files they have been defined in. Should these be/are these in the process of being deprecated? The only time I see Bundled being used is to define subcategories of Cat (e.g. Grpd or Quiver, which should all be replaced with some bicategorical notion at some point anyways) and also at a few places in the model theory library.

[Calle Sönne]

It seems that most places where it was used before, it has been replaced by the structure ObjectProperty.FullSubcategory.

[Calle Sönne]

Actually a comment in the Bundled file refer to TopCat and MonCat neither of which are implemented using bundled anymore, both instead are implemented manually. So it seems we prefer to not use bundled anymore. I think that I missed when this switch was happening, was this part of solving the erw issues with concrete categories? (Edit: seems so, as I found this: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Concrete.20category.20class.20redesign/near/493903980 now)

[Calle Sönne]

If so, can I remove the final instances of bundled and deprecate these files?

[Kim Morrison]

Yes please!

[Aaron Anderson]

Calle Sönne said:

Bundled seems to be used only 4-5 times in mathlib, and both BundledHom and UnbundledHom are used 0 times outside of the files they have been defined in. Should these be/are these in the process of being deprecated? The only time I see Bundled being used is to define subcategories of Cat (e.g. Grpd or Quiver, which should all be replaced with some bicategorical notion at some point anyways) and also at a few places in the model theory library.

I wrote much of that part of the model theory library - would it be helpful for me to rewrite that, or are you working on it already and I should save my thoughts for a review?

[Calle Sönne]

Hi! I planned to contact you about it when I got to that point actually, so it's nice that you messaged here :)

After a brief look in the model theory library, I didn't see a clear way to remove it from there, but more importantly I need to figure out what should be replacing the ~3 remaining uses in the category theory library. I thought I knew how to replace it, but now I think it is more tricky than that (and maybe something like Bundled will be needed after all). Once I have a solution to this, then maybe it will be clear that the cases in the model theory library can just be refactored to use whatever my solution is.

[Aaron Anderson]

I think I can take essentially the same approach as MonCat and AddMonCat. It would be nice to also define the actual categories induced by first-order homomorphisms, embeddings, and elementary embeddings on L.Structures and T.ModelTypes, but this would presumably require a bunch of type synonyms.

[Aaron Anderson]

I'm trying it here: #32285

[Adrian Marti]

The category of categories Cat is defined using Bundled. I currently need this for a project. Are there going to be any changes to this soon or am I fine using it?

Also, I'm naturally inclined to have certain constructions take a C : Cat instead of a C : Type u and a Category C, since I'm using a certain functor F : Cat -> Catand I don't want to constantly call Bundled.mk to apply it to an argument. Is there some reason I should be discouraged from using this approach?

[Calle Sönne]

Adrian Marti said:

The category of categories Cat is defined using Bundled. I currently need this for a project. Are there going to be any changes to this soon or am I fine using it?

Also, I'm naturally inclined to have certain constructions take a C : Cat instead of a C : Type u and a Category C, since I'm using a certain functor F : Cat -> Catand I don't want to constantly call Bundled.mk to apply it to an argument. Is there some reason I should be discouraged from using this approach?

I don't think you should worry, as in whatever way it is replaced, most of the API should stay the same. Also I don't think you should be using Bundled.mk but rather Cat.of (which will likely remain the name after that refactor).

Maybe what you should note is that there is the PR #31807 which adds type-aliases to distinguish functors and 1-morphisms in Cat as well as natural transformations and 2-morphisms. This should improve automation.

[Calle Sönne]

Aaron Anderson said:

I think I can take essentially the same approach as MonCat and AddMonCat. It would be nice to also define the actual categories induced by first-order homomorphisms, embeddings, and elementary embeddings on L.Structures and T.ModelTypes, but this would presumably require a bunch of type synonyms.

Yes, but I actually don't fully understand why this is not done using Bundled (or something like it). Much of the setup seems the same.

[Edward van de Meent]

Adrian Marti said:

... and I don't want to constantly call Bundled.mk to apply it to an argument. Is there some reason I should be discouraged from using this approach?

to start with, you should be using Cat.of instead

[Adrian Marti]

Thank both of you I will do that :)