• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Constructions with Non-Recursive Higher Inductive Types
【24h】

Constructions with Non-Recursive Higher Inductive Types

机译：具有非递归更高电感类型的结构

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify over elements or paths in H. The advantage of non-recursive HITs is that their elimination principles are easier to apply than those of general HITs.It is an open question which classes of HITs can be encoded as non-recursive HITs. One result of this paper is the construction of the propositional truncation via a sequence of approximations, yielding a representation as a non-recursive HIT. Compared to a related construction by van Doorn, ours has the advantage that the connectedness level increases in each step, yielding simplified elimination principles into n-types. As the elimination principle of our sequence has strictly lower requirements, we can then prove a similar result for van Doorn's construction. We further derive general elimination principles of higher truncations (say, k-truncations) into n-types, generalizing a previous result by Capriotti et al. which considered the case n ≡ k + 1.
机译：同型感应类型（HITS）在同型型理论中是一种强大的电感类型的泛化。它们不仅可以具有普通的构造函数来定义元素，还可以定义更高的构造函数来定义平等（路径）。我们说，如果其构造函数没有量化的元素或路径，则一个HIT H是非递归的。非递归命中的优点是它们的消除原则比普通匹配项更容易申请。它是一个打开的问题可以编码哪个命中作为非递归点击。本文的一个结果是通过近似序列构建命题截断，从而产生作为非递归击中的表示。与Van Doorn的相关建筑相比，我们的优点是，每个步骤中的连接水平增加，产生简化的消除原理进入N型。由于我们序列的消除原则严格降低了要求，我们可以证明Van Doorn的建筑的类似结果。我们进一步推导出普遍消除更高截断的原则（例如，k截断）进入n型，概括了Capriotti等人的先前结果。考虑到案例n k + 1。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号