Supremum is Coproduct in Order Category

Theorem

Let $\mathbf P$ be an order category with ordering $\preceq$.

Let $p, q \in P_0$, and suppose they have some supremum $r = \sup \left\{{p, q}\right\}$.

Then $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.

Proof

Let $\mathbf P^{\text{op}}$ be the dual category of $\mathbf P$.

From Dual of Order Category, it is the order category corresponding to the dual ordering $\succeq$.

From Dual Pairs (Order Theory), it follows that in $\mathbf P^{\text{op}}$:

$r = \inf \left\{{p, q}\right\}$

where $\inf$ denotes infimum.

By Infimum is Product in Order Category, $r$ is the product of $p$ and $q$ in $\mathbf P^{\text{op}}$.

By Dual Pairs (Category Theory), $r$ is the coproduct of $p$ and $q$ in $\mathbf P$.

$\blacksquare$