Relating set theories and type theories via categorical logic

通过分类逻辑将集合论和类型论联系起来

• 批准号: 2438979
• 金额: --
• 依托单位: University of Leeds
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2438979
• 关键词: Relating; set; theories; type; via

Ever since the fundamental work of Aczel in the '60s, the study of the relationship between constructive set theories and constructive type theories has been a very important topic of research. Further impetus in this area has been given by the recent development of Homotopy Type Theory. The aim of this project is to develop further categorical logic so as to provide a unified account of the plethora of type-theoretic interpretations of constructive set theories, thereby providing a clear understanding of their relationship. This will require significant and challenging technical work in extending the framework of Algebraic Set Theory to allow for interpretations of logic other than the standard propositions-as-subobjects one, in order to encompass some examples of type-theoretic interpretations of set theories that use the propositions-as-types or propositions-as-h-props paradigms. Potential applications include the creation of new models of constructive set theories by considering examples in known categorical models of type theory (groupoids, simplicial sets). These may lead to new applications to relative consistency and independence results.

自从Aczel在60年代的基础工作以来，构造性集合论和构造性类型理论之间关系的研究一直是一个非常重要的研究课题。同伦类型理论的最新发展进一步推动了这一领域的发展。该项目的目的是发展进一步的范畴逻辑，以便为构造性集合论的过多类型论解释提供统一的解释，从而提供对它们之间关系的清晰理解。这将需要在扩展代数集合论框架方面进行重大且具有挑战性的技术工作，以允许对标准命题作为子对象之外的逻辑进行解释，以便涵盖使用集合论的类型论解释的一些示例命题作为类型或命题作为 h-props 范式。潜在的应用包括通过考虑类型论的已知分类模型（群群、单纯集）中的示例来创建构造性集合论的新模型。这些可能会导致新的应用程序获得相对一致性和独立性的结果。