Is there an alternative definition of finite-coproduct categories? In order theory, there's two possible definitions of the term unital join-semilattice.


*

*A unital join-semilattice is a poset $P$ with a least element $0$, such that for any two $x,y \in P$, there exists a least upper bound $x \vee y \in P$.

*A unital join-semilattice is a set $S$ together with a distinguished element $0 \in S$ and a distinguished function $\vee : S \times S \rightarrow S$ satisfying the axioms for an idempotent commutative monoid.
Is there anything like this in category theory? In particular, I want to replace unital join-semilattices with finite-coproduct categories. The problem then becomes the second dot point. I was thinking maybe we can replace $S$ with a groupoid equipped with a symmetric monoidal structure, together with some coprojection and codiagonal maps. The details aren't clear to me. For example, can we speak of the "underlying category" of such a thing?
 A: A poset with a least element is generalised to a category with an initial element:
just pretend the arrows are inclusions to see this.
A poset with a lub for each pair of items is generalised to a category with sums:
just pretend the arrows are inclusions within the sum universal property and from
that you can obtain the lub properties.
For your second point, the idea is essentially the same:
you want a category with an inital object and a functor that assisgns pairs of objects
to their sum within the category.
Categories can be thought of as coherently constructive lattices!
A: Here are some possible definitions of a finite coproduct category, essentially generalizing the definitions you had.


*

*A finite coproduct category is a category with an initial object such that any pair of objects has a coproduct.  

*A finite coproduct category is a category $\mathcal{C}$ equipped with functors $\mathcal{C}\times\mathcal{C}\to \mathcal{C}$ and $1\to \mathcal{C}$ that are left adjoints to the diagonal functor $\mathcal{C}\to \mathcal{C}\times\mathcal{C}$ and the unique functor $\mathcal{C}\to 1$ respectively. This was already mentioned in the comments.

*A finite coproduct category is a symmetric monoidal category $(\mathcal{C},\otimes,I,\alpha,\rho,\lambda,\sigma)$ equipped with codiagonals, i.e. a monoidal natural transformation with components $A\otimes A\to A$ and a monoidal natural transformation with components $I\to A$ such that certain diagrams commute. These diagrams are essentially the unit-counit equations from the previous definition, so in a sense we're only doing a change of language here. On the other hand, those same equations could be interpreted as equipping each object with the structure of a monoid, which leads to our final definition.

*A finite coproduct category is a symmetric monoidal category $(\mathcal{C},\otimes,I,\alpha,\rho,\lambda,\sigma)$ such that the forgetful functor $cMon(\mathcal{C})\to\mathcal{C}$ is an isomorphism, where  $cMon(\mathcal{C})$ is the category of commutative monoids in $\mathcal{C}$. 


Assuming enough choice these amount to the same thing.
