立方 Agda 中三个等价的序数记号系统
逻辑
2020-05-06 v2
摘要
我们利用互归纳-归纳定义和高阶归纳类型等近期类型论创新，给出了类型论中表示 以下序数的三个序数记号系统。我们展示了如何为这些系统发展序数算术，以及它们如何容许超限归纳原理。我们证明所有三个记号系统都是等价的，从而可利用 univalence 原理在它们之间传输结果。我们所有的构造都已在立方 Agda 中实现。
引用
@article{arxiv.1904.10759,
title = {Three Equivalent Ordinal Notation Systems in Cubical Agda},
author = {Fredrik Nordvall Forsberg and Chuangjie Xu and Neil Ghani},
journal= {arXiv preprint arXiv:1904.10759},
year = {2020}
}
备注
14 pages, to appear at CPP 2020