Semi-simplicial Types in Logic-enriched Homotopy Type Theory
Semi-simplicial Types in Logic-enriched Homotopy Type Theory
复制标题
逻辑丰富的同伦类型理论中的半单纯类型
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Zhaohui Luo
中科院分区：
文献类型：
--
作者：
Fedor Part;Zhaohui Luo
同伦类型论（HoTT）中定义半单纯型（SST）的问题在高等研究所的单价基础年中被认为是重要的。根据HoTT在Quillen模型范畴中的解释，SST是模型范畴中Reedy非单半单纯对象的类型论版本，单纯和半单纯对象在同伦理论和高级范畴理论中的许多构造中起着至关重要的作用。试图定义SST在HoTT导致一些困难，如需要无限的假设，这是超越HoTT只有非严格的平等类型。
Voevodsky在同伦类型系统（HTS）中提出了SST的定义，HTS是HoTT的一个扩展，包含了一个扩展的严格相等类型。然而，HTS不具有理想的计算属性，例如类型检查的可判定性和强规范化。在本文中，我们研究了逻辑丰富的同伦类型理论，一个替代的HoTT扩展与方程逻辑的逻辑丰富的类型理论的思想的基础上。与Voevodskys的HTS相比，我们系统中的所有类型都是并行的，并且可以在现有的证明助手中实现。我们将展示如何在我们的系统中定义SST，并概述了在证明助手塑料中的实现。
The problem of defining Semi-Simplicial Types (SSTs) in Homotopy Type Theory (HoTT) has been recognized as important during the Year of Univalent Foundations at the Institute of Advanced Study. According to the interpretation of HoTT in Quillen model categories, SSTs are type-theoretic versions of Reedy fibrant semi-simplicial objects in a model category and simplicial and semi-simplicial objects play a crucial role in many constructions in homotopy theory and higher category theory. Attempts to define SSTs in HoTT lead to some difficulties such as the need of infinitary assumptions which are beyond HoTT with only non-strict equality types.
Voevodsky proposed a definition of SSTs in Homotopy Type System (HTS), an extension of HoTT with non-fibrant types, including an extensional strict equality type. However, HTS does not have the desirable computational properties such as decidability of type checking and strong normalization. In this paper, we study a logic-enriched homotopy type theory, an alternative extension of HoTT with equational logic based on the idea of logic-enriched type theories. In contrast to Voevodskys HTS, all types in our system are fibrant and it can be implemented in existing proof assistants. We show how SSTs can be defined in our system and outline an implementation in the proof assistant Plastic.