∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {S T : CategoryTheory.Over X} (f₁ f₂ : R ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).left),
  CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.fst S.hom T.hom) =
      CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.fst S.hom T.hom) →
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.snd S.hom T.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.snd S.hom T.hom) →
      f₁ = f₂