The Cayley-Dickson Construction in Homotopy Type Theory
本文在同伦类型论的背景下定义了$\mathbb S^3$上的H-空间结构。因此，我们得到的四元数的Hopf纤维化$\mathbb S^3\hookrightarrow\mathbb S^7\twoheadrightarrow\mathbb S^4$的描述，只使用同伦不变量的工具。
2016-10-04 cs.LO math.AT math.CT
Homotopy-initial algebras in type theory
我们研究归纳类型的类型理论，使用同伦类型理论和数学的单价数学基础提供的见解。我们这样做是通过引入同伦初始代数的新概念。这个概念是由一个纯粹的类型理论的可压缩性条件，取代了标准的，范畴理论的泛性质，涉及适当的态射的存在性和唯一性。我们的主要结果刻画了与W-型等价的同伦初始代数的类型。
2015-04-21 math.CT math.LO
The equivalence of the torus and the product of two circles in homotopy type theory
同伦类型论是一个新的数学分支，它融合了抽象同伦论和高级范畴论与逻辑和类型论的观点。它允许我们将各种数学对象表示为基本类型论构造，更高的归纳类型。证明了在同伦类型论中，环面等价于两个圆的乘积。这一结果表明，环面作为高阶归纳型的综合定义是正确的。
2015-10-13 cs.LO math.LO
Homotopy Type Theory in Lean
我们在精益证明助手中讨论同伦类型论库。该图书馆特别面向合成同伦理论。特别令人感兴趣的是使用了一些高级归纳类型的原始概念，即截断和截断，以及立方方法的使用。
2017-09-20 cs.LO math.LO
The HoTT Library: A formalization of homotopy type theory in Coq
我们报告的HoTT库的发展，同伦类型论的形式化Coq证明助手。它形式化了大多数基本的同伦类型论，包括单值性、高级归纳类型、大量的综合同伦理论，以及范畴论和模态。该图书馆已被用作几个独立开发的基础。我们讨论的决定，导致图书馆的设计，我们评论同伦类型论的相互作用与最近推出的功能Coq，如宇宙多态性和私人归纳类型。
2016-12-09 cs.LO math.LO
Homotopy type theory: the logic of space
这是从范畴论和拓扑学的角度对类型论、合成拓扑学和同伦类型论的介绍，作为《数学和物理的新空间》（Gabriel Catren和Mathieu Anel编）一书的一章。
2017-03-08 math.CT math.LO
Homotopy Type Theory: A synthetic approach to higher equalities
这是对同伦类型理论和哲学家的单价基础的介绍，作为《工作哲学家的范畴》一书的一章（伊莱恩·兰德里编辑）。
2016-01-27 math.CT math.LO
Type theory and homotopy
这篇综述文章的目的是向读者介绍逻辑、几何和代数之间的联系，这种联系最近以马丁-洛夫的构造性类型理论到同伦理论的解释的形式被发现，从而产生了新的例子。更高维度的类别。
2010-10-09 math.CT math.LO
2-adjoint equivalences in homotopy type theory
本文在同伦类型论中定义（半）2-伴随等价并证明其性质，且已在Lean中形式化验证。
2021-01-21 math.CT math.LO
Homotopy Types of Abstract Elementary Classes
证明了对于任何同伦型$X$，存在一个抽象初等类$\mathcal{C}$，它具有联合嵌入、混合和无极大模型，使得分类空间实现同伦型$X$ .我们提供了一些明确的例子。
2020-05-18 math.AT math.CT math.LO
Univalent universes for elegant models of homotopy types
我们构造了一个在Voevodsky意义下的单叶宇宙在一些合适的模型范畴同伦类型（从Grothendieck的测试范畴理论获得）。在实践中，这意味着，例如，从单纯集的同伦理论，内涵类型理论与单叶公理可以解释在同伦理论的立方集（有或没有联系），或Joyal的细胞集。
2014-05-31 math.AT math.CT math.LO
Natural models of homotopy type theory
类型论的自然模型的概念是根据预层的可表示的自然拟序来定义的。结果表明，这种模型完全符合Dybjer意义下的族范畴的概念，它可以被看作是一个代数形式的类型论。我们确定这样的模型的条件，以满足推理规则的依赖和，依赖产品，和内涵的身份类型，在同伦类型理论中使用。然后，它表明，一个类别承认这样的模型，如果它有一类映射，表现得像抽象的纤维化在公理同伦理论：他们应该是稳定的拉回下，封闭的组合和相关产品，并应有弱正交分解到类。因此，同伦理论的许多熟悉的设置也承认同伦类型理论的基本系统的自然模型。
2017-01-08 math.CT math.LO
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
本论文的目的是在同伦型理论的背景下提出综合同伦理论。我们将提出各种结果在这个框架中，最值得注意的是建设的Atiyah-Hirzebruch和塞尔谱序列的上同调，已完全正式的精益证明助手。
2018-08-31 cs.LO math.AT math.LO
W-types in Homotopy Type Theory
我们将详细说明为什么Voevodsky的单性公理的单纯集模型也是W型模型。此外，我们还将讨论单纯预层范畴中的W-型以及在集合论模型中的应用。
2015-11-25 math.CT math.LO
Classifying Types
在类型论的语言中，同伦理论现象的研究有时被称为“合成同伦理论”。同伦类型论中的同伦理论只是同伦类型论的众多方面之一，同伦类型论还包括集合论语义的研究（同伦类型论模型和集合或范畴的元理论中的单值性），类型论语义学（同伦类型理论的内模）和计算语义学，以及研究同伦类型理论内部语言中的各种问题，这些问题不一定是由同伦理论激发的，或与基于同伦类型理论的形式化数学库的发展相关的问题。本论文是关于综合同伦理论的发展。
2019-06-22 math.LO
Canonicity and homotopy canonicity for cubical type theory
本文通过锥形论证，在预层模型内证明了立方类型理论的两个规范性结果：同伦规范性和规范性，分别在不使用和使用路径提升方程的情况下，确保每个自然数与数字路径相等。
2022-02-02 cs.LO math.LO
Homotopy theoretic models of identity types
本文提出了同伦代数与数理逻辑之间的一种新的联系。证明了一种形式的内涵类型理论在任何Quillen模型范畴中都是有效的，推广了Martin-Loef类型理论的Hofmann-Streicher广群模型。
2007-09-03 math.AT math.CT math.LO
Higher Structures in Homotopy Type Theory
同伦类型理论在《单叶基础》中使用的预期模型是同伦类型的无穷范畴，也称为无穷广群胚。高级结构的问题是构造数学所需的同伦类型，特别是那些不是集合的同伦类型。目前的构式库，包括通常的类型形成词和更高的归纳类型，足以满足其中的许多但不是全部。我们讨论有问题的情况，通常是那些涉及无限层次的相干数据（例如半单纯类型）的情况，以及在单价基础中发展同伦类型理论的元理论的问题。我们还讨论了一些建议的解决方案。
2018-07-05 math.LO
Brouwer's fixed-point theorem in real-cohesive homotopy type theory
我们结合同伦类型理论与公理的凝聚力，表达后者内部的一个版本的“伴随逻辑”，其中的离散化和cosdiscretization模态的特点是使用判断的形式主义的“脆变量”。这就产生了我们称之为“空间”和“内聚”的类型理论，其中的类型可以被视为具有独立的拓扑和同伦结构。这些类型理论可以用来正式研究拓扑学产生同伦理论的过程（“基本的$\infty$ -广群”或“形状”），将同伦类型理论的“标识”从拓扑学的“连续路径”中分离出来。在一个称为“实凝聚”的进一步改进中，形状由来自实数的连续映射确定，如在经典代数拓扑中一样。这使我们能够正式地再现同伦理论在拓扑学中的一些经典应用。作为例子，我们证明了Brouwer的不动点定理.
2017-04-25 math.AT math.CT math.LO
Classical field theory via Cohesive homotopy types
经典场论如何在凝聚同伦型理论中综合出现的简要综述。扩展的会议摘要提交给2013年秋季在巴塞罗那举行的类型理论，同伦理论和单价基础会议的会议记录
2013-11-05 hep-th math-ph math.AT
Calculating the Fundamental Group of the Circle in Homotopy Type Theory
最近的工作同伦类型理论利用了一个令人兴奋的新的对应马丁-洛夫的依赖型理论和数学学科的范畴论和同伦理论。范畴论和同伦理论提出了新的原则，以增加类型论，类型论可以用新的方式来形式化这些数学领域。本文给出了代数拓扑学中的一个基本结果：圆的基本群是整数。虽然简单，这个例子是有趣的几个原因：它说明了同伦类型论的新原则;它混合了传统同伦理论证明的结果与类型理论归纳推理的想法;它提供了一个上下文来理解现有的类型理论难题-一个宇宙（类型）是必要的，以证明归纳类型的构造函数是不相交的和单射的。
2013-01-15 cs.PL math.AT math.LO
Homotopy Type Theory: Univalent Foundations of Mathematics
同伦类型论是一个新的数学分支，基于最近发现的同伦理论和类型论之间的联系，它为数学的数学基础带来了新的思想。一方面，Voevodsky的微妙而美丽的“univalence公理”意味着同构结构可以被识别。另一方面，“高级归纳类型”提供了对同伦理论的一些基本空间和构造的直接的、逻辑的描述。两者都不可能在经典的集合论基础上直接捕获，但是当它们结合在同伦类型论中时，它们允许一种全新的“同伦类型逻辑”。这就提出了一种新的数学数学基础概念，具有内在的同伦内容，数学对象的“不变”概念，以及方便的机器实现，可以作为工作数学家的实际帮助。这本书的目的是作为第一个系统的阐述基础上产生的“单价基础”计划，和收集的例子，这种新风格的推理-但不要求读者知道或学习任何形式的逻辑，或使用任何计算机证明助手。
2013-08-03 cs.PL math.AT math.CT
Voevodsky's Univalence Axiom in homotopy type theory
在这个简短的说明，我们给一个一瞥同伦型理论，一个新的数学领域的交叉代数拓扑和数理逻辑，我们解释弗拉基米尔Voevodsky的单价解释它。这种解释引起了单价基金会计划，这是今年的主题在高等研究所。
2013-02-19 math.HO math.LO
Synthetic Homotopy Theory
本论文基于同伦类型论（HoTT）系统阐述合成同伦理论，通过合成构造 Hopf 纤维化、证明 Blakers--Massey 定理、推导 Freudenthal 悬挂定理并计算 $n$-球面的部分同伦群，为代数拓扑研究提供了新的形式化方法。
2024-09-24 math.AT math.LO
On homotopy types of limits of semi-algebraic sets and additive complexity of polynomials
证明了由闭有界半代数集构成的单参数半代数族的极限的不同同伦类型的个数在定义该族的任意无量词一阶公式的加法复杂度中是单指数有界的.作为一个重要的结果，我们得到的不同同伦类型的数目定义的半代数子集的$\mathbb{R}^k$的一个无量词的一阶公式$Φ$，其中的总和出现在$Φ$的多项式的加法复杂性至多是$a$，是有界的$2^{(k+a)^{O(1)}}$。这证明了一个猜想所作的巴苏和Vorobjov [在一些同伦类型的纤维的一个可定义的地图，J。（2）2007，757- 776]。
2012-06-19 math.AG math.AT math.LO
