带族范畴：单类型、简单类型与依赖类型
计算机科学中的逻辑
2020-07-08 v2
摘要
我们展示了无类型、简单类型和依赖类型 lambda 演算的范畴逻辑如何围绕带族范畴（cwf）这一概念来构造。为此，我们引入简单类型 cwf（scwf，其中类型不依赖于变量）的子范畴，以及单类型 cwf（ucwf，其中仅有一个类型）。我们证明了若干基于 cwf 的概念与范畴逻辑基本概念（如笛卡儿算子、Lawvere 理论、具有有限积与极限的范畴、笛卡儿闭范畴和局部笛卡儿闭范畴）之间的等价与双等价定理。其中部分定理依赖于上下文性（Cartmell 意义下）或民主性（Clairambault 与 Dybjer 用于其双等价定理）的限制。一些定理是在严格保持所选结构意义上的等价。另一些是仅在性质保持到同构意义上的双等价。此外，我们讨论了具有额外结构的初始 ucwf、scwf 和 cwf 的各种构造。
引用
@article{arxiv.1904.00827,
title = {Categories with Families: Unityped, Simply Typed, and Dependently Typed},
author = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
journal= {arXiv preprint arXiv:1904.00827},
year = {2020}
}