{D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D] →
      (A : CategoryTheory.AddMon D) → Unique (A ⟶ CategoryTheory.AddMon.trivial D)