Commit 2025-10-02 17:25 3576a645

feat(CategoryTheory/Bicategory): EqToHom for bicategories (#28242) We generalize the eqToHom construction from Category to CategoryStruct, allowing its usage in bicategorical contexts. We introduce a file CategoryTheory/Bicategory/EqToHom that records some of the properties of eqToHoms 1-morphisms and 2-morphisms, such as the transitivity up to isomorphism of eqToHom 1-morphisms, and congruence lemmas for unitors, associators and whiskering with respects to eqToHom 2-morphisms. This generalization and these congruence lemmas will be used to define icons between lax functors, and work with categories of strictly unitary lax/pseudo-functors (e.g for pseudocomposable arrows and lax-composable arrows in bicategories, which are part of the definitions of nerve constructions in bicategories).