Till innehåll på sidan

Martin Lundfall: Models of linear dependent type theory

Tid: Må 2017-12-18 kl 11.00 - 12.00

Plats: Room 14, House 5, Kräftriket, Department of Mathematics, Stockholm University

Respondent: Martin Lundfall (MSc student)

Handledare: Peter Lumsdaine

Exportera till kalender

Abstract:  In this paper, we construct a type theory which deals with non-linear, ordinary dependent types (which we will call cartesian), andlinear types, where both constructs may depend on terms of cartesian types. In the interplay between the cartesian and linear types we introduce the new type formers ⊓x:AB and 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 quantification over linear propositions. We also introduce the modalities M and L, transforming linear types into cartesian types and vice versa. We interpret the theory in a split comprehension category π : T → C→ [Jac93], accompanied by a split monoidal fibration (Definition4.3), q : L → C. The intuition is that C models a category of contexts, so that for any Γ ∈ C, the fiber TΓ is the category containing the cartesian types which can be formed in the context Γ, while the fiber LΓ is a monoidal category of linear types in Γ. In this setting, the type formers ⊓x:A and x:A are understood as right and left adjoints of the monoidal reindexing functor πA∗ : LΓ → LΓ.Acorresponding to the weakening projection πA : Γ.A → Γ in C. The operators M and L give rise to a fiberwise adjunction L ⊣ Mbetween L and T , where we understand the traditional exponential modality as the comonad ! = LM. We provide two concrete examples of models, the set-indexed families model and the diagrams model. In the former, cartesian types are interpreted in the familiar way, as sets indexed by their context set Γ, and linear types are interpreted as Γ-indexed family of objects of a symmetric monoidal category V. The latter model extends the groupoid model of dependent type theory [HS98] to accomodate linear types. Here, cartesian types over a context Γ are interpreted as a family of groupoids indexed over the groupoid Γ, while linear types are interpreted as diagrams over groupoids, A : Γ → V in any symmetric monoidal category V. We show that thediagrams model can under certain conditions model a linear analogue of the univalence axiom, and provide some discussion on the higher-dimensional nature of linear dependent types.