Homotopy theoretic models of identity types
Steve Awodey, Michael A. Warren
本文提出了同伦代数与数理逻辑之间的一种新的联系。证明了一种形式的内涵类型理论在任何Quillen模型范畴中都是有效的，推广了Martin-Loef类型理论的Hofmann-Streicher广群模型。
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Topological and simplicial models of identity types
本文在拓扑空间的Top范畴和单纯集的SSet范畴中，构造了Martin-Löf型理论的恒等式的新范畴模型.我们这样做的基础上，早期的工作Awodey和沃伦，这表明，一个合适的环境，解释身份类型应该是一个类别配备了一个弱因子分解系统的意义上的Bousfield-Quillen。事实证明，这对于一个健全的模型是不够的，因为一些微妙的连贯性问题与替换下的稳定性有关;因此，我们的第一个任务是引入一个稍微丰富的结构--我们称之为同伦理论模型的身份类型--并证明这对于一个健全的解释是足够的。现在，虽然Top和SSet都是具有弱因子分解系统的范畴-事实上，整个Quillen模型结构-展示同伦理论模型所需的额外结构是很难做到的。然而，我们感兴趣的类别有许多共同的特征，从这些特征中抽象出来，我们引入了路径对象类别的概念。这是一个相对简单的公理化框架，但它足够强大，允许同伦理论模型的建设。通过在Top和SSet上展示合适的路径对象结构，我们赋予这些范畴同伦模型的结构，从而得到所需的恒等式的拓扑模型和单纯模型.
Path categories and propositional identity types
同伦理论和类型理论之间的联系最近吸引了很多关注，Voevodsky的单价基础和马丁-洛夫的单位元类型在奎伦模型范畴中的解释是其中的亮点。在本文中，我们建立了一个自然的削弱马丁-洛夫的规则之间的联系的身份类型已被科恩，Coquand，Huber和Mortberg在他们的工作中考虑的一个建设性的解释，一方面，和一个道路范畴的概念，一个轻微的变化的经典概念的范畴的不确定性对象由于布朗。这涉及到表明，与弱身份类型的类型理论的句法类别进行结构的路径类别，加强早期的结果由Avigad，Lumsdaine和Kobrkin。通过这种方式，我们不仅将同伦理论中的一个著名概念与逻辑中的一个自然概念联系起来，而且还为进一步的发展提供了一个框架。
The identity type weak factorisation system
我们证明了具有单位型公理的依赖型理论T的分类范畴C（T）允许一个非平凡的弱因子分解系统。我们提供了一个明确的特征的元素的左类和右类的弱因子分解系统。这一特征被应用于关系单位类型和同伦理论的群胚。
On a model invariance problem in Homotopy Type Theory
本文利用内射模型结构赋予函子范畴[B（Z ~ 2），Gpd]一个具有单叶论域的类型论纤维化范畴的结构.它给我们一个新的模型的马丁-洛夫型理论与相关的总和，相关的产品，单位类型和一个单叶宇宙。这个模型，连同作者在另一部著作中发展的模型，在同一个基本范畴中，连同同一个宇宙，就投射纤维化而言，被证明不是单价的，提供了两个奎伦等价模型范畴的一个例子，它们承载着不同的类型论模型。因此，我们提供了一个反例的模型不变性问题制定的迈克尔舒尔曼。
Natural models of homotopy type theory
类型论的自然模型的概念是根据预层的可表示的自然拟序来定义的。结果表明，这种模型完全符合Dybjer意义下的族范畴的概念，它可以被看作是一个代数形式的类型论。我们确定这样的模型的条件，以满足推理规则的依赖和，依赖产品，和内涵的身份类型，在同伦类型理论中使用。然后，它表明，一个类别承认这样的模型，如果它有一类映射，表现得像抽象的纤维化在公理同伦理论：他们应该是稳定的拉回下，封闭的组合和相关产品，并应有弱正交分解到类。因此，同伦理论的许多熟悉的设置也承认同伦类型理论的基本系统的自然模型。
Higher Groups in Homotopy Type Theory
本文在同伦类型论中发展了高阶群理论，包括无穷群和联结谱。无穷群只是一个指向的连通类型中的环，其中群结构来自马丁-洛夫类型论的单位类型中固有的结构。我们从这个角度研究普通的群体，以及高维群体和群体，可以不止一次地去圈。一个主要的结果是稳定性定理，它指出，如果一个$n$型可以去环$n+2$倍，那么它是一个无限循环类型。大部分结果已经在精益证明助手中正式化。
Homotopy-initial algebras in type theory
我们研究归纳类型的类型理论，使用同伦类型理论和数学的单价数学基础提供的见解。我们这样做是通过引入同伦初始代数的新概念。这个概念是由一个纯粹的类型理论的可压缩性条件，取代了标准的，范畴理论的泛性质，涉及适当的态射的存在性和唯一性。我们的主要结果刻画了与W-型等价的同伦初始代数的类型。
Homotopy Theoretic Models of Type Theory
我们引入了逻辑模型范畴的概念，它是一个Quillen模型范畴满足一些附加条件。这些条件提供了足够的表达能力，可以很好地解释其中的相关乘积和和，另一方面，这些条件易于检验，并提供了广泛的模型，其中一些在本文中列出。
Internal Languages of Finitely Complete $(\infty, 1)$-categories
我们证明了Joyal族的同伦理论与纤维化范畴的同伦理论是等价的。作为结果，我们推导出一个变体的猜想断言，马丁-洛夫类型理论与依赖和和内涵单位类型是内部语言的$(\infty, 1)$ -范畴有限限制。
Classifying Types
在类型论的语言中，同伦理论现象的研究有时被称为“合成同伦理论”。同伦类型论中的同伦理论只是同伦类型论的众多方面之一，同伦类型论还包括集合论语义的研究（同伦类型论模型和集合或范畴的元理论中的单值性），类型论语义学（同伦类型理论的内模）和计算语义学，以及研究同伦类型理论内部语言中的各种问题，这些问题不一定是由同伦理论激发的，或与基于同伦类型理论的形式化数学库的发展相关的问题。本论文是关于综合同伦理论的发展。
Homotopy type theory: the logic of space
这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍，作为《数学和物理的新空间》（Gabriel Catren和Mathieu Anel编）一书的一章。
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
本文在同伦类型理论中构建了非良基础集模型，提出扩展AFA和SAFA的通用化，并通过M型构建了满足SAFA通用化的层级模型，同时刻画了M型的身份类型。
Exercices de style: a homotopy theory for set theory, I
我们从两个任意但自然的约定出发，为集合论构建了一个模型范畴（在奎伦的意义上）。它是最简单的范畴，满足我们的约定，并模拟有限性，可数性和无限等势的概念。在随后的文件\cite{GaHa1}我们给出了同伦理论字典集理论的概念，最显着的谢拉的覆盖数$\cov(λ, \aleph_1,\aleph_1,2)$，恢复从这个模型类别。我们认为，从同伦理论的角度来看，我们的建设基本上是自动遵循现有的基本方法，所以是（几乎所有）的建设工程的验证。
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
最近的工作同伦类型理论利用了一个令人兴奋的新的对应马丁-洛夫的依赖型理论和数学学科的范畴论和同伦理论。范畴论和同伦理论提出了新的原则，以增加类型论，类型论可以用新的方式来形式化这些数学领域。本文给出了代数拓扑学中的一个基本结果：圆的基本群是整数。虽然简单，这个例子是有趣的几个原因：它说明了同伦类型论的新原则;它混合了传统同伦理论证明的结果与类型理论归纳推理的想法;它提供了一个上下文来理解现有的类型理论难题-一个宇宙（类型）是必要的，以证明归纳类型的构造函数是不相交的和单射的。
The Fullness Axiom and exact completion of homotopy categories
我们使用的范畴理论制定的Aczel的充满性公理从建设性集合论，以获得当地carnival封闭的一个确切的完成。作为应用，我们证明了这样一个公式在满足温和要求的任何模型范畴的同伦范畴中都是有效的，从而特别得到了拓扑空间和同伦映射类的精确完备的局部Carnival闭包.根据类型理论的阅读，这些结果提供了一个一般的动机，当地carless-closure类setoids。然而，结果和证明仅仅是用范畴的语言来表述的，读者不需要类型论或构造性集合论的知识。
Homotopy limits in type theory
工作在同伦类型理论，我们提供了一个系统的研究同伦极限的图，形式化的Coq证明助手。我们讨论了这种方法形式化同伦理论材料所带来的一些挑战。我们还比较了我们的建设与更经典的方法，通过纤维化类同伦极限。
Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence
在本文中，基于以前的工作（第一部分），我们提出了一个游戏语义的内涵变体的直觉类型论，反驳了唯一性的原则，身份证明和验证的univalence公理，虽然我们不解释非平凡的高等命题等式。具体来说，根据霍夫曼和Streicher的历史广群解释，我们配备了一个广群结构的第一部分中的谓词游戏，这引起了（谓词）gamoid的概念。粗略地说，gamoids是“指定（计算）等式的游戏”，它解释了ID类型中的微妙之处。然后，我们制定了一个类别的家庭的预测gamoid，配备了依赖产品，依赖和，ID类型以及宇宙，这形成了一个具体的实例的广群模型。我们相信，这项工作是一个重要的垫脚石走向一个完整的解释同伦类型论。
A category-theoretic version of the identity type weak factorization system
Gambino和Garner证明了具有单位类型的依赖类型理论的句法范畴可以被赋予一个弱分解系统结构，称为单位类型弱分解系统。在本文中，我们考虑了丰富的Joyal的部落的概念，我们称之为部落与弱稳定的道路对象，并证明了一个纯粹的范畴论版本的单位型弱因子分解系统，从而推广Gambino和加纳的结果。我们的结论表明，这种结构也包含弱因子分解系统来自的拓扑和单纯模型的身份类型由van den Berg和加纳。
Non-Standard Models of Homotopy Type Theory
本文提出 filter quotient construction 作为构建同伦类型论新模型的方法，证明其在保留类型论构造子和公理的模型范畴性质的同时不保留集合论外部性质，从而产生具有新行为的非标准模型。
From Multisets to Sets in Hotmotopy Type Theory
基于同伦类型论中的多重集，给出了一个集合论模型。模型的平等性是身份类型。迭代集的基本类型可以在马丁-洛夫类型理论中表述，没有更高的归纳类型（HIT），并且是类型论中集合论的Aczel 1978模型的基本类型的子类型。Voevodsky的Univalence公理和纯粹的集合等价性（一种温和的HIT）被用来证明该模型的构造性集合论的公理。我们给出了一个等价的模型在第10章中提供的同伦型理论的单价基础计划。
Homotopy type theory and Voevodsky's univalent foundations
最近的发现已经取得了连接抽象同伦理论和领域的类型理论从逻辑和理论计算机科学。这就产生了一个新的领域，它被命名为“同伦型理论”。在这个方向上，弗拉基米尔·沃沃茨基观察到，可以用单纯集来建模类型论，并且这个模型满足一个额外的属性，称为单价公理，它有许多惊人的结果。他随后提出了一个计划，他称之为单价基础，在类型论的背景下发展数学，其中包含单价公理和其他可能的公理，这些公理是由单纯集模型激发的。由于类型论具有良好的计算性质，该程序可在计算机辅助下进行。在本文中，我们给同伦类型理论在Voevodsky的设置，注意理论和实践问题的介绍。特别是，该文件作为一个介绍的一般思想同伦类型理论以及一些具体细节Voevodsky的工作使用著名的证明助手Coq。这篇论文是为具有代数拓扑学基础知识的普通数学家编写的;本文不假设任何类型论、逻辑或计算机科学的初步知识。
Higher Inductive Types as Homotopy-Initial Algebras
同伦类型论是基于马丁-洛夫构造性类型论和抽象同伦理论之间令人惊讶的和优雅的对应关系的一个新的数学领域。我们在这些学科之间有着强大的相互作用--我们可以使用几何直观来表述类型论中的新概念，相反，我们可以使用类型论的机器来验证并经常简化现有的数学证明。这个新系统中的一个关键成分是更高的归纳类型，它允许我们表示诸如球体、环面、推出物和平行物之类的对象。我们研究了一种高阶归纳类型的变体，它的计算行为取决于一个高阶路径，我们证明了在这种情况下，高阶归纳类型的特征在于它是一个同伦初始代数的泛性质.
The equivalence of the torus and the product of two circles in homotopy type theory
同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。
An Implementation of Homotopy Type Theory in Isabelle/Pure
在这篇硕士论文中，我们提出了一个实现的片段“书HoTT”作为一个对象逻辑的交互式证明助手伊莎贝尔。我们还给出了一个数学描述的基础理论的伊莎贝尔/纯逻辑框架，并讨论了各种问题和设计决策时，试图编码内涵依赖类型论与宇宙内一个简单的类型理论的逻辑基础。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。