Type theory in type theory using quotient inductive types
Type theory in type theory using quotient inductive types
复制标题
DOI：
10.1145/2837614.2837638
复制
发表时间：
2016-01
期刊：
影响因子：
--
通讯作者：
Thorsten Altenkirch;A. Kaposi
中科院分区：
文献类型：
--
作者：
Thorsten Altenkirch;A. Kaposi
我们使用类型理论中具有依赖类型的类型发言的内部形式化，使用同型类型理论的较高归纳类型的特殊情况，我们称之为商归纳类型（QITS）。我们对类型理论的形式化避免了提及早产或特异性关系，但通过归纳定义直接定义了典型的对象。我们使用消除原理来定义集合理论和逻辑谓语解释。使用AGDA系统使用QITS使用假设进行了正式化。
We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.