平凡化高阶索引族的两种技巧
计算机科学中的逻辑
2023-10-31 v2
摘要
依赖类型论中索引族的常规通用语法遵循“构造子返回特例”的风格，如 Agda、Lean、Idris、Coq 以及可能许多其他系统所示。Fording 是一种用无索引归纳类型与恒等类型来编码此种风格索引族的方法。另有一种技巧可将交错的高阶归纳-归纳类型合并为单一的大型类型族。它利用一个小宇宙作为索引以区分原有类型。在本文中，我们展示这两种方法可以平凡化某些看似非常花哨的带高阶归纳索引的索引族（我们称之为高阶索引族）。
引用
@article{arxiv.2309.14187,
title = {Two tricks to trivialize higher-indexed families},
author = {Tesla Zhang},
journal= {arXiv preprint arXiv:2309.14187},
year = {2023}
}
备注
9 pages