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.

翻译：我们研究了构造性单值基础中的谓词性方面。所谓谓词性和构造性，分别指我们既不假定Voevodsky的命题缩放公理，也不假定排中律。我们的工作通过探索在单值基础中谓词性地无法完成的事项，补充了现有的谓词性数学研究。第一个主要结果是：非平凡（有向或有界）完全偏序集必然是大规模的。即，如果这样一个非平凡偏序集是小的，则弱命题缩放成立。若将非平凡性加强为积极性，则可推导出完全命题缩放。非平凡性与积极性之间的区别类似于非空性与可居住性之间的区别。此外，我们证明：局部小的非平凡（有向或有界）完全偏序集必然缺乏可判定相等性。我们针对一类广义偏序集证明了这些结果，其中包括有向完备偏序集、有界完备偏序集、上确界格和框架。其次，这些非平凡偏序集必然是大规模的这一事实具有重要推论：塔斯基定理（及类似结果）无法应用于非平凡实例。进一步地，我们通过证明：在单值宇宙中，序数之序数在存在集合商的情况下具有小上确界，从而表明允许大规模结构的塔斯基定理推广是显然错误的。后者也引导我们研究命题截断与集合商类型宇宙之间的相互可定义性与互动，以及集合替换原则。第三，在我们的谓词性设定下，我们澄清了传统上要求所有子集上确界的上确界格定义与我们要求所有小族上确界的定义之间的关系。