Reflexification of a strict partial order ($x\le y⟺(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.