@sliminality@types.pl When people told me this holds for real numbers in #constructiveMathematics (in fact is often the definition of ≤), I didn't believe them at first. But not only did my collaborators tell me this was a good definition and I read it in the HoTT Book, but I also found it allowed me to prove the expected theorems about ≤