About partial ordering

Partial ordering should not use the ≤ symbol. It is disrespectful to equality.

A partial ordering operator on a set is as follows. Given two members, they are either ordered or unordered. If ordered, either one may be ordered before another.

inductive PartialOrder
| less
| unordered
| greater

tryOrder : A -> A -> PartialOrder

Then, transitivity is optional.

Math is fun outside the beaten path. I feel terrified that the mainstream math notation even overloads the equal sign to mean two totally different concepts.