{B : Type u} →
  [inst : Quiver B] →
    {a b c d : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.FreeBicategory.Hom₂
              (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)