与布尔巴基结构与同构概念相关的依赖类型论
计算机科学中的逻辑
2021-04-20 v1
摘要
本文发展了一个版本的依赖类型论，其中同构通过直接推广布尔巴基（Bourbaki）1939年的定义来处理。更具体地说，我们将布尔巴基的结构定义从简单类型签名推广到依赖类型签名。无论是原始的布尔巴基同构概念还是此处给出的推广，都将两个结构 与 之间的同构定义为它们排序之间的双射，这些双射将 的结构迁移为 的结构。此处迁移由以集合论等式表述的交换条件定义。这不同于群oid模型与同伦类型论中给出的依赖类型论同构处理，后者未指定类似直白的集合论迁移定义。这一直白的迁移定义也带来了关于同构可替换性成立性的直白构造性证明（构造内容）——这在群oid模型或同伦类型论中是困难的。
引用
@article{arxiv.2104.08958,
title = {Dependent Type Theory as Related to the Bourbaki Notions of Structure and Isomorphism},
author = {David McAllester},
journal= {arXiv preprint arXiv:2104.08958},
year = {2021}
}