论文标题
参数概念作为类型理论的单体模型
Notions of parametricity as monoidal models for type theory
论文作者
论文摘要
本文为观察到了立方结构在使用参数时自然出现的观察，从而给出了坚实的理论基础。我们声称立方模型是参数性的。我们将类别，LEX类别或氏族用作类型理论的模型。在这种情况下，我们将参数性的概念定义为单体模型，而参数模型则将其定义为模块。这不仅涵盖了任何类型都带有关系的通常参数，还涵盖了与谓词，反身关系，两个关系等的变体。在这种情况下，我们证明了从参数模型到任意模型的健忘函数的左右与伴随。此外，我们为这些自由和可爱的参数模型提供了明确的紧凑描述。然后，我们给出了许多参数概念的示例，可以构建以下内容作为cofrey parametric模型： - 立方体任何变体的立方体类别。 - 截断的半立管的LEX类别（或仅具有反射性的立方体）对象。 - 芦苇纤维纤维的半立方体（或仅具有反射性的立方体）对象的氏族。
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 functors from parametric models to arbitrary ones have left and right adjoints. Moreover we give explicit compact descriptions for these freely and cofreely parametric models. Then we give many examples of notion of parametricity, allowing to build the following as cofreely parametric models: - Categories of cubical objects for any variant of cube. - Lex categories of truncated semi-cubical (or cubical with reflexivities only) objects. - Clans of Reedy fibrant semi-cubical (or cubical with reflexivities only) objects.
