逻辑系统I：通过离散性的Lambda演算
Logical systems I: Lambda calculi through discreteness
摘要：
本文展示了多态lambda演算的内模是如何在任何具有离散性概念的2-范畴中产生的。我们推广到一个2-范畴设置著名的定理彼得Freyd说，有没有充分（共）完整的非退化范畴。作为一个简单的推论，我们得到了Freyd定理的一个变种，范畴内部的任何张量范畴。此外，借助相关范畴的概念，我们证明了一个表示定理，我们的内模与研究良好的纤维模型多态性。
英文摘要：
This paper shows how internal models for polymorphic lambda calculi arise in any 2-category with a notion of discreteness. We generalise to a 2-categorical setting the famous theorem of Peter Freyd saying that there are no sufficiently (co)complete non-degenerate categories. As a simple corollary, we obtain a variant of Freyd theorem for categories internal to any tensored category. Also, with help of introduced concept of an associated category, we prove a representation theorem relating our internal models with well-studied fibrational models for polymorphism.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
