{B : Type u} →
  {inst : Quiver B} →
    {P : Sort u_1} →
      {a b : B} →
        {f : a ⟶ b} →
          {a' b' : B} →
            {f' : a' ⟶ b'} →
              a = a' →
                b = b' →
                  CategoryTheory.FreeBicategory.Hom.of f ≍ CategoryTheory.FreeBicategory.Hom.of f' →
                    (a ≍ a' → b ≍ b' → f ≍ f' → P) → P