where to place bicategory lemma

Stream: mathlib4

[Calle Sönne]

I need the following lemma (about Oplax functors) in an upcoming PR:

lemma map₂_eqToHom {a b : B} {f g : a ⟶ b} (h : f = g) :
    F.map₂ (eqToHom h) = eqToHom (F.congr_map h) := by
  subst h; simp only [eqToHom_refl, OplaxFunctor.map₂_id]

I'm not sure where to place it, as Bicategory/Functor currently does not import eqToHom and I'm worried this will add a lot of imports that are not really needed there. It also feels weird to add a new file Bicategory/eqToHom just for this one lemma. Does anyone have any recommendations?

[Kevin Buzzard]

I think the community is moving on from the weird feelings and is now rather disposed to having lots of small files.

[Adam Topaz]

I think a natural place might be the file about locally discrete bicats

[Calle Sönne]

Adam Topaz said:

I think a natural place might be the file about locally discrete bicats

Okay that sound reasonable