∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G H : CategoryTheory.Grp C) {T : CategoryTheory.Grp C} (f : T ⟶ G)
  (g : T ⟶ H),
  CategoryTheory.CategoryStruct.comp
      ((fun {T} f g => { hom := CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom }) f g)
      (CategoryTheory.Limits.BinaryFan.mk
          (CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.fst G.toMon H.toMon))
          (CategoryTheory.Grp.homMk' (CategoryTheory.SemiCartesianMonoidalCategory.snd G.toMon H.toMon))).snd =
    g