Commit 2026-10-08 18:10 1b3c4196

View on Github →

chore(CategoryTheory/Limits/Shapes/BinaryProducts): use to_dual (#43571) This PR uses to_dual on binary products/coproducts.

  • BinaryFan.fst/snd have been given a type manually so that the type is a simpler expression and doesn't involve Functor.const. This allows some simp only calls to now use fewer lemmas.
  • coprodComparison_inl was renamed to inl_coprodComparison, which is a more accurate name (and some analogous ones). Various other naming inconsistencies are also fixed.
  • As a result of aligning the APIs, some parameters changed from implicit to explicit, in particular inl_coprodComparison and inr_coprodComparison
  • As a result of aligning the APIs, some declarations were generalized from HasBinaryCoproducts _ to only the specific relevant HasBinaryCoproduct _ _, e.g. coprod.leftUnitor and coprod.braiding

Estimated changes