{α : Type u_5} →
  {β : Type u_6} →
    {inst : NonAssocSemiring α} →
      {inst_1 : NonAssocSemiring β} →
        {P : Sort u} →
          {toMonoidHom : α →* β} →
            {map_zero' : (↑toMonoidHom).toFun 0 = 0} →
              {map_add' : ∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y} →
                {toMonoidHom' : α →* β} →
                  {map_zero'' : (↑toMonoidHom').toFun 0 = 0} →
                    {map_add'' :
                        ∀ (x y : α),
                          (↑toMonoidHom').toFun (x + y) = (↑toMonoidHom').toFun x + (↑toMonoidHom').toFun y} →
                      { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' } =
                          { toMonoidHom := toMonoidHom', map_zero' := map_zero'', map_add' := map_add'' } →
                        (toMonoidHom ≍ toMonoidHom' → P) → P