∀ {B : Type u_2} {C : Type u_3} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X Y : CategoryTheory.Bicategory.InducedBicategory C F) {X_1 Y_1 : X ⟶ Y}
  (f : CategoryTheory.Bicategory.InducedBicategory.Hom₂ X_1 Y_1),
  { hom := CategoryTheory.CategoryStruct.comp { hom := CategoryTheory.CategoryStruct.id X_1.hom }.hom f.hom } = f