Predicative Aspects of Order Theory in Univalent Foundations

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

Thumbnail PDF


  • Filesize: 0.76 MB
  • 18 pages

Document Identifiers

Author Details

Tom de Jong
  • University of Birmingham, UK
Martín Hötzel Escardó
  • University of Birmingham, UK

Cite AsGet BibTex

Tom de Jong and Martín Hötzel Escardó. Predicative Aspects of Order Theory in Univalent Foundations. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


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 propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. We prove our results for a general class of posets, which includes directed complete posets, bounded complete posets and sup-lattices, using a technical notion of a δ_V-complete poset. We also show that nontrivial locally small δ_V-complete posets necessarily lack decidable equality. Specifically, we derive weak excluded middle from assuming a nontrivial locally small δ_V-complete poset with decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we show that each of Zorn’s lemma, Tarski’s greatest fixed point theorem and Pataraia’s lemma implies propositional resizing. Hence, these principles are inherently impredicative and a predicative development of order theory must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constructive mathematics
  • Theory of computation → Type theory
  • order theory
  • constructivity
  • predicativity
  • univalent foundations


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. URL:
  2. Peter Aczel and Michael Rathjen. Notes on constructive set theory. Book draft, August 2010. URL:
  3. J. L. Bell. Zorn’s lemma and complete Boolean algebras in intuitionistic type theories. The Journal of Symbolic Logic, 62(4):1265-1279, 1997. URL:
  4. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics, volume 97 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1987. Google Scholar
  5. Douglas S. Bridges and Luminiţa Simona Vîţǎ. Apartness and Uniformity: A Constructive Development. Springer, 2011. URL:
  6. Thierry Coquand, Giovanni Sambin, Jan Smith, and Silvio Valentini. Inductively generated formal topologies. Annals of Pure and Applied Logic, 124(1-3):71-106, 2003. URL:
  7. Giovanni Curi. On some peculiar aspects of the constructive theory of point-free spaces. Mathematical Logic Quarterly, 56(4):375-387, 2010. URL:
  8. Giovanni Curi. On the existence of Stone-Čech compactification. The Journal of Symbolic Logic, 75(4):1137-1146, 2010. URL:
  9. Giovanni Curi. On Tarski’s fixed point theorem. Proceedings of the American Mathematical Society, 143(10):4439-4455, 2015. URL:
  10. Giovanni Curi. Abstract inductive and co-inductive definitions. The Journal of Symbolic Logic, 83(2):598-616, 2018. URL:
  11. Giovanni Curi and Michael Rathjen. Formal Baire space in constructive set theory. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, volume 3 of Ontos Matematical Logic, pages 123-136. De Gruyter, 2012. URL:
  12. Tom de Jong and Martín Hötzel Escardó. Domain theory in constructive and predicative univalent foundations. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:18. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. URL:
  13. Martín H. Escardó. Joins in the frame of nuclei. Applied Categorical Structures, 11:117-124, 2003. URL:
  14. Martín H. Escardó and Cory M. Knapp. Partial elements and recursion via dominances in univalent type theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2017. URL:
  15. Martín Hötzel Escardó. Introduction to univalent foundations of mathematics with Agda, November 2020. URL:
  16. Martín Hötzel Escardó. Various new theorems in constructive univalent mathematics written in Agda., June 2020. Agda development.
  17. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. Continuous Lattices and Domains, volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 2003. URL:
  18. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, CS 6:43-59, 2006. URL:
  19. Peter T. Johnstone. Open locales and exponentiation. In J. W. Gray, editor, Mathematical Applications of Category Theory, volume 30 of Contemporary Mathematics, pages 84-116. American Mathematical Society, 1984. URL:
  20. Dito Pataraia. A constructive proof of Tarski’s fixed-point theorem for dcpos. Presented at the 65th Peripatetic Seminar on Sheaves and Logic, 1997. Google Scholar
  21. Giovanni Sambin. Intuitionistic formal spaces - a first communication. In Mathematical logic and its applications, pages 187-204. Springer, 1987. URL:
  22. Michael Shulman. Idempotents in intensional type theory. Logical Methods in Computer Science, 12(3):1-24, 2016. URL:
  23. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. URL:
  24. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics., Institute for Advanced Study, 2013.
  25. Benno van den Berg. Predicative topos theory and models for constructive set theory. PhD thesis, Utrecht University, 2006. URL:
  26. Vladimir Voevodsky. Resizing rules - their use and semantic justification. Slides from a talk at TYPES, Bergen, 11 September, 2011. URL:
  27. Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5):1278-1294, 2015. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail