Post #2061453

@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.