Predicative Aspects of Order Theory in Univalent Foundations

Tom de Jong, Martín Hötzel Escardó

We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's pr…