∀ {B : Type u_3} {C : Type u_4} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom),
  CategoryTheory.CategoryStruct.comp { hom := φ.hom } { hom := φ.inv } = CategoryTheory.CategoryStruct.id f