Post #1511729

as an example, i had a very interesting discussion on irc the other day about the relationship between total orders and decidable orders. if you define totality in the "obvious" way, as \((x\ y : S) \to x \le y \uplus y \le x\), this turns out to be equivalent to decidability of the order (better still, the proof is surprisingly tricky)! to distinguish the two notions, you need to be sure that totality is valued in propositions, and define it as something like \((x\ y : S) \to \| x\le y \uplus y \le x \|\). it's a neat bit of subtlety which simply disappears classically