Limits commute with binary products

Stream: Is there code for X?

[Sophie Morel]

Hi everybody, to prove that the category of group objects in a category $C$ has limits of a certain type whenever $C$ does, I need the fact that limits commute with binary products. Now mathlib has a very general Fubini theorem for limits (and colimits) there, but I run into universe problems when I try to use it. For example, I wanted to use this statement with K equal to my indexing category and J equal to Discrete WalkingPair, but the statement in question requires J and K to be in the same universe as the hom sets of C. This would be okay for K, but Discrete WalkingPair has a fixed universe level, which is 0, and that's a pretty strong constraint to put on C (what if it's a presheaf category, for instance?).
Did I miss something? I really don't look forward to playing around with ULift...

[Andrew Yang]

I think we (maybe you!) can try to generalize the universe arguments in that file?

[Sophie Morel]

Er maybe, but not today, I had to get up at 3:30 am to catch the Eurostar...
More importantly, I'd like to be sure that it is really necessary before I start on something like that.

[Sophie Morel]

Well guess what, I removed all universe constraints in the mathlib file on Fubini for limits, and it still compiles... The only issue was that at some point there's an instance HasLimits C that only gives limits of size the Hom sets of C, but you can just replace it with hypotheses that the needed limits exist (maybe they are very big limits, but who cares).

[Andrew Yang]

There is docs#CategoryTheory.Limits.HasLimitsOfSize (of which HasLimits is an abbreviation)

[Sophie Morel]

I think it's better anyway to only put the hypotheses that are needed. I need limits indexed by like 4 categories, it's massive overkill to suppose that C has all limits indexed by categories of the same size.