The HoTT book has a proof that if excluded middle holds then all ordinals are trichotomous, meaning that x < y or x = y or x > y.

Ohad Kammar gave a better proof.

Today my colleague Paul Blain Levy improved both the proof and at the same time strengthened the statement: An ordinal is trichotomous if and only if its order is decidable.
1/

#hott #univalentFoundations #constructiveMathematics
#neutralMathematics