  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.

Logic in Computer Science;Programming Languages;Category Theory