A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are developed, the latter in terms of (strict) indexed symmetric monoidal categories with comprehension. Various optional type formers are treated in a modular way. In particular, we will see that the historically much-debated multiplicative quantifiers and identity types arise naturally from categorical considerations. These new multiplicative connectives are further characterised by several identities relating them to the usual connectives from dependent type theory and linear logic. Finally, one important class of models, given by families with values in some symmetric monoidal category, is investigated in detail.

翻译：本文提出了一种结合（直觉主义）线性类型与类型依赖的类型理论，从而恰当地推广了直觉主义依赖类型理论和完整线性逻辑。我们发展了该理论的语法和完备的范畴语义，后者基于（严格）带理解构的索引对称幺半范畴。各种可选类型构造子以模块化方式处理。特别地，我们将看到历史上备受争议的乘法量词和同一类型自然而然地源于范畴考量。这些新的乘法连接词进一步通过若干恒等式表征，这些恒等式将它们与依赖类型理论和线性逻辑中的常用连接词联系起来。最后，我们详细研究了一类重要模型，即取值于某个对称幺半范畴的族模型。