Post #1487035
2026-04-18 19:59 UTC
Replies (5)
-
@ncf@types.pl 2026-04-19 14:02
(The solution is now here: https://1lab.dev/Order.Total.html#as-discrete-total-orders)
-
@jeanas@mathstodon.xyz 2026-04-18 20:07
@ncf By “relation”, do you mean a mere relation or a proof-relevant relation?
-
@mei@donotsta.re 2026-04-18 23:12
@ncf this feels... extremely unintuitive. like, there's no data to go off! everything's truncated! (assuming the type that's being related in a set, i guess) how can you ever construct anything that's not a proposition out of this?
-
@hallasurvivor@sunny.garden 2026-04-19 17:31
@ncf Thanks for the puzzle and the solution!! That's REALLY clever, and I don't think I've seen the trick before. Perfectly sized to think about over a late breakfast 💖
-
@jac@types.pl 2026-04-19 18:44
@ncf I assume by relation you mean prop-valued. In that case decidability is effectively a prop (even without extensionality we can factor through its truncation) strong total => decidable: so eliminate the truncation and we have inputs x y, and a function `d: ∀ x y. (x ≤ y) + (y ≤ x)`. We play this function against itself: consider d x y, and d y x. If the first returns the left branch or the latter returns the right, we're done by picking x ≤ y. But otherwise we have y ≤ x, in which case given x ≤ y we have x = x, and hence the two functions must have agreed, and hence we have a contradiction strong total <= decidable: Given a decision d, and any inputs x y, let's prove x ≤ y + y ≤ x, Consider d x y, d y x. If Either returns their first input, we are done. But if both return the negation, we have a contradiction using totality, hence we have handled all cases.