Category of Ordered Sets has Enough Constants
Theorem
Let $\mathbf{OrdSet}$ be the category of ordered sets.
Then $\mathbf{OrdSet}$ has enough constants.
Proof
By Singleton Ordered Set is Terminal Object, we have that any ordered set with a singleton as underlying set is terminal in $\mathbf{OrdSet}$.
Let $1$ be such a singleton ordered set.
To show that $\mathbf{OrdSet}$ has enough constants, it is to be shown that if:
- $f: P \to Q \ne g: P \to Q$
then there exists an $x: 1 \to P$ such that $f \circ x \ne g \circ x$.
Now by definition of $\mathbf{OrdSet}$, $f$ and $g$ are increasing mappings.
In particular, they are mappings, and by Equality of Mappings, there must be a $p \in P$ such that:
- $\map f p \ne \map g p$
Define $\bar p: 1 \to P$ by $\map {\bar p} * = p$ (where $*$ is the unique element of $1$).
If this is a morphism in $\mathbf{OrdSet}$, we are evidently done.
This follows from Mapping is Constant iff Increasing and Decreasing.
Hence $\mathbf{OrdSet}$ has enough constants.
$\blacksquare$
Sources
- 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous) ... (next): $\S 2.3$: Example $2.12$: $1$