内部代数类型理论
Internal Algebraic Type Theory
浏览论文内容
中文总结 AI 辅助
本论文将计算机辅助的内部类型论推理应用于范畴，以立方集等范畴为例，推进类型论分析并实现HoTTLean项目相关推理，通过新指数可实现条件与多项式函子拓展代数类型理论的适用范围。
中文摘要 AI 辅助
本论文让我们更接近将计算机辅助的、内部的、类型论的推理应用于范畴，具体例子包括立方集范畴、群胚范畴和范畴范畴。我们朝着这一总体目标推进的步骤，既包括对这些例子的类型论分析的深入，也包括将计算机辅助的句法-语义推理作为HoTTLean项目的一部分来实现。这项工作的一个关键组成部分是考虑关于范畴中一类映射的新的指数可实现条件，并为这类映射开发多项式函子，使得“代数类型理论”的方法能在这一非常一般的语境中得以应用。
英文摘要
This thesis brings us closer to applying computer-assisted, internal, type-theoretic reasoning to a category, with examples in the category of cubical sets, the category of groupoids, and the category of categories. The steps we make towards this general goal are both in furthering the type theoretic analysis of these examples, as well as implementing computer-assisted syntax-semantic reasoning as part of the HoTTLean project. One key component of this work is the consideration of new exponentiability conditions with respect to a class of maps in a category, and the development of polynomial functors for these maps, making the methods of "algebraic type theory" possible in this very general setting.
