plt-amy
`is-total-order` is not a property
Currently, the definition of is-total-order is
record is-total-order {o ℓ} (P : Poset o ℓ) : Type (o ⊔ ℓ) where
open Poset P public
field
compare : ∀ x y → (x ≤ y) ⊎ (y ≤ x)
This is not a property: in a discrete order, this is equivalent to a function compare : P -> P -> Bool. This can be fixed by truncating the result of compare; note that we can still compute meets and joins, as those are properties!
let's rename it instead of truncating. the things you want to do with a decidable total order are things like sorting which it would be very inconvenient to prove that a sorting is unique and then like do choice over the list to get all the possible comparisons upfront or something
Can we use (x ≤ y) ⊎ (y < x) instead, where y < x is y ≤ x × y ≠ x? That is a proposition and is probably usable for sorting? I'm not sure if it's (logically) equivalent to what we have now, though. EDIT: probably not, unless the underlying set is discrete.
If that still lets you compute meets and joins then I guess that works because is-total-order is only used for that and the definition of is-decidable-total-order which implies discreteness (and that's what you'd (i did) use in a sorting algorithm)
Is src/Order/Total.lagda.md the only file to change ? Because if so there is only 8 lines to change and 1 to add to use this new definition
(see this commit)
Why not compare : ∀ x y → (x ≤ y) ∗ (y ≤ x), where _∗_ is as defined in Homotopy.Join? This is equivalent to ∥ (x ≤ y) ⊎ (y ≤ x) ∥, but has a more convenient universal property.
