Binary (co)products of (co)products

Stream: Is there code for X?

[Robert Maxton]

Is there a reason we don't already have an instance for synthesizing [HasBinary(Co)Products C] from a [Has(Co)Products C], or is this something I should PR?

[Robin Carlier]

import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
open CategoryTheory Limits

example (B : Type u) [Category.{v} B] [HasProducts.{0} B] :
    HasBinaryProducts B := by
  infer_instance -- works

example (B : Type u) [Category.{v} B] [HasProducts B] :
    HasBinaryProducts B := by
  infer_instance --fails

I guess the issue is that HasProducts is an abbrev for ∀ J : Type w, HasLimitsOfShape (Discrete J) C, and
HasBinaryProducts for HasLimitsOfShape (Discrete WalkingPair) C, but the walking pair is in Type...

[Robin Carlier]

attribute [local instance] has_smallest_products_of_hasProducts in
example (B : Type u) [Category.{v} B] [HasProducts B] :
    HasBinaryProducts B := by
  infer_instance

works, and if you import Limits.Shapes.Countable, then it also works (without the local instance) because docs#CategoryTheory.Limits.hasCountableProducts_of_hasProducts (which uses this local instance behind the scene) is in scope then.
Maybe docs#CategoryTheory.Limits.has_smallest_products_of_hasProducts was not made a global instance for perf reasons?

[Robin Carlier]

The discussion in !3#15067 seems to suggest at the time there was a potential instance loop when making it an instance.

[Robin Carlier]

Also, since things like docs#CategoryTheory.Limits.hasCountableProducts_of_hasProducts have to exist and be explicitly recorded and are instances, I guess this means that it would make sense to add an instance CategoryTheory.Limits.hasBinaryProducts_of_hasProducts, but it’s probably best if a maintainer confirms.