线性依赖型理论的一个图模型
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$，其中传统的指数模态被理解为共同的$! = LM$。我们提供了这个理论的模型称为图模型，它扩展了依赖类型理论的广群模型，以适应线性类型。在这里，Carnival类型被解释为一个群胚族，而线性类型被解释为任何对称幺半群范畴$\mathcal{V}$中的图$A:Γ\to\mathcal{V}$。我们表明，图模型可以在一定条件下支持一个线性模拟的单价公理，并提供了一些讨论的高维性质的线性依赖类型。
英文摘要：
We present a type theory dealing with non-linear, "ordinary" dependent types (which we will call cartesian) and linear types, where both constructs may depend on terms of the former. In the interplay between these, we find new type formers $\sqcap_{x:A}B$ and $\sqsubset_{x:A}B$, akin to $Π$ and $Σ$, but where the dependent type $B$, (and therefore the resulting construct) is a linear type. These can be seen as internalizing universal and existential quantification of linear predicates. We also consider two modalities, $M$ and $L$, transforming linear types into cartesian types and vice versa. The theory is interpreted in a split comprehension category $π:\mathcal{T}\to\mathcal{C}^\to$ accompanied by a split symmetric monoidal fibration, $π: \mathcal{L}\to\mathcal{C}$. This structure determines, for any context $Γ$, fibers $\mathcal{T}_Γ$ and $\mathcal{L}_Γ$; the category of cartesian types and the monoidal category of linear types over $Γ$, respectively. Here, the type formers $\sqcap_{x:A}$ and $\sqsubset_{x:A}$ are understood as right and left adjoints of the monoidal reindexing functor $π_A^*:\mathcal{L}_Γ\to\mathcal{L}_{Γ.A}$. The operators $M$ and $L$ induce a fiberwise adjunction $L \dashv M$ between $\mathcal{L}$ and $\mathcal{T}$, where the traditional exponential modality is understood as the comonad $! = LM$. We provide a model of this theory called the Diagram model, which extends the groupoid model of dependent type theory to accommodate linear types. Here, cartesian types are interpreted as a family of groupoids, while linear types are interpreted as diagrams $A:Γ\to\mathcal{V}$ in any symmetric monoidal category $\mathcal{V}$. We show that the diagrams model can under certain conditions support a linear analogue of the univalence axiom, and provide some discussion on the higher-dimensional nature of linear dependent types.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
