Predicative Aspects of Order Theory in Univalent Foundations

We investigate predicative aspects of order theory in constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively. 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 impredicativity holds. It is possible to derive full impredicativity if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonempty and inhabited types. 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 $\delta$-complete poset. We also show that nontrivial locally small $\delta$-complete posets necessarily lack decidable equality. Specifically, we can derive weak excluded middle from assuming that a nontrivial locally small $\delta$-complete poset has decidable equality. Moreover, if we assume positivity instead of nontriviality, then we can derive full excluded middle. Secondly, we prove that Zorn's lemma, Tarski's greatest fixed point theorem and Pataraia's lemma all imply impredicativity axioms. Hence, these principles are inherently impredicative and a predicative development of order theory (in univalent foundations) must therefore do without them. Finally, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattices that requires suprema for all subsets and our definition that asks for suprema of all small families. This is important in practice in order to obtain workable definitions of dcpos, sup-lattices, etc. in the context of predicative univalent mathematics.