The order type is a $Prop$-valued relation on coordinates rather than a three-valued code: in a linear order the strict-order pattern determines the equality pattern ($a i = a j$ exactly when neither $a i < a j$ nor $a j < a i$), so recording $<$ alone loses nothing and keeps decidability, $compare$ and $Ordering$ off the endorsement surface.

The definition is stated for an arbitrary linearly ordered vertex type, not only for $Fin n$: it is a pointwise notion, and proofs that consume it work over intermediate carriers. Statements of this submission still instantiate it at the canonical carriers.