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.

翻译：我们研究了构造性单值基础的谓词性方面。所谓谓词性和构造性，分别指我们不假设弗拉基米尔·沃埃沃茨基的命题大小调整公理或排中律。我们的工作通过探索在单值基础中哪些内容无法以谓词方式完成，补充了现有关于谓词性数学的研究。我们的第一个主要结果是：非平凡（有向或有界）完全偏序集必然是大的。也就是说，如果这样一个非平凡偏序集是小的，则弱命题大小调整成立。若将非平凡性增强为积极性，则可以推导出完全命题大小调整。非平凡性与积极性之间的区别类似于非空性与被占据性之间的区别。此外，我们证明局部小且非平凡（有向或有界）完全偏序集必然缺乏可判定相等性。我们的证明适用于一类广义偏序集，包括有向完全偏序集、有界完全偏序集、上确界格和框架等。其次，这些非平凡偏序集必然是大这一事实的重要推论是：塔斯基定理（及其类似结果）无法应用于非平凡实例。此外，我们通过证明单值宇宙中的序数序集在存在集合商的情况下具有小上确界，说明允许大结构的塔斯基定理推广是命题可证伪的。后者也引导我们研究命题截断与集合商类型宇宙之间的相互可定义性与相互作用，以及集合替换原则。第三，我们在谓词性框架下阐释了传统上要求所有子集上确界的上确界格定义与我们要求所有小族上确界的定义之间的关系。