Strict partial order ($<$)

A strict partial order is an irreflexive transitive relation. In a classical set, it corresponds to a partial order through reflexification, but recovering the strict relation from the weak one requires inequality. In an arbitrary topos, this reverse operation need not be geometric or define an inverse interpretation.

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.