∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (a b : CategoryTheory.Bicategory.InducedBicategory C F) {X Y Z : a ⟶ b}
  (u : CategoryTheory.Bicategory.InducedBicategory.Hom₂ X Y) (v : CategoryTheory.Bicategory.InducedBicategory.Hom₂ Y Z),
  (CategoryTheory.CategoryStruct.comp u v).hom = CategoryTheory.CategoryStruct.comp u.hom v.hom