一句话：提出 HIIT 签名的类型理论，统一描述高阶归纳-归纳类型，并通过语法逻辑关系翻译计算归纳/递归原理。
高阶归纳-归纳类型（HIITs）同时推广依赖类型理论中的归纳类型与同伦类型论中的高阶归纳类型：既可相互索引地同时定义多个 sort，又允许相等构造子；Cauchy 实数与带转换规则的良类型语法是其典型例子。本文提出一种小型类型理论“签名理论”，用上下文列出构造子来编码 HIIT，从而给出 HIIT 的一般定义。作者借助句法逻辑关系翻译的变体，计算 HIIT 的归纳与递归原理；范畴语义与初始代数留待未来。该签名理论及句法翻译已在 Agda 中形式化，并提供 Haskell 实现，可将签名翻译为合法 Agda 代码。
Higher inductive-inductive types (HIITs) generalize inductive types of dependent type theories in two ways. On the one hand they allow the simultaneous definition of multiple sorts that can be indexed over each other. On the other hand they support equality constructors, thus generalizing higher inductive types of homotopy type theory. Examples that make use of both features are the Cauchy real numbers and the well-typed syntax of type theory where conversion rules are given as equality constructors. In this paper we propose a general definition of HIITs using a small type theory, named the theory of signatures. A context in this theory encodes a HIIT by listing the constructors. We also compute notions of induction and recursion for HIITs, by using variants of syntactic logical relation translations. Building full categorical semantics and constructing initial algebras is left for future work. The theory of HIIT signatures was formalised in Agda together with the syntactic translations. We also provide a Haskell implementation, which takes signatures as input and outputs translation results as valid Agda code.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{KaposiK19,
title = {Signatures and Induction Principles for Higher Inductive-Inductive Types},
author = {Ambrus Kaposi and András Kovács},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 1},
year = {2020},
doi = {10.23638/lmcs-16(1:10)2020}
}