一句话：在构造性单值基础中证明非平凡完备偏序集必然是大类型，并揭示 Tarski 定理的谓词式限制。
本文在构造性单值基础中研究谓词式方面，不假设命题消解与排中律，考察哪些构造不能谓词式完成。主要结果：非平凡的（有向或有界）完备偏序集必然是大类型；若其小则弱命题消解成立，加强为正性可推出完整命题消解。非平凡性与正性之别类似非空与居留。还证明局部小且非平凡的此类偏序集缺乏可判定相等。结果覆盖有向/有界完备偏序集、sup-lattice 与 frame。由此 Tarski 定理不能用于非平凡实例，允许大结构的推广可证伪，并引出命题截断与集合商类型宇宙的相互作用及集合替换原则，最后澄清传统 sup-lattice 定义与小族上确界定义的关系。
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.