Master thesis by Arnoud van der Leer: Universal Algebra, Univalent Foundations and the Untyped λ-Calculus

"This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. [...] The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation."

https://repository.tudelft.nl/record/uuid:e6582866-9c0d-4a13-8eda-42c25e0deba4

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