一个对小型族类通用的归纳-递归宇宙
计算机科学中的逻辑
2022-02-14 v1
摘要
我们证明了在所有 Grothendieck 拓扑斯中，可以构造一个具有 Pujet 与 Tabareau 式内射码的宇宙，且该宇宙对小型族类仍然是通用的。作为一个平凡推论，我们证明了他们的观察类型论允许在 Grothendieck 拓扑斯中得到适合作为内语言的解释。
引用
@article{arxiv.2202.05529,
title = {An inductive-recursive universe generic for small families},
author = {Daniel Gratzer},
journal= {arXiv preprint arXiv:2202.05529},
year = {2022}
}