Reflexification of a strict partial order
= Reflexification of a strict partial order
{title2=$x\le y\;\Longleftrightarrow\;(x<y)\vee(x=y)$}
Reflexification turns a <strict partial order> into a <partial order>. Reflexivity is immediate, transitivity follows by the four disjunction cases, and antisymmetry follows because two opposed strict comparisons imply a forbidden self-comparison. The construction uses only <coherent logic>, so is preserved by <inverse image functors of geometric morphisms>.