Commit 2025-12-02 15:26 656d9cd4

feat(Bicategory/Product): add products of bicategories (#31169) In this PR the cartesian product of bicategories is added. I also partially revert, only for products, a previous change which removed the simps projection _Hom from CategoryStruct. The reason for this is that simp is no longer able to apply lemmas like (𝟙 X).1 = 𝟙 X.1 due to defeq abuse of the notation .1 for homomorphisms in this category. The solution to this would be to add a type-alias for Hom in case of products, however I am not convinced this is worth it, as we would lose the notation (𝟙 X).1 which is heavily used in mathlib and would take ages to replace everywhere. What is lost from including _Hom as a simp lemma is that after application, simp can no longer know that it is the Hom type in some category. However since the product is such a simple structure, simp should be able to easily recover any such results after projection to the two factors. Therefore I believe not much is lost in this specific case.