Models of Homotopy Type Theory with an Interval Type
Valery Isaev
在这篇短文中，我们构造了同伦类型论的一类推广模型，我们称之为具有区间类型的同伦类型论。
In this short note, we construct a class of models of an extension of homotopy type theory, which we call homotopy type theory with an interval type.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Internal Universes in Models of Homotopy Type Theory
首先，我们回顾了同伦类型论的各种模型中宇宙的基本全局性质，这防止了使用这些模型构建的预层拓扑的内部语言对其属性进行直接的公理化。我们通过扩展内部语言来解决这个问题，使用模态运算符来表达全局元素的属性。在这种情况下，我们展示了如何从三次集合模型出发，从区间很小的假设出发，构造一个对科恩-科坎德-胡贝尔-默特伯格（CCHM）的纤维化概念进行分类的宇宙--三次集合中的区间确实具有这种性质。这就导致了同伦类型论的基本公理化，我们称之为清晰类型论。
A homotopy-theoretic model of function extensionality in the effective topos
我们提出了一种方法来构建一个Quillen模型结构上的一个完整的子范畴的基本topos，开始与连接和一定的优势区间对象。这种方法的优点是它不需要底层拓扑是共完备的。由此产生的模型类别结构产生了同伦类型论的模型与身份类型，$Σ$ -和$Π$ -类型，和功能的可拓性。我们将该方法应用于具有区间对象$\nabla 2$的有效拓扑。在由此产生的模型结构中，我们确定均匀居住的对象作为可收缩的对象，并表明离散对象是不连续的。此外，我们还证明了离散反射的单位是同伦等价的，并且同伦集合范畴等价于适度集合范畴。我们比较了我们的工作与路径对象类别建设的有效topos的雅普范Oosten。
Homotopy Type Theory in Isabelle
本文介绍了Isabelle/HoTT，同伦类型论的第一个发展Isabelle证明助手。在Paulson早期工作的基础上，我使用Isabelle现有的逻辑框架基础设施来实现基本的自动化，例如类型检查和术语细化，这通常是在依赖类型系统的源代码级别上处理的。我还集成了命题作为类型的范式与声明性的Isar证明语言，提供了一种替代的Coq和Agda的证明条款的基于策略的证明。基础设施开发，然后用于形式化的同伦类型论书的基础结果。
Semi-simplicial Types in Logic-enriched Homotopy Type Theory
同伦类型论（HoTT）中定义半单纯类型（SST）的问题在高等研究院的单价基础年中被认为是重要的。根据HoTT在Quillen模型范畴中的解释，SST是模型范畴中Reedy非单半单纯对象的类型论版本，单纯和半单纯对象在同伦理论和高级范畴理论中的许多构造中起着至关重要的作用。试图定义SST在HoTT导致一些困难，如需要无限的假设，这是超越HoTT只有非严格的平等类型。Voevodsky在同伦类型系统（HTS）中提出了SST的定义，HTS是HoTT的一个扩展，包含了一个扩展的严格相等类型。然而，HTS不具有所需的计算属性，如类型检查和强规范化的可判定性。在本文中，我们研究了逻辑丰富的同伦类型论，一个可选的扩展HoTT与方程逻辑的逻辑丰富的类型论的想法的基础上。与Voevodskys的HTS相比，我们系统中的所有类型都是并行的，并且可以在现有的证明助手中实现。我们将展示如何SST可以在我们的系统中定义，并概述了在证明助手塑料的实施。
Synthetic Homology in Homotopy Type Theory
本文在同伦类型论中定义了同调，并在此过程中定义了稳定同伦群。合成同伦理论的研究依赖于以前的研究，特别是上同调的定义。这一工作为计算机检验同调结构奠定了基础。
The equivalence of the torus and the product of two circles in homotopy type theory
同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。
Homotopy Type Theory in Lean
我们在精益证明助手中讨论同伦类型论库。该图书馆特别面向合成同伦理论。特别令人感兴趣的是使用了一些高级归纳类型的原始概念，即截断和截断，以及立方方法的使用。
The HoTT Library: A formalization of homotopy type theory in Coq
我们报告的HoTT库的发展，同伦类型论的形式化Coq证明助手。它形式化了大多数基本的同伦类型论，包括单值性、高级归纳类型、大量的综合同伦理论，以及范畴论和模态。该图书馆已被用作几个独立开发的基础。我们讨论的决定，导致图书馆的设计，我们评论同伦类型论的相互作用与最近推出的功能Coq，如宇宙多态性和私人归纳类型。
A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory
本文继续调查“合成同伦理论”：使用同伦类型论给机器检查证明的建设从同伦理论我们提出了一个机械化的证明的布莱克斯-梅西连通性定理，一个结果有关高维同伦群的推出型（粗略地说，一个空间构造的两个空间沿一个共享子空间）的组件推出。这个定理给出了关于推出型的重要信息，并有许多有用的推论，包括弗赖登塔尔悬置定理，它在以前的形式化中已经研究过。新的证明比现有的抽象同伦理论设置更基本，机械化是简洁和高层次的，这要归功于同伦理论和类型论思想的新颖组合。
Non-wellfounded trees in Homotopy Type Theory
我们证明了同伦类型论中关于共归纳类型的可构造性的一个猜想--以索引M-类型的原则形式。该猜想说，在归纳类型存在的情况下，共归纳类型是可导出的。事实上，在这项工作中，我们在同伦类型论的一个子系统中构造了共归纳类型;这个子系统由内涵马丁-洛夫类型论与自然数和Voevodsky的单价公理给出。我们的结果在计算机证明助手Agda中实现了机械化。
Towards a directed homotopy type theory
在本文中，我们提出了一个有向同伦类型论综合推理（高）类，有向同伦理论，及其应用并发。我们指定一个新的“同态”型前的马丁-洛夫类型论，这是大致类似的身份型前最初介绍的马丁-洛夫。同态类型形成器是用来捕捉态射（来自范畴理论）和有向路径（来自有向同伦理论）的概念，就像单位类型形成器是用来捕捉同构（来自群胚理论）和路径（来自同伦理论）的概念一样。我们的主要结果是这些同态类型的猫，范畴的小范畴的解释。在那里，每个同态类型hom（a，b）的解释确实是范畴C的对象a和b之间的态射集合。最后，我们分析了猫的解释，我们认为，我们的同态类型确实是有向版本的马丁-洛夫的身份类型。
Homotopy limits in type theory
工作在同伦类型理论，我们提供了一个系统的研究同伦极限的图，形式化的Coq证明助手。我们讨论了这种方法形式化同伦理论材料所带来的一些挑战。我们还比较了我们的建设与更经典的方法，通过纤维化类同伦极限。
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
本论文的目的是在同伦型理论的背景下提出综合同伦理论。我们将提出各种结果在这个框架中，最值得注意的是建设的Atiyah-Hirzebruch和塞尔谱序列的上同调，已完全正式的精益证明助手。
Classifying covering types in homotopy type theory
本文在同伦型理论中形式化了覆盖空间与基本群子群的对应关系，发展了n维覆盖空间的泛化，并通过分类棱镜空间的覆盖来展示方法的应用，解释了如何构造庞加莱紧致球面。
The Cayley-Dickson Construction in Homotopy Type Theory
本文在同伦类型论的背景下定义了$\mathbb S^3$上的H-空间结构。因此，我们得到的四元数的Hopf纤维化$\mathbb S^3\hookrightarrow\mathbb S^7\twoheadrightarrow\mathbb S^4$的描述，只使用同伦不变量的工具。
Higher Inductive Types as Homotopy-Initial Algebras
同伦类型论是基于马丁-洛夫构造性类型论和抽象同伦理论之间令人惊讶的和优雅的对应关系的一个新的数学领域。我们在这些学科之间有着强大的相互作用--我们可以使用几何直观来表述类型论中的新概念，相反，我们可以使用类型论的机器来验证并经常简化现有的数学证明。这个新系统中的一个关键成分是更高的归纳类型，它允许我们表示诸如球体、环面、推出物和平行物之类的对象。我们研究了一种高阶归纳类型的变体，它的计算行为取决于一个高阶路径，我们证明了在这种情况下，高阶归纳类型的特征在于它是一个同伦初始代数的泛性质.
Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
我们在同伦类型论的形式语言中实现了一组新的公理，称为凝聚力。然后，我们指出如何产生的凝聚同伦型理论自然作为一个正式的基础，在量子规范场理论的中心概念。这是作者在其他地方详细发展的工作的简要调查。
Homotopy type theory as a language for diagrams of $\infty$-logoses
论文展示通过扩展同伦类型论加入某些lex可及模态量，可将∞-逻辑格的图示重构，从而用普通同伦类型论处理单个或多个∞-逻辑格。
Relating homotopy equivalences to conservativity in dependent type theories with computation axioms
本文借助同伦类型理论与带属性范畴，通过上下文间典范同伦等价证明外延类型理论对带命题计算公理的依赖类型理论具有保守性。
Inductive types in homotopy type theory
同伦类型论（英语：Homotopy type theory）是马丁-勒夫的构造性类型论在抽象同伦理论中的一种解释。有结果之间的联系建设性数学和代数拓扑，提供拓扑语义内涵系统的类型理论，以及计算方法，代数拓扑通过类型理论为基础的证明助手，如Coq。目前的工作调查归纳类型在这种情况下。修改规则的归纳类型，包括类型的良基树，或W型，提出了，并确定了基本的同伦语义，这样的类型。所有结果的证明都已由Coq证明助理正式验证，并且用于此验证的证明脚本构成了本研究的重要组成部分。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。