  We investigate predicative aspects of 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. Moreover, we prove that locally small, nontrivial (directed or
bounded) complete posets necessarily lack decidable equality. We prove our
results for a general class of posets, which includes e.g. directed complete
posets, bounded complete posets, sup-lattices and frames. Secondly, the fact
that these nontrivial posets are necessarily large has the important
consequence that Tarski's theorem (and similar results) cannot be applied in
nontrivial instances. Furthermore, we explain that generalizations of Tarski's
theorem that allow for large structures are provably false by showing that the
ordinal of ordinals in a univalent universe has small suprema in the presence
of set quotients. The latter also leads us to investigate the
inter-definability and interaction of type universes of propositional
truncations and set quotients, as well as a set replacement principle. Thirdly,
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.

Logic in Computer Science;Logic