Reflexification of a strict partial order

ID: reflexification-of-a-strict-partial-order

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.

New to topics? Read the docs here!