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