使用非递归HITs构造命题截断
逻辑
2015-12-09 v1
摘要
在同伦类型论中，我们仅使用非递归高阶归纳类型（HITs）将命题截断构造为一个余极限。这是将递归HITs归约为非递归HITs的第一步。该构造给出了从命题截断到任意类型的函数的刻画，扩展了命题截断的泛性质。我们已在一个新证明助手Lean中完全形式化了所有结果。
引用
@article{arxiv.1512.02274,
title = {Constructing the Propositional Truncation using Non-recursive HITs},
author = {Floris van Doorn},
journal= {arXiv preprint arXiv:1512.02274},
year = {2015}
}
备注
8 pages, Certified Programs and Proofs 2016