论文标题
双重否定稳定的H呈立方组
Double negation stable h-propositions in cubical sets
论文作者
论文摘要
我们为双重否定的分类器构建稳定的H-合适，以各种立方体集合模型的同型理论和立方体类型理论。这用于给出一些相对一致性的结果：双重否定的分类器稳定命题在立方集中存在于元鉴定中； Dedekind实数可以添加到同型类型理论中，而不会改变一致性强度。我们构建了一个具有扩展教会论文的同型类型理论的模型，该论文指出，具有双重负稳定域的所有部分函数都是可计算的。
We give a construction of classifiers for double negation stable h-propositions in a variety of cubical set models of homotopy type theory and cubical type theory. This is used to give some relative consistency results: classifiers for double negation stable propositions exist in cubical sets whenever they exist in the metatheory; the Dedekind real numbers can be added to homotopy type theory without changing the consistency strength; we construct a model of homotopy type theory with extended Church's thesis, which states that all partial functions with double negation stable domain are computable.
