• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory
【24h】

A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory

机译：同态型理论中的Blakes-Massey连通性定理的机械化

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper contributes to recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory. We present a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.
机译：本文为利用同伦类型理论的最新研究做出了贡献，以从同伦理论提供机器检验的构造证明。我们提出了一个名为Blakers-Massey连接性定理的结果的机械化证明，该定理将共享同一部分（以推出类型表示，这是不相交和类型的泛化）的两个空间的高维循环结构联系起来。共同部分本身。该定理提供有关推出类型的重要信息，并具有许多有用的推论，包括先前形式化中使用的Freudenthal悬浮定理。该证明比同态理论的一般类别理论环境中已有的证明更直接，并且由于同态理论和类型理论的新颖思想结合，其机械化简洁而高级。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号