Cubical sets and the topological topos
Coquand的三次集模型同伦类型论提供了计算解释的基础上的一价公理和一些更高的归纳类型，实现在三次证明助手。本文有助于理解该模型。我们做了三个贡献：1。约翰斯通的拓扑拓扑是为了将单纯集的几何实现作为拓扑之间的几何态射而创建的。约翰斯通表明，单纯集分类严格的线性秩序与不相交的端点和（经典）的单位区间是这样一个秩序。在这里，我们表明，它也可以是一个目标的立体实现表明，Coquand的立体集分类的几何理论的平坦分配格。作为一个副结果，我们得到了一个三次集的单纯实现。2.利用三次集拓扑中的内部“区间”，我们构造了单位类型的Moore路径模型。3.我们在三次类型论内部构造了一个预模型结构，从而在三次集合中的非线性对象上构造了一个预模型结构。
2016-10-17 cs.LO math.CT math.LO
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
守护递归是一种强大的模式递归方法，可以看作是步进索引的抽象形式。它目前被广泛用于分离逻辑，通过求解具有负出现的域方程来模拟具有高级功能的程序设计语言。在其多时钟版本中，保护递归也可以用于对共归纳类型进行编程和推理，编码类型中递归定义所需的生产力条件。本文提出了第一种类型论，它结合了多时钟保护递归和立方类型论的特点，并给出了一个指称语义。结合使用高阶归纳类型（Higher Inductive Types，HIT）和保护递归，可以对传统上难以在类型论中表示的共归纳类型进行简单的编程和推理，例如标记转移系统的分支分支类型。例如，我们的研究结果意味着这些双相似性意味着路径平等，因此证明可以沿着双相似性证明。我们的技术贡献之一是一个新的原则下的时钟感应。这允许在时钟上的通用量化与HIT交换直到等价的类型，并且对于共归纳类型的编码至关重要。这种交换性的要求已经制定了归纳类型的公理在以前的类型论与多时钟保护递归，但我们目前的配方作为一个归纳原则允许制定一般的计算规则。
2022-06-03 cs.LO
Normal forms in cubical type theory
本文研究立方类型论中规范形式的定义与规范化的证明，提出传统风格的明确表述以供参考。
2026-10-28 cs.LO math.LO
On Higher Inductive Types in Cubical Type Theory
立方类型论为同伦类型论的某些方面提供了一个建设性的证明，如Voevodsky的univalence公理。这使得许多外延性原则，如函数和命题外延性，可以在理论中直接证明。本文描述了一个构造性语义，表达在一个预层拓扑结构的适当结构的启发，立方集，一些更高的归纳类型。它还扩展了立方类型论的语法更高的归纳类型的领域，环面，悬浮液，截断，和推出。所有这些类型都由语义证明，并且对所有构造函数（包括高维构造函数）都有判断计算规则，并且在这些类型形成器下，宇宙是封闭的。
2018-04-30 cs.LO math.LO
Normalization for Cubical Type Theory
我们证明了规范化（单价，笛卡尔）立方类型论，关闭立方类型论的语法元理论的最后一个主要的开放问题。我们的规范化结果是减少免费的，在这个意义上产生的上下文中的条款和一个听话的语言$β/η$ -范式之间的等价类的双射。作为推论，我们得到了判断等式的可判定性和类型构造函数的内射性。
2021-04-19 cs.LO math.LO
On Church's Thesis in Cubical Assemblies
我们表明，教会的论文，公理指出，所有功能的自然是可计算的，不举行立方型理论的立方大会模型。我们表明，尽管如此教会的论文是一致的，通过构建一个反射子宇宙的立方大会，它持有的单价类型理论。
2019-05-08 cs.LO math.LO
The univalence axiom in cubical sets
本文证明了Voevodsky的univalence公理在基于对称三次集的类型论模型中成立。我们还将讨论天鹅建设的身份类型在这种变化的立方集。这证明了我们有一个支持依赖积、依赖和、单叶宇宙和具有通常判断等式的恒等类型的类型论模型，并且这个模型是在一个构造性元理论中制定的。
2017-10-30 cs.LO math.LO
Double negation stable h-propositions in cubical sets
研究在立方集模型中双重否定稳定h命题的分类器构造，通过该构造得出一些相对一致性结果，如特定分类器在立方集与元理论中的存在关系、添加戴德金实数不改变一致性强度及构造带扩展丘奇论题的同伦类型理论模型。
2026-07-15 cs.LO math.LO
Cubical Type Theory: a constructive interpretation of the univalence axiom
本文提出了一种类型论，它可以直接操作$n$维立方体（点、线、正方形、立方体等）。基于在立方集合模型中的依赖类型论的解释。这使得新的方法来推理身份类型，例如，函数可拓性在系统中直接可证明。此外，Voevodsky的univalence公理在这个系统中是可证明的。我们还解释了一些更高的归纳类型，如圆和命题截断的扩展。最后，我们在一个构造性的元理论中为这种立方类型论提供了语义。
2016-11-07 cs.LO math.LO
The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。
2016-09-05 cs.LO cs.PL
Canonicity and homotopy canonicity for cubical type theory
本文通过锥形论证，在预层模型内证明了立方类型理论的两个规范性结果：同伦规范性和规范性，分别在不使用和使用路径提升方程的情况下，确保每个自然数与数字路径相等。
2022-02-02 cs.LO math.LO
Parametricity and Semi-Cubical Types
我们从一个任意的模型构造了一个具有参数性的类型论模型。新模型中的一个类型是旧模型中的半立方体类型，说明了参数性和立方体之间的对应关系。我们的结构不仅适用于参数性，而且适用于类型论的类似解释，实际上也适用于任何广义代数理论的类似解释。更准确地说，我们认为函子遗忘一元运算和方程定义他们递归的广义代数理论。证明了它有一个右伴随。我们使用的技术从局部可表示的范畴论，以及从商归纳归纳类型。
2022-01-25 cs.LO math.LO
A Cubical Language for Bishop Sets
提出XTT，一种面向Bishop集的笛卡尔立方类型理论，赋予类型同一性证明唯一性的定义性版本，并利用Artin粘合证明其规范性。
2022-03-28 cs.LO math.LO
Cubical Syntax for Reflection-Free Extensional Equality
我们贡献XTT，观察类型论的立体重建，扩展马丁-洛夫的内涵类型论与依赖的平等类型，享有功能扩展性和判断版本的唯一性的身份类型原则（UIP）：任何两个元素相同的平等类型是判断平等的。此外，我们推测，类型关系可以决定在一个实用的方式。在本文中，我们建立了一个代数规范性定理，使用一个新的立方扩展（独立提出的Awodey）的逻辑家庭或范畴胶合参数的启发Coquand和Shulman：每一个封闭的布尔类型的元素是可导等于要么“真”或“假”。
2019-06-06 cs.LO math.LO
Programming and Reasoning with Guarded Recursion for Coinductive Types
我们提出了守护的Alguda演算，简单类型的Alguda演算与守护递归和共归纳类型的扩展。保护递归类型的使用确保了良好类型程序的生产力。受模态逻辑和Atkey-McBride时钟量化启发的类型生成器可以将受保护的递归类型转换为共归纳类型，从而允许非因果函数的类型化。我们给出了演算的按名调用操作语义，并在树的拓扑中定义了适当的指称语义。充分性证明意味着程序的评估总是终止的。我们展示了表现力的演算显示的可定义性的解决方案Rutten的行为微分方程。我们介绍了一个程序逻辑与Löb归纳推理的上下文等价的程序。
2015-01-15 cs.LO cs.PL
Guarded Computational Type Theory
中野后来的模态可以用来指定和定义递归函数，这些函数是因果或同步的;与时钟变量的概念相一致，也可以捕获更广泛的生产性（co）程序。到目前为止，很难将这些构造与依赖类型结合起来，以保持类型论的操作意义并承认宇宙的层次结构。我们提出了一个业务帐户的守卫依赖类型论与时钟称为守卫计算类型论，具有一个新的时钟交叉连接，享有时钟无关原则，以及谓词层次的宇宙，不需要任何索引的时钟上下文。守护计算类型论同时是一种具有丰富规范逻辑的程序设计语言，也是一种可用于开发其他语言和逻辑语义的计算元语言。
2018-04-24 cs.LO
Guarded Dependent Type Theory with Coinductive Types
我们提出了守护依赖类型论，gDTT，一个扩展的依赖类型论与“后来”的模态和时钟量词的编程和证明与守护递归和共归纳类型。后一种模态用于以模块化的、基于类型的方式确保递归定义的生产力。时钟量词用于控制消除后一种模态，并使用保护递归类型对共归纳类型进行编码。发展gDTT的关键是新型和术语形成者，涉及我们所说的“延迟替代”。这些概括了早期工作中考虑的后一种模态的适用函子规则，并且对于依赖类型的编程和证明至关重要。我们证明了相对于指称模型的类型论的合理性。
2016-01-07 cs.LO cs.PL
Type Inference for Guarded Recursive Data Types
我们考虑保护递归数据类型（GRDT）的类型推断--代数数据类型的最新概括。我们减少类型推断GRDTs统一下的混合前缀。因此，我们得到有效的类型推断。推断是不完整的，因为允许出现在类型系统中的类型约束集只是由类型推断生成的那些类型约束的子集。因此，只有当程序被充分地类型注释时，推理才会成功。我们提出了完善的程序，逐步推断类型，并协助用户识别哪些类型的信息丢失。此外，我们还引入了一些过程来测试一个类型是否不是主体类型，并在存在主体类型时查找主体类型。
2005-07-14 cs.LO cs.PL
Denotational semantics for guarded dependent type theory
我们提出了一个新的模型的保护依赖类型论（GDTT），一个类型论与保护递归和多个时钟，其中一个可以编程，共归纳类型的原因。递归定义的共归纳程序和证明的生产力是使用保护递归编码在类型中的，因此可以模块化地检查，不像现代证明助手中实现的语法检查。该模型基于一类时间对象的协变预层，并使用时钟的预层对时钟进行量化建模。为了模拟时钟无关性公理，这对于使用共归纳类型进行编程至关重要，类型必须被解释为与时钟对象正交的预层。在依赖类型的情况下，这转化为提升条件，类似于在类型论的同伦理论模型中发现的提升条件，但在这里具有提升唯一性的额外要求。由于在这个模型中标准的Hofmann-Streicher构造定义的宇宙不满足这个性质，GDTT中的宇宙必须通过时钟变量的上下文来索引。我们展示了如何模拟这些宇宙的方式，时钟上下文的夹杂物引起的夹杂物的宇宙与类型操作的鼻子。
2020-04-13 cs.LO
First steps in synthetic guarded domain theory: step-indexing in the topos of trees
我们提出的拓扑S的树作为一个模型的保护递归。我们研究了内部依赖类型的高阶逻辑的S，并表明S模型的两个模态算子，谓词和类型，作为后卫的递归定义的条款，谓词和类型。特别是，我们将展示如何解决递归类型方程涉及依赖类型。我们建议S的内部逻辑为程序设计语言和程序逻辑的步骤索引模型的抽象版本的合成构造提供了正确的设置。作为一个例子，我们展示了如何构建一个程序设计语言的模型，该语言具有完全在S内部逻辑中的高阶存储和递归类型。此外，我们给出了合成守护整环理论模型的公理化范畴处理，证明了对任何具有良基的完备Heyting代数A，A上层的拓扑构成合成守护整环理论的模型，推广了S的结果.
2012-10-01 cs.LO
Internal Parametricity for Cubical Type Theory
本文提出一种结合立方类型论与内部参数性原语的计算类型论，支持非直性和相对性，通过分析高阶归纳类型间的多态函数展示其应用，并给出预层模型。
2021-11-02 cs.LO
Denotational semantics of recursive types in synthetic guarded domain theory
就像数学的任何其他分支一样，程序设计语言的指称语义应该在类型论中形式化，但是将传统的域理论语义（如最初在经典集合论中制定的）适应类型论已经证明是具有挑战性的。本文是一个项目的一部分，制定指称语义的类型论与保护递归。这样做的好处不仅是提供更简单的语义和充分性等属性的证明，而且有望在未来扩展到具有高级功能的语言，如通用引用，超出了传统域理论技术的范围。工作在保护依赖类型论（GDTT），我们开发的指称语义的FPC，简单类型的λ演算扩展与递归类型，建模的递归类型的FPC使用保护递归类型的GDTT。我们证明了GDTT模型的合理性和计算充分性，使用语法和语义之间的逻辑关系，也使用守护递归类型。指称语义是内涵的，在这个意义上，它计算计算一个项的值所需的展开-折叠约简的数量，但是我们构建了一个关系，该关系涉及外延相等项的指称，即，在不同步骤中计算相同值的项对。最后，我们展示了如何在类型论中执行术语的指称语义，并证明了执行布尔术语的指称计算与FPC的操作语义相同的值。
2018-05-02 cs.LO cs.PL
Naive cubical type theory
本文提出一种基于笛卡尔立方体类型论的非形式化类型论方法，作为同伦类型论非形式化程序的立方体式替代，涵盖函数外延性、路径归纳、群胚结构等基本结果。
2021-05-09 cs.LO
Canonicity for Cubical Type Theory
立方类型论是马丁-洛夫类型论的一个扩展，最近由科恩、科坎德、莫特伯格和作者提出，它允许直接操纵$n$维立方体，其中Voevodsky的Univalence公理是可证明的。在本文中，我们证明了立方类型论的规范性：任何自然数在一个仅由名称变量构建的上下文中判断等于一个数字。为了实现这一点，我们制定了一个类型和确定性的操作语义，并采用了适应于预表设置的可计算性参数。
2017-10-30 cs.LO
Modelling Recursion and Probabilistic Choice in Guarded Type Theory
本文在守护类型论中利用高阶归纳类型和守护递归建模带概率选择与递归类型的语言，并建立操作与指称语义间的关系以支持充分性和上下文等价推理。
2024-10-24 cs.LO cs.PL
Cubical informal type theory: the higher groupoid structure
在同伦类型论一书中进行了一个为非正式类型论开发约定和符号的项目，该项目是为了建立一个框架，该框架是通过Voevodsky的univalance公理和更高的归纳类型来管理高维结构的公理来增强建设性类型论的，本文提出了一种以立方类型论为基础的非正式类型论的方法。为此，我们采用了一个立方体类型论最近提出的Angiuli，侯（Favonia）和哈珀，一个框架与累积层次的单价Kan宇宙，充分的univalence和实例的高归纳类型。本文只研究关于型的高广群结构的几个基本定理。
2018-06-22 cs.LO
Parametric Cubical Type Theory
我们展示了一个计算类型论，它结合了高维结构的carnivical立方类型论的内部参数化原语的参数类型论，绘制出两者之间的相似性和区别。结合理论既支持一价性，也支持它的关系等价物，我们称之为相对论。我们展示了使用的理论，通过分析多态类型，包括更高的归纳类型之间的功能，我们通过例子展示了如何相对性可以用来表征归纳类型的关系解释。
2019-07-08 cs.LO
Eliminating reversals from cubical type theories
University of Gothenburg（哥德堡大学）；Chalmers University of Technology（查尔姆斯理工大学）
本文研究了立方类型理论中反向操作的消除，通过扭构造证明了在自对偶区间理论中加入反向操作的保守扩展，首次给出了具有反向操作理论的同调理论对应于拓扑空间的模型。
2026-05-14 cs.LO
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
在一个立方集合范畴中，我们构造了一个具有一个单叶的非谓词论域的立方类型论模型。我们表明，这种不可预测的宇宙在立方组装模型不满足命题的形式。
2019-09-09 cs.LO
Implementation of Two Layers Type Theory in Dedukti and Application to Cubical Type Theory
在本文中，我们在Dedukti逻辑框架中对立体类型论（CTT）进行了编码。类型检查CTT表达式的特点是在德摩根代数中的一个决策过程，到目前为止，这还不能用Dedukti的重写规则来表达。作为替代，2层类型理论是马丁-洛夫类型论的变体，其中所有或部分定义的平等可以用所谓的外部平等来表示。我们建议通过在Dedukti中给出2层类型论（2LTT）的编码和在2LTT中给出CTT的部分编码来拆分编码。
2021-01-11 cs.LO
A Model of Parametric Dependent Type Theory in Bridge/Path Cubical Sets
本文的目的是证明我们的依赖类型论模型的所有技术方面与参数量词[Nuyts，Vezzosi和Devriese，2017]。众所周知，任何预层范畴都构成了依赖类型论的模型[Hofmann，1997]，如果元理论有一个宇宙的层次，那么它也包括一个宇宙的层次[Hofmann and Streicher，1997]。我们通过定义桥/路径立方体的基本类别BPCube和适应BPCube的一般预层模型来构建我们的模型，以满足我们的需要。我们的模型主要基于Atkey，Ghani和Johann [2014]，Huber [2015]，Bezem，Coquand和Huber [2014]，Cohen，Coquand，Huber和Mörtberg [2016]，Moulin [2016]和Bernardy，Coquand和Moulin [2015]的模型。在第一章中，我们回顾了含族范畴的主要概念，以及依赖类型论的标准预层模型，并建立了我们将要使用的符号。在第二章中，我们在类型化规则中捕获了CwF的态射，以及它们之间的自然转换和转换。我们特别研究了前层范畴之间的CwFs的态射，这是由基范畴之间的函子引起的。第三章介绍了桥/路立方范畴BPCube及其桥/路立方集的预层范畴Psh（BPCube）。与三次集Psh（Cube）的范畴有丰富的相互作用，我们使用公理凝聚的思想更密切地研究[Licata和Shulman，…
2017-11-09 cs.LO math.CT
Using Structural Recursion for Corecursion
我们提出了一个（有限的）解决方案的问题，构造流值定义的递归方程，不尊重guardedness条件。在Coq、AGDA和其他高阶证明助手中，对上递归函数的定义施加了保护性条件。在本文中，我们特别集中在那些非守护方程递归调用下出现的功能。我们使用的流和函数之间的对应关系自然数表明，一些类的非保护的定义可以通过结构递归函数的编码建模。在实践中，这项工作扩展了流值类，可以在基于构造性类型论的定理证明器中定义归纳和共归纳类型，结构递归和保护共递归
2009-03-23 cs.LO
Notions of parametricity as monoidal models for type theory
这篇文章给出了一个坚实的理论基础，观察立方体结构自然出现时，与参数。我们认为三次模型是余自由参数的。我们使用范畴、lex范畴或氏族作为类型论的模型。在这种情况下，我们定义的概念参数作为monoidal模型，参数模型作为模块。这不仅涵盖了通常的参数性，其中任何类型都带有一个关系，而且还涵盖了它带有一个谓词，一个自反关系，两个关系等等的变体。在这种情况下，我们证明了从参数模型到任意模型的健忘函子都有左右伴随。此外，我们给出了这些自由和cofreely参数模型的显式紧描述。然后，我们给出了许多例子的概念parametricity，允许建立以下cofrely参数模型：-类别的立方体对象的任何变体的立方体。- 截顶半立方（或仅具自反性的立方）对象的Lex范畴。- 半立方体（或只有自反性的立方体）物体。
2022-09-02 cs.LO
Cubical Type Theoretic Navya-Nyāya
本文用立方体类型论形式化了印度晚期古典哲学中的海军-尼亚耶学派逻辑语言，解决了传统逻辑无法处理的依赖限定、类型缺失、非扩展性身份和无界关系深度等问题。
2026-05-10 cs.LO
Computational Higher Type Theory II: Dependent Cubical Realizability
这是第二次在一系列的论文扩展马丁勒夫的意义解释依赖类型论占高维类型。我们建立在第一部分中开发的简单类型的立体可实现性框架上，并将其扩展到依赖高维类型论的意义解释。这种扩展需要推广第一部分中给出的计算Kan条件，并考虑类型族对路径的作用。我们定义了标识类型，它将标识（路径）分类为一个类型，以及依赖函数和对类型。主要结果是一个规范性定理，它指出布尔类型的闭项的计算结果要么为真，要么为假。这一结果建立了第一个计算解释较高的依赖类型论，给出了一个确定性的操作语义，其程序，包括操作，实现Kan条件。
2017-04-26 cs.LO
Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
The University of Utah（犹他大学）
本文用立方阿格达形式化同调类型理论中的实数，避免了经典证明中的可数选择、 Bishop 集合构造的持久书务开销和 Dedekind 切割在预设类型理论中的繁琐层级跟踪。
2026-04-23 cs.LO
A Generalized Modality for Recursion
中野的后期模态允许类型表示函数的输出不直接依赖于其输入，因此计算其不动点是安全的。事实证明，这种保护递归的想法在各种上下文中都很有用，从具有无限数据结构的函数式编程到类型论内部的步进索引公式。分类模型表明，后一种模态本质上对应于离散时间尺度的简单重新索引。不幸的是，现有的保护类型论遭受编程目的的重大限制。这些局限性源于这样一个事实，即后一种模态的表达能力不足以捕捉函数的精确输入-输出依赖关系。因此，守卫类型论拒绝许多生产性定义。结合守卫类型论和同步程序设计语言的见解，我们提出了一个新的模式守卫递归。此模态可以将时间尺度的任何行为良好的重新索引应用于类型。我们称这种重新索引为时间扭曲。文献中的几种模态，包括后来的模态，对应于固定的时间扭曲，因此作为我们的特例出现。
2020-08-03 cs.LO cs.PL
Automating Boundary Filling in Cubical Type Theories
University of Oxford（牛津大学）；University of Gothenburg（哥德堡大学）；Chalmers University of Technology（查尔姆斯理工大学）；Stockholm University（斯德哥尔摩大学）
针对立方类型理论中高阶结构的复杂组合问题，提出基于偏序集映射的扭曲求解器和约束满足的Kan求解器，实现边界填充自动化，并通过Eckmann-Hilton定理等案例验证。
2026-06-15 cs.LO
Oracle modalities
本文以高阶模态重新表述 Turing 可归约性，在 cubical type theory 中借助 Markov induction 与 computable choice 公理给出综合证明，并初步建立 Turing 度与同伦论的联系。
2024-06-09 cs.LO math.CT math.LO
The equivariant model structure on cartesian cubical sets
Carnegie Mellon University（卡内基梅隆大学）；Chalmers University of Technology（查尔姆斯理工大学）；University of Gothenburg（哥德堡大学）；Johns Hopkins University（约翰斯·霍普金斯大学）
本文基于笛卡尔立方范畴的预层发展了构造性同调类型论模型，通过引入等变条件改进立方Kan纤维化，主要贡献是用计算机证明助手形式化了关键技术结果。
2026-04-20 cs.LO math.AT math.LO
Computational Higher Type Theory III: Univalent Universes and Exact Equality
这是一系列论文中的第三篇，这些论文将马丁-洛夫对依赖类型论的意义解释扩展到了一个笛卡尔立体可实现性框架，该框架解释了高维类型。我们扩展这个框架，包括一个累积层次的单叶Kan宇宙的Kan类型，确切的平等和其他pretypes缺乏Kan结构，和一个累积层次的pretype宇宙。与第一部分和第二部分一样，主要结果是一个规范性定理，说明布尔类型的闭项的值要么为真，要么为假。这建立了计算解释的笛卡尔立方更高的类型论的基础上立方程序配备了一个确定性的操作语义。
2017-12-05 cs.LO
Computing Cohomology Rings in Cubical Agda
在同伦类型论中，上同调理论是用高阶归纳类型和单叶性来综合研究的。本文通过给出上同调环的第一个完全机械化的定义，推广了以前的发展。这些环可以被定义为上同调群的直和加上由上积引起的乘法，并且在许多情况下可以被表征为多元多项式环的直积。为此，我们引入适当的定义的直和和分次环，然后我们使用定义的上同调环和多元多项式环。利用这一性质，我们计算了一些经典空间的上同调环，如球面和克莱因瓶.形式化是建设性的，因此它可以用来做具体的计算，它依赖于立方体Agda系统，它本身支持更高的归纳类型和计算的univalence。
2022-12-08 cs.LO math.AT
Formalising Inductive and Coinductive Containers
本文在Cubical Agda中形式化证明了容器保持最小与最大不动点，在不依赖UIP的条件下将容器函子理论从Set推广到类型的wild范畴，并展示了路径类型对共归纳证明的作用。
2025-07-04 cs.LO math.LO
An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets
Staton已经证明了有限集和部分双射上的预层范畴与名义限制集范畴之间存在等价性：参见[2，练习9.7]。这里的目的是看到，这扩展到[1]中引入的三次集范畴和配备了“01-替换”操作的名义集范畴之间的等价性。在我看来，将所讨论的拓扑等价地表示为01-替换集而不是立方集，将使构建和计算更容易（也更优雅），而这些构建和计算是建立意向性构造类型论的预期单价模型所必需的。
2014-01-30 cs.LO
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl
本文是解释Nuprl中立方类型论的构造模型的形式化的系列文章中的第一篇。在本文中，我们只讨论形式化的不依赖于基范畴选择的部分。所以，它阐明了我们如何，进行，三次类型论的形式化的第一步。
2018-06-15 cs.LO
Axioms for Modelling Cubical Type Theory in a Topos
本文探讨在任意拓扑斯中建模立方类型论所需的弱公理，阐明均匀Kan填充的定义，支撑Voevodsky univalence公理的构造性解释。
2018-12-08 cs.LO
Cubical Categories for Higher-Dimensional Parametricity
Reynolds的关系参数化理论形式化了系统F的参数多态性，从而捕捉到多态类型的系统F程序总是将相关的输入映射到相关的结果的想法。本文表明，Reynolds理论可以看作是系统F的关系参数化理论在1维的实例化，该理论在所有高维，包括无穷维都成立。这个理论是制定的一个p维立方范畴，我们使用它来定义一个p维参数模型的系统F的任何p，其中p是一个自然数或无穷大的新概念。我们表明，每个p维参数模型的系统F产生分裂$λ$ 2纤维化的类型被解释为面地图和退化保持立方函子和条款被解释为面地图和退化保持立方自然变换。我们证明了我们的理论是“好”的，通过证明Bainbridge等人的PER模型是可导出的另一个一维实例，并且所有维度的所有实例都导出了参数模型预期结果的高维类似物，例如图引理以及初始代数和最终余代数的存在。最后，我们的技术开发解决了Ghani等人提出的一些重大技术问题。最近的bifibrational治疗的关系parametricity，这使我们能够澄清他们的方法，并加强他们的主要结果。一旦澄清，他们的双纤维框架，也可以被视为我们的理论的一维实例。
2017-01-23 cs.LO
A General Framework for the Semantics of Type Theory
本文提出类型论的抽象概念，统一Martin-Löf、双层与立方类型论的语义，并证明双初始模型、内部语言及理论范畴与模型2-范畴的双等价等基本结果。
2023-05-26 cs.LO math.CT math.LO
A Semantics for Hybrid Iteration
最近引入的概念，保护跟踪（monoidal）范畴和保护（前）迭代单子的目的是统一不同的情况下，部分迭代，同时保持联系，建立理论的总迭代和保留其优点。在本文中，我们使用这些概念和相应的股票的结果来检查不同类型的混合计算的迭代。作为一个出发点，我们使用一个可用的概念，混合单子限制的类别集，并修改它，以获得一个合适的概念，守卫迭代与守卫解释为渐进性的时间-我们激励这种修改我们的意图捕捉芝诺行为在一个可以说是一般和可行的方式。我们说明了我们的结果与一个简单的程序设计语言的混合计算和解释它在开发的语义基础。
2019-02-05 cs.LO cs.PL
Extension Types for Free
本文将多种场景下的扩展类型统一到双层类型论框架，证明其对HoTT保守，验证了Riehl等的演算，还结合Agda形式化结果，为解决立方类型论对书式HoTT的保守性猜想提供了方法。
2026-07-31 cs.LO math.AT math.CT
Computational Higher Type Theory I: Abstract Cubical Realizability
布劳威尔的数学建构主义基础是基于一个直观的有意义的概念计算共享的所有数学家。Martin-Löf对构造性类型论的意义解释定义了计算方面的类型概念。简单地说，一个类型是一个完整的（封闭的）程序，它计算为一个规范类型，其成员是计算为该类型的规范元素的完整程序。这个解释可以通过功能扩展到不完整的（开放的）程序：类型和元素必须尊重自由变量的相等性。平等是没有证据的-两种类型或元素最多是平等的-平等的东西在所有的上下文中都是隐含的可互换的。更高维的类型论扩展了类型论以解释类型和元素的标识。同一性证明了两种类型或元素在所有的上下文中都可以通过一种明确的传输或强制操作而明确地互换。必须有足够多的标识，这是通过从同伦理论中强加一个广义形式的Kan条件来保证的。在这里，我们提供了一个简单的高维类型论基于一个程序设计语言，其中包括类似Kan-like结构见证了类型的更高结构的计算意义的马丁-勒夫风格的意义解释。处理包括一个更高的归纳类型的例子（即1维球体）和Voevodsky的一价原则的例子，它确定了等价类型。主要结果是一个计算规范性定理，验证了计算解释：一个封闭的布尔表达式必须总是评估为布尔值，即使在存在更高维的结构。这提供了高维类型论的第一个完全计算公式。
2016-06-14 cs.LO
The clocks they are adjunctions:Denotational semantics for Clocked Type Theory
Clocked类型论（Clotted Type Theory，CloTT）是一种用于保护递归的类型论，可用于使用共归纳类型进行编程，允许将生产力编码在类型中，并用于使用步骤索引的抽象形式来推理高级程序设计语言功能。CloTT之前已经被证明具有许多语法属性，包括强规范化，规范性和类型检查的可判定性。在本文中，我们为CloTT提供了一个有用的指称语义，例如，用于研究未来的CloTT扩展，如路径类型。构建这个模型的主要挑战是对CloTT中用于共归纳类型的共归纳推理的滴答概念进行建模。我们建立在一个以前用于对保护递归进行建模的类别上，但是在这个类别中没有ticks对象，因此不能使用标准工具对上下文中的tick假设进行建模。相反，我们展示了如何使用伴随函子来建模滴答，以及如何使用语义替换来建模滴答常数。
2018-04-18 cs.LO
Towards univalent reference types
本文在 guarded homotopy type theory 中为一般引用类型发展了指称语义，首次揭示了 univalence 对可变状态语义的深远影响，自动确保计算在堆对称性下不变，从而提供丰富的程序等价性。
2023-11-21 cs.LO
The RedPRL Proof Assistant (Invited Paper)
RedPRL是一个实验性的证明助手，基于笛卡尔立方计算类型论，一种新的类型论，用于受同伦类型论启发的高维结构。在Nuprl的风格中，RedPRL用户采用策略来建立立方函数程序的行为属性，体现证明的建设性内容。值得注意的是，RedPRL实现了两级类型论，允许扩展的、与证明无关的精确相等概念与高维的与证明相关的路径概念共存。
2018-07-05 cs.LO cs.PL
