Homotopy Type Theory: Univalent Foundations of Mathematics
同伦类型论是一个新的数学分支，基于最近发现的同伦理论和类型论之间的联系，它为数学的数学基础带来了新的思想。一方面，Voevodsky的微妙而美丽的“univalence公理”意味着同构结构可以被识别。另一方面，“高级归纳类型”提供了对同伦理论的一些基本空间和构造的直接的、逻辑的描述。两者都不可能在经典的集合论基础上直接捕获，但是当它们结合在同伦类型论中时，它们允许一种全新的“同伦类型逻辑”。这就提出了一种新的数学数学基础概念，具有内在的同伦内容，数学对象的“不变”概念，以及方便的机器实现，可以作为工作数学家的实际帮助。这本书的目的是作为第一个系统的阐述基础上产生的“单价基础”计划，和收集的例子，这种新风格的推理-但不要求读者知道或学习任何形式的逻辑，或使用任何计算机证明助手。
2013-08-03 cs.PL math.AT math.CT
Introduction to Univalent Foundations of Mathematics with Agda
我们介绍Voevodsky的单价基础和单价数学，并解释如何发展他们与计算机系统Agda，这是基于马丁-洛夫类型论。Agda允许我们编写数学定义、构造、定理和证明，例如数论、分析、群论、拓扑学、范畴论或程序设计语言理论，检查它们的逻辑和数学正确性。Agda默认是一个构造性的数学系统，这相当于说它也可以被认为是一种用于操作数学对象的程序设计语言。但我们可以假设选择公理或排中律的数学部分，需要他们，在失去系统的隐式编程语言的字符为代价。对于一个完全建设性的发展单价数学在阿格达，我们将需要使用其新的立方风味，我们希望这些说明提供了一个基础，研究人员有兴趣学习立方类型论和立方阿格达作为下一步。与大多数主题的论述相比，我们的工作与明确的宇宙水平。
2022-09-02 cs.LO math.LO
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
本文将 Gylterud 的迭代集合类型 V0 构造为非单价严格范畴并证明其局部笛卡尔闭，从而在最小构造性直谓 HoTT/UF 中内部建模外延类型论，且结果已基本在 Agda 中形式化。
2024-02-07 cs.LO math.LO
The Univalence Principle
单价原理是这样一种陈述，等价的数学结构是不可区分的。我们证明了这一原理的一般版本，适用于以非代数和基于空间的风格定义的所有基于集合的、范畴的和更高范畴的结构，以及高阶理论（例如拓扑空间）的模型。特别是，我们制定了一个一般的定义，任何这样的结构的对象的不可分割性，和相应的单性条件，推广Rezk的完整性条件的Segal空间，并确保所有等价的结构是levelwise等价。我们的工作建立在Makkai的一阶逻辑与相关排序，但表示在Voevodsky的单价基础（UF），扩展以前的工作的结构同一性原则和单价类别UF。这使得不可否认性可以简单地表示为识别，并产生一个正式的理论，在经典同伦理论中是可解释的，但也在其他更高的拓扑模型。由此可见，单价基础是更高范畴数学的完全等价不变基础，正如Voevodsky所意图的那样。
2022-08-29 cs.LO math.CT math.LO
Towards a constructive simplicial model of Univalent Foundations
我们提供了一个部分解决方案的问题，定义一个建设性的版本Voevodsky的单纯模型的单价基础。为此，我们证明建设性的对应物的必要结果的单纯同伦理论，建设性版本的Kan-Quillen模型结构的第二个命名的作者建立的基础上。特别是，我们表明，依赖产品沿纤维化与coherant域保持纤维化，建立弱等价扩张性质的弱等价纤维化与coherant域之间的定义和一个单叶分类纤维化的小纤维化之间的bioherant对象。这些结果使我们能够定义一个理解类支持身份类型，$Σ$ -类型，$Π$ -类型和一个单价宇宙，只留下一个连贯的问题要解决。
2021-03-16 math.CT math.LO
On a model invariance problem in Homotopy Type Theory
本文利用内射模型结构赋予函子范畴[B（Z ~ 2），Gpd]一个具有单叶论域的类型论纤维化范畴的结构.它给我们一个新的模型的马丁-洛夫型理论与相关的总和，相关的产品，单位类型和一个单叶宇宙。这个模型，连同作者在另一部著作中发展的模型，在同一个基本范畴中，连同同一个宇宙，就投射纤维化而言，被证明不是单价的，提供了两个奎伦等价模型范畴的一个例子，它们承载着不同的类型论模型。因此，我们提供了一个反例的模型不变性问题制定的迈克尔舒尔曼。
2017-12-09 math.AT math.CT math.LO
A univalent universe in finite order arithmetic
本文用有穷级算法解释了具有单叶论域$\,\mathcal{U}_0$的同伦型理论。我们消除了格罗滕迪克宇宙，避免了替换公理，并限制了分离的所有用途。
2015-01-10 math.LO
Higher Structures in Homotopy Type Theory
同伦类型理论在《单叶基础》中使用的预期模型是同伦类型的无穷范畴，也称为无穷广群胚。高级结构的问题是构造数学所需的同伦类型，特别是那些不是集合的同伦类型。目前的构式库，包括通常的类型形成词和更高的归纳类型，足以满足其中的许多但不是全部。我们讨论有问题的情况，通常是那些涉及无限层次的相干数据（例如半单纯类型）的情况，以及在单价基础中发展同伦类型理论的元理论的问题。我们还讨论了一些建议的解决方案。
2018-07-05 math.LO
The univalence axiom in cubical sets
本文证明了Voevodsky的univalence公理在基于对称三次集的类型论模型中成立。我们还将讨论天鹅建设的身份类型在这种变化的立方集。这证明了我们有一个支持依赖积、依赖和、单叶宇宙和具有通常判断等式的恒等类型的类型论模型，并且这个模型是在一个构造性元理论中制定的。
2017-10-30 cs.LO math.LO
On Small Types in Univalent Foundations
我们调查建设性的单价基础的谓词方面。通过谓词和构造性，我们分别意味着我们不假设Voevodsky的命题公理或排中律。我们的工作补充了现有的工作预测数学探索什么不能做预测在单价基础。我们的第一个主要结果是，非平凡的（有向或有界）完全偏序集必然是大的。也就是说，如果这样一个非平凡偏序集是小的，那么弱命题集成立。如果我们把非平凡性加强到正性，就有可能导出完整的命题正性。非平凡性和积极性之间的区别类似于非空性和居住性之间的区别。此外，我们证明了局部小，非平凡（有向或有界）完全偏序集必然缺乏可判定的平等。我们证明了我们的结果一般类的偏序集，其中包括例如有向完备偏序集，有界完备偏序集，超格和框架。其次，这些非平凡偏序集必然很大的事实有一个重要的推论，就是塔斯基定理（以及类似的结果）不能应用于非平凡的例子。此外，我们解释说，塔斯基定理，允许大结构的推广是可证明为假的，在一个单价宇宙中的序数序数有小的上确界的存在下，设置consistents。后者也导致我们调查的相互定义性和相互作用的类型宇宙的命题截断和集的替代品，以及一个集替换原则。第三，我们澄清，在我们的谓词设置，之间的关系的传统定义的超格，要求所有子集的上确界和我们的定义，要求所有小家庭的上确界。
2023-05-03 cs.LO math.LO
Domain Theory in Constructive and Predicative Univalent Foundations
我们在没有Voevodsky公理的构造性单叶基础上发展域理论。在以前的工作中，在这个方向上，我们构建了PCF的斯科特模型，并证明了其计算充分性，基于有向完备偏序集（dcpos）。在这里，我们进一步考虑代数和连续dcpos，并建立斯科特的$D_\infty$模型的无类型的$λ$ -演算。在谓词基础中处理大小问题的一种常见方法是使用信息系统或抽象基或形式拓扑而不是dcpos，以及近似关系而不是Scott连续函数。在这里，我们接受dcpos可能很大，并与类型宇宙一起工作来解释这一点。例如，在PCF的Scott模型中，dcpo在第二论域$\mathcal{U}_1$中具有载体，在第一论域$\mathcal{U}_0$中具有索引类型的有向族的上确界。把偏序集看作是一个范畴，我们可以说这些dcpos是大的，但局部很小，并且有小的滤子余极限。在代数dcpos的情况下，为了处理大小问题，我们继续模仿可及范畴的定义。有了这样的定义，我们的斯科特的$D_\infty$的建设再次给出了一个大的，局部小，代数dcpo小有向上确界。
2022-06-15 cs.LO math.LO
On lifting univalence to the equivariant setting
这篇博士论文讨论了弗拉基米尔·沃德斯基提出的内涵类型理论和单价公理的一些新模型。我们的工作是在类型论纤维化范畴的定义（本文中考虑的模型概念）和类型论纤维化范畴中的宇宙的框架内进行的，这些定义是由Michael Shulman定义的。本论文的目的主要在于探索单叶性公理的稳定性，特别是在以下意义上：给定一个配备有单叶论域U的类型论纤维化范畴C，我们渴望赋予函子范畴[D，C]（其中D是一个小范畴）一个类型论纤维化范畴加一个单叶论域的结构。
2016-04-12 math.AT math.CT math.LO
Classical field theory via Cohesive homotopy types
经典场论如何在凝聚同伦型理论中综合出现的简要综述。扩展的会议摘要提交给2013年秋季在巴塞罗那举行的类型理论，同伦理论和单价基础会议的会议记录
2013-11-05 hep-th math-ph math.AT
Predicative Aspects of Order Theory in Univalent Foundations
我们调查的预测方面的建设性的单叶基础秩序理论。通过谓词和构造性，我们分别意味着我们不假设Voevodsky的命题公理或排中律。我们的工作补充了现有的工作预测数学探索什么不能做预测在单价基础。我们的第一个主要结果是，非平凡的（有向或有界）完全偏序集必然是大的。也就是说，如果这样一个非平凡偏序集是小的，那么弱命题集成立。如果我们把非平凡性加强到正性，就有可能导出完整的命题正性。非平凡性和积极性之间的区别类似于非空性和有住性之间的区别。我们证明了我们的结果一般类的偏序集，其中包括有向完备偏序集，有界完备偏序集和超格，使用一个技术概念的$δ_{\mathcal V}$ -完备偏序集。我们还表明，非平凡的局部小$δ_{\mathcal V}$ -完全偏序集必然缺乏可判定的平等。具体地说，我们得到弱排中假设一个非平凡的局部小$δ_{\mathcal V}$ -完全偏序集与可判定的平等。此外，如果我们假设正性而不是非平凡性，那么我们可以导出完全排中律。其次，我们证明了Zorn引理、Tarski最大不动点定理和Pataraia引理中的每一个引理都蕴涵命题的不动点。因此，这些原则在本质上是不可断言的，因此，秩序理论的谓词性发展必须没有它们。最后，我们澄清，在我们的谓词设置，超格的传统定义，要求所有子集的上确界和我们的定义，要求所有小家庭的上确界之间的关系。
2021-04-21 cs.LO math.LO
Introduction to Homotopy Type Theory
这是一本介绍性教科书，以单价数学和同伦类型理论，数学基础，利用结构性质的数学定义和建设。在数学实践中，通常认为等价对象是相同的，例如，识别同构群。在集合论中，不可能使这种常见的实践形式化。例如，在集合论中有多少不同的单例集，就有多少不同的平凡群。另一方面，类型论对适应单价公理的数学基础采取了一种更结构化的方法。然而，这需要我们重新思考两个物体相等意味着什么。这本教科书向读者介绍马丁-勒夫的依赖型理论，单价数学的中心概念，并向读者展示如何做数学从一个单价的观点。超过200个练习包括训练读者在类型理论推理。这本书是完全独立的，特别是没有事先熟悉类型理论或同伦理论的假设。
2022-12-21 math.CT math.LO
Univalent Foundations of Constructive Algebraic Geometry
本文在同伦类型论与单一基础下，研究了定义qcqs-schemes的两种构造性方法，并证明了这两种定义的一致性，建立了相应范畴间的等价关系。
2024-07-24 math.AG math.LO
Homotopy Type Theory: A synthetic approach to higher equalities
这是对同伦类型理论和哲学家的单价基础的介绍，作为《工作哲学家的范畴》一书的一章（伊莱恩·兰德里编辑）。
2016-01-27 math.CT math.LO
The Cantor-Schröder-Bernstein Theorem for $\infty$-groupoids
我们证明了同伦类型或$\infty$ -群胚的康托-施罗德-伯恩斯坦定理以如下形式成立：对于任何两个类型，如果每一个嵌入到另一个中，那么它们是等价的。这个论证是在同伦类型论或Voevodsky的单价基础（HoTT/UF）的语言中发展出来的，并且需要经典逻辑。由此可见，该定理在任何布尔型$\infty$ -topos中都成立。
2020-08-26 math.AG math.LO
Reflexive graph lenses in univalent foundations
本文提出反向图棱镜，作为介于反射图族和展示反射图之间的中间抽象，简化了复杂结构中身份类型的特征化。通过案例研究展示了其在反射图理论和多项式类型运算中的应用，并建立了反射图纤维类型与单值反射图棱镜类型的等价性。
2026-01-19 cs.LO math.CT math.LO
Univalent typoids
一个typoid是一个配备了等价关系的类型，使得该类型的项之间的等价项相对于它们之间的给定等价关系满足某些条件，这些条件概括了等式项的属性。由此得到的弱2-广群结构可以推广到每一个有限水平。引入的typoid和typoid函数的概念推广了setoid和setoid函数的概念。单价typoid是满足单价公理的一般版本的typoid。我们证明了一些基本事实，单价typoids，他们的产品和指数。作为推论，我们在typoid理论中得到了命题截断的一个解释。偶类型胚和单叶类型胚是同伦类型论中偶预范畴和范畴的一个弱广群。
2022-04-24 math.CT math.LO
W-types in Homotopy Type Theory
我们将详细说明为什么Voevodsky的单性公理的单纯集模型也是W型模型。此外，我们还将讨论单纯预层范畴中的W-型以及在集合论模型中的应用。
2015-11-25 math.CT math.LO
Domain theory in univalent foundations I: Directed complete posets and Scott's $D_\infty$
本文在构造性和谓词性单值基础中发展域理论，通过跟踪类型宇宙参数实现有向完备偏序集的迭代构造，并给出 Scott 的 $D_\infty$ 模型的谓词性重构，已在 Agda 中形式化。
2024-07-18 cs.LO math.LO
Domain Theory in Constructive and Predicative Univalent Foundations
本文在不使用命题重定尺寸、排中律及选择公理的构造性谓词化单子基础中发展 dcpo 与 Scott 连续映射理论，并形式化验证 PCF 和 λ-演算模型。
2023-09-28 cs.LO math.LO
Continuous and algebraic domains in univalent foundations
本文在不使用命题重定尺寸、排中律和选择公理的构造性直谓单值基础中，借助命题截断与小基条件发展连续和代数 dcpo 理论，并形式化于 Agda。
2025-09-02 cs.LO math.LO
On the $\infty$-topos semantics of homotopy type theory
本文以课程讲义形式综述同伦类型论的语义基础，介绍 Voevodsky 的单纯模型与 Shulman 将严格单价宇宙解释推广至任意 $\infty$-拓扑斯的成果。
2024-03-01 math.AT math.CT math.LO
Homotopy-initial algebras in type theory
我们研究归纳类型的类型理论，使用同伦类型理论和数学的单价数学基础提供的见解。我们这样做是通过引入同伦初始代数的新概念。这个概念是由一个纯粹的类型理论的可压缩性条件，取代了标准的，范畴理论的泛性质，涉及适当的态射的存在性和唯一性。我们的主要结果刻画了与W-型等价的同伦初始代数的类型。
2015-04-21 math.CT math.LO
Construction of the Circle in UniMath
证明了$\mathbb{Z}$ -torsons的$\mathrm{T}\mathbb{Z}$型具有圆的依赖泛性质，这一性质将其刻画为唯一的同伦等价.该结构使用Voevodsky的Univalence公理和命题截断，产生一个独立的圆结构，不使用更高的归纳类型。
2020-11-18 cs.LO math.AT math.LO
The Compatibility of the Minimalist Foundation with Homotopy Type Theory
本文证明MF的内涵与外延两个层次均与HoTT兼容，关键在于HoTT借助单价公理和高归纳商类型统一内涵与外延特征，从而使MF获得全新可计算模型。
2024-01-29 math.LO
Synthetic perspectives on spaces and categories
研究利用同伦类型理论和单纯类型理论，揭示在原生等价不变环境中关于空间和范畴的基本证明技术，包括路径或箭头归纳原理及相关构造。
2026-07-17 math.AT math.CT math.LO
Modalities in homotopy type theory
本文在同伦类型论中发展因子分解系统、反射子全域和模态理论，通过局部化高阶归纳类型构造（n-连通，n-截断）因子分解系统及子拓扑斯的内部表示，并给出语义。
2020-01-07 cs.LO math.CT math.LO
Notes on Clans and Tribes
这些笔记的目的是给出同伦类型理论的分类介绍/分析。这些笔记不完整（2017年10月）。关于单价部落的那一章不见了。引用并不总是与文本相关联。更好的版本正在准备中。
2017-10-27 math.AT math.CT math.LO
From Multisets to Sets in Hotmotopy Type Theory
基于同伦类型论中的多重集，给出了一个集合论模型。模型的平等性是身份类型。迭代集的基本类型可以在马丁-洛夫类型理论中表述，没有更高的归纳类型（HIT），并且是类型论中集合论的Aczel 1978模型的基本类型的子类型。Voevodsky的Univalence公理和纯粹的集合等价性（一种温和的HIT）被用来证明该模型的构造性集合论的公理。我们给出了一个等价的模型在第10章中提供的同伦型理论的单价基础计划。
2016-12-16 math.LO
Effective Kan fibrations in simplicial sets
我们介绍的概念，一个有效的Kan纤维化，一个新的数学结构，可用于研究单纯同伦理论。我们的主要动机是使单纯同伦理论适用于同伦类型理论。有效Kan纤维化是简单集的映射，配备了满足某些非平凡性质的选择电梯的结构化集合。这与Kan纤维化的普通的、非结构化的概念形成对比。我们表明，Kan纤维化的基本性质可以扩展到明确的建设有效的Kan纤维化。特别是，我们给出了一个建设性的（明确的）证明，有效的Kan纤维化是稳定的推动下，或crossred指数。这对于普通的Kan纤维是不可能的。我们进一步表明，有效的Kan纤维化是本地的，或完全由他们的纤维以上的representables。我们还给出了一个（无效）证明，即能具有有效Kan纤维化结构的映射，恰是普通Kan纤维化。因此，隐含地，这两个概念仍然描述相同的同伦理论。通过证明有效的Kan纤维化结合了所有这些性质，我们解决了同伦型理论中的一个公开问题。通过这种方式，我们的工作提供了第一步，在给予建设性的Voevodsky模型的单叶型理论在单纯集。
2022-04-30 cs.LO math.AT math.CT
Univalent Material Set Theory
本文在同伦类型论框架下推广物质集合论至更高类型层级，定义∈-结构与构造性集合论高阶公理，给出Pⁿ函子余代数表述并构造其初始代数模型，实现单值宇宙的分层∈-结构表示。
2024-07-18 math.LO
Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
University of Bergen（卑尔根大学）；Tallinn University of Technology（塔林理工大学）
本文在同伦类型理论中构建了非良基础集模型，提出扩展AFA和SAFA的通用化，并通过M型构建了满足SAFA通用化的层级模型，同时刻画了M型的身份类型。
2026-06-26 cs.LO math.LO
Could $\infty$-category theory be taught to undergraduates?
在21世纪初，普通范畴论扩展到$\infty$范畴，这是一项引人注目的成就，由Joyal和Lurie开创，其他许多人也做出了贡献。不幸的是，解决这些结果中固有的无限同伦相干问题所需的技术参数使得非专家很难学习这个理论。本文综述了两个旨在缩小$\infty$ -范畴论和普通1-范畴论之间差距的程序。第一个利用1-范畴和$\infty$ -范畴作为对象的范畴之间的相似性来提供标准范畴定理的“形式”证明。第二，这是相当多的投机，探讨$\infty$ -类别从新的“单价”基础密切相关的同伦类型理论。
2023-02-15 math.AT math.CT math.LO
Strict stability of extension types
Chapman University（查普曼大学）
本文通过Voevodsky分裂方法证明扩展类型在Riehl-Shulman同伦类型论中严格稳定，从而为内∞-范畴提供语义基础。
2026-06-06 cs.LO math.CT math.LO
Path categories and propositional identity types
同伦理论和类型理论之间的联系最近吸引了很多关注，Voevodsky的单价基础和马丁-洛夫的单位元类型在奎伦模型范畴中的解释是其中的亮点。在本文中，我们建立了一个自然的削弱马丁-洛夫的规则之间的联系的身份类型已被科恩，Coquand，Huber和Mortberg在他们的工作中考虑的一个建设性的解释，一方面，和一个道路范畴的概念，一个轻微的变化的经典概念的范畴的不确定性对象由于布朗。这涉及到表明，与弱身份类型的类型理论的句法类别进行结构的路径类别，加强早期的结果由Avigad，Lumsdaine和Kobrkin。通过这种方式，我们不仅将同伦理论中的一个著名概念与逻辑中的一个自然概念联系起来，而且还为进一步的发展提供了一个框架。
2016-09-20 math.CT math.LO
Non-Standard Models of Homotopy Type Theory
本文提出 filter quotient construction 作为构建同伦类型论新模型的方法，证明其在保留类型论构造子和公理的模型范畴性质的同时不保留集合论外部性质，从而产生具有新行为的非标准模型。
2025-08-12 math.CT math.LO
