基于参数性的半单纯与半立方集合的形式化

Notions of parametricity as monoidal models for type theory

This article gives a solid theoretical grounding to the observation that cubical structures arise naturally when working with parametricity. We claim that cubical models are cofreely parametric. We use categories, lex categories or clans as models of type theory. In this context we define notions of parametricity as monoidal models, and parametric models as modules. This covers not only the usual parametricity where any type comes with a relation, but also variants where it comes with a predicate, a reflexive relation, two relations, and many more. In this setting we prove that forgetful funct…

立方类型论的内部参数性

Internal Parametricity for Cubical Type Theory

本文提出一种结合立方类型论与内部参数性原语的计算类型论，支持非直性和相对性，通过分析高阶归纳类型间的多态函数展示其应用，并给出预层模型。

高维参数性的立方范畴

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，这使我们能够澄清他们的方法，并加强他们的主要结果。一旦澄清，他们的双纤维框架，也可以被视为我们的理论的一维实例。

Parametricity and Semi-Cubical Types

We construct a model of type theory enjoying parametricity from an arbitrary one. A type in the new model is a semi-cubical type in the old one, illustrating the correspondence between parametricity and cubes. Our construction works not only for parametricity, but also for similar interpretations of type theory and in fact similar interpretations of any generalized algebraic theory. To be precise we consider a functor forgetting unary operations and equations defining them recursively in a generalized algebraic theory. We show that it has a right adjoint. We use techniques from locally present…

迭代参数性在索引形式中的高度依赖递归结构

The very dependent recursive structure of iterated parametricity in indexed form

本文研究了迭代参数性在索引形式中的依赖结构，通过定义性推理替代等式推理，提出了一种高度依赖的构造方法。

Nuprl中范畴理论和类型论的前层模型的形式化

Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl

本文是解释Nuprl中立方类型论的构造模型的形式化的系列文章中的第一篇。在本文中，我们只讨论形式化的不依赖于基范畴选择的部分。所以，它阐明了我们如何，进行，三次类型论的形式化的第一步。