论单价基础中的小类型
On Small Types in Univalent Foundations
摘要：
我们调查建设性的单价基础的谓词方面。通过谓词和构造性，我们分别意味着我们不假设Voevodsky的命题公理或排中律。我们的工作补充了现有的工作预测数学探索什么不能做预测在单价基础。我们的第一个主要结果是，非平凡的（有向或有界）完全偏序集必然是大的。也就是说，如果这样一个非平凡偏序集是小的，那么弱命题集成立。如果我们把非平凡性加强到正性，就有可能导出完整的命题正性。非平凡性和积极性之间的区别类似于非空性和居住性之间的区别。此外，我们证明了局部小，非平凡（有向或有界）完全偏序集必然缺乏可判定的平等。我们证明了我们的结果一般类的偏序集，其中包括例如有向完备偏序集，有界完备偏序集，超格和框架。其次，这些非平凡偏序集必然很大的事实有一个重要的推论，就是塔斯基定理（以及类似的结果）不能应用于非平凡的例子。此外，我们解释说，塔斯基定理，允许大结构的推广是可证明为假的，在一个单价宇宙中的序数序数有小的上确界的存在下，设置consistents。后者也导致我们调查的相互定义性和相互作用的类型宇宙的命题截断和集的替代品，以及一个集替换原则。第三，我们澄清，在我们的谓词设置，之间的关系的传统定义的超格，要求所有子集的上确界和我们的定义，要求所有小家庭的上确界。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
