Commit 2025-09-01 13:46 6ecc08fc

chore(CategoryTheory/Bicategory): move map₂_eqToHom earlier in the import graph (#28287) The lemma PrelaxFunctor.map₂_eqToHom currently sits in the file CategoryTheory/Bicategory/LocallyDiscrete. This has low discoverability, and it is unavailable to other files that deals with eqToHoms, such as CategoryTheory/Bicategory/Functor/Strict. We move the lemma in the file Category/Bicategory/Functor/Prelax. This comes at the cost of an extra import (CategoryTheory.EqToHom) in the file. The lemma is unsimped for consistency with the corresponding lemma for ordinary categories, which is intentionally not a simp lemma. We also sneak in the eqToIso version for completeness.