On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom
本文利用投射纤维化赋予函子范畴[B（C2），Gpd]一个具有论域的类型论纤维化范畴的结构.它提供了一个新的模型的马丁-洛夫型理论与相关的总和，相关的产品，单位类型和一个宇宙。事实证明，这个宇宙，在霍夫曼和施特赖歇的群胚模型中提升小离散群胚的单价宇宙的自然候选者，不是单价的。
2020-09-08 math.AT math.CT math.LO
Three Equivalent Ordinal Notation Systems in Cubical Agda
我们提出了三个序数记号系统表示序数低于$\varepsilon_0$在类型理论，使用最近的类型理论的创新，如互感归纳的定义和更高的归纳类型。我们展示了如何序数算术可以开发这些系统，以及他们如何承认一个超穷归纳法原则。我们证明了所有三个符号系统是等价的，这样我们就可以使用单价原理在它们之间传输结果。我们所有的建筑都在立方体的阿格达中实现。
2020-01-02 math.LO
Cubical sets and the topological topos
Coquand的三次集模型同伦类型论提供了计算解释的基础上的一价公理和一些更高的归纳类型，实现在三次证明助手。本文有助于理解该模型。我们做了三个贡献：1。约翰斯通的拓扑拓扑是为了将单纯集的几何实现作为拓扑之间的几何态射而创建的。约翰斯通表明，单纯集分类严格的线性秩序与不相交的端点和（经典）的单位区间是这样一个秩序。在这里，我们表明，它也可以是一个目标的立体实现表明，Coquand的立体集分类的几何理论的平坦分配格。作为一个副结果，我们得到了一个三次集的单纯实现。2.利用三次集拓扑中的内部“区间”，我们构造了单位类型的Moore路径模型。3.我们在三次类型论内部构造了一个预模型结构，从而在三次集合中的非线性对象上构造了一个预模型结构。
2016-10-17 cs.LO math.CT math.LO
On Church's Thesis in Cubical Assemblies
我们表明，教会的论文，公理指出，所有功能的自然是可计算的，不举行立方型理论的立方大会模型。我们表明，尽管如此教会的论文是一致的，通过构建一个反射子宇宙的立方大会，它持有的单价类型理论。
2019-05-08 cs.LO math.LO
Multisets in Type Theory
一个多重集由元素组成，但多重集的概念与集合的概念不同，它包含了每个元素在给定多重集中出现多少次的信息。在这项工作中，我们将研究迭代多集的概念，其中多集是从其他多集迭代建立起来的，在马丁-洛夫类型理论的背景下，在Voevodsky的单价公理的存在下。Aczel 1978在类型论中引入了一个构造性集合论模型，使用了一个论域上的W-型量化和一个在其上归纳定义的等价关系，我们的研究采用了这个W-型，而不是考虑它上的单位类型，单位类型可以从Univalence公理中计算出来。我们的论文是，这给出了一个模型的多重集。为了证明这一点，我们适应公理的建设性集合论的多重集，并表明，他们持有我们的模型。
2016-10-25 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
Partial Univalence in n-truncated Type Theory
众所周知，univalence与unique of identity proofs（UIP）是不相容的，UIP是所有类型都是h-集的公理。这是由于有限的h-集只要不是h-命题就有非平凡的自同构。一个自然的问题是，限制于h-命题的单价是否与UIP相容。我们通过构建一个模型来肯定地回答这个问题，在这个模型中，类型是同伦类型论中定义为更高归纳类型的封闭宇宙的元素。这个宇宙有一个同时“部分”单价完成的路径构造器，即，仅限于H命题。更一般地说，我们表明，单价限于$(n-1)$类型是一致的假设，所有类型的$n$截断。此外，我们参数化我们的建设一个适当的良好的行为容器，抽象从一个具体的选择类型的former的宇宙。
2020-05-01 cs.LO math.CT math.LO
The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010)
这是我2010年2月4日在CMU的演讲，我第二次公开介绍了单价公理（文中称为“等价公理”）。公理的第一次介绍是在2009年11月慕尼黑LMU的一次演讲中。
2014-02-25 math.LO
Proof Theory of Constructive Systems: Inductive Types and Univalence
在费弗曼的工作中，显式数学和广义归纳定义理论起着核心作用。本文的一个目的是描述与马丁-洛夫类型理论和建设性Zermelo-Fraenkel集合论的连接。证明论有助于更深入地理解构造性数学的不同框架之间的关系。一些减少是已知的，只有通过序理论的特征。本文还讨论了Voevodsky的univalence公理的强度。另一个目标是在直觉显式数学的框架内研究广义归纳定义的直觉理论的强度，这超出了马丁-洛夫类型理论的范围。
2018-01-05 math.LO
Parametricity, automorphisms of the universe, and excluded middle
众所周知，人们可以通过假设经典公理来构造非参数函数。我们的工作是一个相反的：我们证明经典公理依赖类型论假设特定的非参数化的情况。我们还讨论了经典公理和类型宇宙的自同构的存在性之间的相互作用。我们研究了内涵的Martin-Löf依赖类型论，并在某些结果中假设了进一步的原则，包括函数外延性、命题外延性、命题截断性和单价公理。
2017-06-27 cs.LO math.LO
Game-theoretic Interpretation of Type Theory Part II: Uniqueness of Identity Proofs and Univalence
在本文中，基于以前的工作（第一部分），我们提出了一个游戏语义的内涵变体的直觉类型论，反驳了唯一性的原则，身份证明和验证的univalence公理，虽然我们不解释非平凡的高等命题等式。具体来说，根据霍夫曼和Streicher的历史广群解释，我们配备了一个广群结构的第一部分中的谓词游戏，这引起了（谓词）gamoid的概念。粗略地说，gamoids是“指定（计算）等式的游戏”，它解释了ID类型中的微妙之处。然后，我们制定了一个类别的家庭的预测gamoid，配备了依赖产品，依赖和，ID类型以及宇宙，这形成了一个具体的实例的广群模型。我们相信，这项工作是一个重要的垫脚石走向一个完整的解释同伦类型论。
2016-04-05 cs.LO math.CO math.CT
Homotopy type theory and Voevodsky's univalent foundations
最近的发现已经取得了连接抽象同伦理论和领域的类型理论从逻辑和理论计算机科学。这就产生了一个新的领域，它被命名为“同伦型理论”。在这个方向上，弗拉基米尔·沃沃茨基观察到，可以用单纯集来建模类型论，并且这个模型满足一个额外的属性，称为单价公理，它有许多惊人的结果。他随后提出了一个计划，他称之为单价基础，在类型论的背景下发展数学，其中包含单价公理和其他可能的公理，这些公理是由单纯集模型激发的。由于类型论具有良好的计算性质，该程序可在计算机辅助下进行。在本文中，我们给同伦类型理论在Voevodsky的设置，注意理论和实践问题的介绍。特别是，该文件作为一个介绍的一般思想同伦类型理论以及一些具体细节Voevodsky的工作使用著名的证明助手Coq。这篇论文是为具有代数拓扑学基础知识的普通数学家编写的;本文不假设任何类型论、逻辑或计算机科学的初步知识。
2012-10-20 cs.LO math.AT math.LO
Categorical structures for type theory in univalent foundations
本文在单值类型论中比较三种依赖类型论模型结构，构造映射并证明在单值公理下部分等价，引入相对宇宙研究其沿范畴等价及Rezk完备化的转移，并在Coq/UniMath中形式化。
2018-09-08 cs.LO math.CT math.LO
From Multisets to Sets in Hotmotopy Type Theory
基于同伦类型论中的多重集，给出了一个集合论模型。模型的平等性是身份类型。迭代集的基本类型可以在马丁-洛夫类型理论中表述，没有更高的归纳类型（HIT），并且是类型论中集合论的Aczel 1978模型的基本类型的子类型。Voevodsky的Univalence公理和纯粹的集合等价性（一种温和的HIT）被用来证明该模型的构造性集合论的公理。我们给出了一个等价的模型在第10章中提供的同伦型理论的单价基础计划。
2016-12-16 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
Oracle modalities
本文以高阶模态重新表述 Turing 可归约性，在 cubical type theory 中借助 Markov induction 与 computable choice 公理给出综合证明，并初步建立 Turing 度与同伦论的联系。
2024-06-09 cs.LO math.CT math.LO
W-types in Homotopy Type Theory
我们将详细说明为什么Voevodsky的单性公理的单纯集模型也是W型模型。此外，我们还将讨论单纯预层范畴中的W-型以及在集合论模型中的应用。
2015-11-25 math.CT math.LO
Extension Types for Free
本文将多种场景下的扩展类型统一到双层类型论框架，证明其对HoTT保守，验证了Riehl等的演算，还结合Agda形式化结果，为解决立方类型论对书式HoTT的保守性猜想提供了方法。
2026-07-31 cs.LO math.AT math.CT
Univalent universes for elegant models of homotopy types
我们构造了一个在Voevodsky意义下的单叶宇宙在一些合适的模型范畴同伦类型（从Grothendieck的测试范畴理论获得）。在实践中，这意味着，例如，从单纯集的同伦理论，内涵类型理论与单叶公理可以解释在同伦理论的立方集（有或没有联系），或Joyal的细胞集。
2014-05-31 math.AT math.CT math.LO
A Foundation for Synthetic Algebraic Geometry
本文基于Kock和Blechschmidt的工作，在Zariski topos内部建立代数几何基础，使用同伦类型论结合三个公理作为其内部语言，提出“Zariski局部选择”公理并通过立方模型证明其合理性，贡献了高阶类型在上同调推理中的应用。
2023-09-12 math.AG 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
The Simplicial Model of Univalent Foundations (after Voevodsky)
University of Pittsburgh（匹兹堡大学）；Institute for Advanced Study, Princeton（普林斯顿高等研究院）
本文通过构造单纯集中的univalent类型论模型，展示了等价性公理在该模型中的成立，并证明了Martin-Löf类型论与ZFC的一致性关系。
2018-10-29 math.AT math.CT math.LO
On the $\infty$-topos semantics of homotopy type theory
本文以课程讲义形式综述同伦类型论的语义基础，介绍 Voevodsky 的单纯模型与 Shulman 将严格单价宇宙解释推广至任意 $\infty$-拓扑斯的成果。
2024-03-01 math.AT math.CT 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
A diagram model of linear dependent type theory
我们提出了一个类型理论处理非线性，“普通”的依赖类型（我们将称为carnival）和线性类型，其中这两个结构可能依赖于前者的条款。在它们之间的相互作用中，我们发现了新的类型形成者$\sqcap_{x:A}B$和$\sqsubset_{x:A}B$，类似于$Π$和$Σ$，但是其中依赖类型$B$（因此得到的构造）是线性类型。这些可以被看作是线性谓词的内在泛量化和存在量化。我们还考虑了两种模式，$M$和$L$，将线性类型转换为腕关节类型，反之亦然。该理论被解释在一个分裂的理解范畴$π:\mathcal{T}\to\mathcal{C}^\to$伴随着一个分裂的对称monoidal纤维化，$π: \mathcal{L}\to\mathcal{C}$。对于任何上下文$Γ$，该结构分别确定纤维$\mathcal{T}_Γ$和$\mathcal{L}_Γ$ ;在$Γ$上的carbohydrate类型的范畴和线性类型的monoidal范畴。在这里，类型形成器$\sqcap_{x:A}$和$\sqsubset_{x:A}$被理解为monoidal重索引函子$π_A^*:\mathcal{L}_Γ\to\mathcal{L}_{Γ.A}$的右伴随和左伴随。操作符$M$和$L$在$\mathcal{L}$和$\mathcal{T}$之间诱导了一个纤维连接$L \dashv M$，其中传统的指数模态被理解…
2018-06-27 math.LO
