首页> 外文会议>Typed lambda calculi and applications >The Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theories
【24h】

The Biequivalence of Locally Cartesian Closed Categories and Martin-Lof Type Theories

机译:局部笛卡尔封闭类别与马丁-洛夫类型理论的双等价性

获取原文
获取原文并翻译 | 示例

摘要

Seely's paper Locally cartesian closed categories and type theory contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-L6f type theories with 77, ∑, and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Benabou-Hofmann interpretation of Martin-Loef type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development we employ categories with families as a substitute for syntactic Martin-Loef type theories. As a second result we prove that if we remove 77-types the resulting categories with families are biequivalent to left exact categories.
机译:Seely的论文局部笛卡尔封闭类别和类型理论在分类类型理论中包含一个众所周知的结果:局部笛卡尔封闭类别的类别等于具有77,∑和扩展标识类型的Martin-L6f类型理论的类别。但是,Seely的证明基于一个有问题的假设,即类型的替换可以通过回调来解释。在这里,我们证明Seely定理的更正形式:Benabou-Hofmann在局部笛卡尔封闭类别中对Martin-Loef类型理论的解释产生2类双重等价性。为了促进技术发展,我们采用带有家族的类别来替代句法式马丁·洛夫类型理论。作为第二个结果,我们证明了,如果删除77个类型,则带有族的结果类别等同于剩余的确切类别。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号