首页> 外文OA文献 >Extending homotopy type theory with strict equality
【2h】

Extending homotopy type theory with strict equality

机译:用严格相等性扩展同伦类型理论

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务,本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文,但由于OA文献来源多样且变更频繁,仍可能出现获取不到、文献不完整或与标题不符等情况,如果获取不到我们将提供退款服务。请知悉。

摘要

In homotopy type theory (HoTT), all constructions are necessarily stable under homotopy equivalence. This has shortcomings: for example, it is believed that it is impossible to define a type of semi-simplicial types. More generally, it is difficult and often impossible to handle towers of coherences. To address this, we propose a 2-level theory which features both strict and weak equality. This can essentially be represented as two type theories: an ``outer'' one, containing a strict equality type former, and an ``inner'' one, which is some version of HoTT. Our type theory is inspired by Voevodsky's suggestion of a homotopy type system (HTS) which currently refers to a range of ideas. A core insight of our proposal is that we do not need any form of equality reflection in order to achieve what HTS was suggested for. Instead, having unique identity proofs in the outer type theory is sufficient, and it also has the meta-theoretical advantage of not breaking decidability of type checking. The inner theory can be an easily justifiable extensions of HoTT, allowing the construction of ``infinite structures'' which are considered impossible in plain HoTT. Alternatively, we can set the inner theory to be exactly the current standard formulation of HoTT, in which case our system can be thought of as a type-theoretic framework for working with ``schematic'' definitions in HoTT. As demonstrations, we define semi-simplicial types and formalise constructions of Reedy fibrant diagrams.
机译:在同伦类型理论(HoTT)中,所有结构在同伦对等下必定是稳定的。这有缺点:例如,据信不可能定义半简单类型的类型。更普遍地讲,处理连贯性的塔很困难,而且常常是不可能的。为了解决这个问题,我们提出了一个具有严格和弱相等性的两层理论。从本质上讲,这可以表示为两种类型理论:``外部''理论包含严格的等式类型前者,而``内部''理论则是HoTT的某种形式。我们的类型理论是受Voevodsky提出的同构类型系统(HTS)的建议启发的,该系统目前涉及一系列思想。我们的建议的核心见解是,我们不需要任何形式的平等反思就可以实现建议的HTS。相反,在外部类型理论中具有唯一的身份证明就足够了,并且它还具有不破坏类型检查的可决定性的元理论优势。内部理论可以是HoTT的一个很容易证明的扩展,允许构造``无限结构'',这在普通HoTT中是不可能的。或者,我们可以将内部理论设置为HoTT的当前标准表述,在这种情况下,我们的系统可以被认为是用于处理HoTT中``示意图''定义的类型理论框架。作为演示,我们定义半简单类型并形式化Reedy纤维图的构造。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号