{B : Type u} →
  [inst : Quiver B] →
    {a b c : B} →
      (f : Quiver.Path a b) →
        (g : Quiver.Path b c) →
          (CategoryTheory.FreeBicategory.preinclusion B).map
              (CategoryTheory.CategoryStruct.comp { as := f } { as := g }) ≅
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.FreeBicategory.preinclusion B).map { as := f })
              ((CategoryTheory.FreeBicategory.preinclusion B).map { as := g })