A Categorical Semantics for Linear Logical Frameworks Matthijs Va´ka´r Department of Computer Science, University of Oxford, Oxford, United Kingdom Abstract. Atypetheoryispresentedthatcombines(intuitionistic)lin- 5 ear types with type dependency, thus properly generalising both intu- 1 itionisticdependenttypetheoryandfulllinearlogic.Asyntaxandcom- 0 plete categorical semantics are developed, the latter in terms of (strict) 2 indexedsymmetricmonoidalcategorieswithcomprehension.Variousop- n tionaltypeformersaretreatedinamodularway.Inparticular,wewillsee a thatthehistoricallymuch-debatedmultiplicativequantifiersandidentity J types arise naturally from categorical considerations. These new multi- 0 plicativeconnectivesarefurthercharacterisedbyseveralidentitiesrelat- 2 ingthemtotheusualconnectivesfromdependenttypetheoryandlinear logic.Finally,oneimportantclassofmodels,givenbyfamilieswithvalues ] O in some symmetric monoidal category, is investigated in detail. L . 1 Introduction s c [ Starting from Church’s simply typed λ-calculus (or intuitionistic propositional type theory), two extensions in perpendicular directions depart: 1 v • following the Curry-Howard propositions-as-types interpretation dependent 6 type theory (DTT) [1] extends the simply typed λ-calculus from a proof- 1 calculus of intuitionistic propositional logic to one for predicate logic; 0 • linear logic [2] gives a more detailed resource sensitive analysis, exposing 5 0 precisely how many times each assumption is used in proofs. . 1 A combined linear dependent type theory is one of the interesting directions 0 toexploretogainamorefine-grainedunderstandingofhomotopy type theory [3] 5 fromacomputersciencepointofview,explainingitsflowofinformation.Indeed, 1 many of the usual settings for computational semantics are naturally linear in : v character, either because they arise as !-co-Kleisli categories (coherence space Xi and game semantics) or for more fundamental reasons (quantum computation). Combining dependent types and linear types is a non-trivial task, however, r a anddespitesomeworkbyvariousauthorsthatweshalldiscuss,thepreciserela- tionship between the two systems remains poorly understood. The discrepancy between linear and dependent types is the following. • The lack of structural rules in linear type theory forces us to refer to each variable precisely once - for a sequent x:A⊢t:B, x occurs uniquely in t. • In dependent type theory, types can have free variables - x : A ⊢ B type, where x is free in B. Crucially, if x:A⊢t:B, x may also be free in t. 2 Matthijs V´ak´ar What does it mean for x to occur uniquely in t in a dependent setting? Do we count its occurrence in B? The usual way out, which we shall follow too, is to restrict type dependency on intuitionistic terms. Although this seems very lim- iting - for instance, we do not obtain an equivalent of the Girard translation, embedding DTT in the resulting system -, it is not clear that there is a reason- able alternative. Moreover, as even this limited scenario has not been studied extensively,we hope that a semantic analysis,which was so far missing entirely, may shed new light on the old mystery of linear type dependency. Historically, Girard’s early work in linear logic already makes movements to extend a linear analysis to predicate logic. Although it talks about first-order quantifiers, the analysis appears to have stayed rather superficial, omitting the identity predicates which, in a way,are what make first-orderlogic tick. Closely relatedisthatanaccountofinternalquantification,oralinearvariantofMartin- Lo¨f’s type theory, was missing, let alone a Curry-Howardcorrespondence. Later, linear types and dependent types were first combined in a Linear Logical Framework [4], where a syntax was presented that extends a Logical Framework with linear types (that depend on terms of intuitionistic types). This has given rise to a line of work in the computer science community [5,6,7]. All the work seems to be syntactic in nature, however, and seems to be mostly restrictedto the asynchronousfragmentin which we only have⊸-, Π-, ⊤-,and &-types. An exception is the Concurrent Logical Framework [8], which treats synchronous connectives resembling our I-, ⊗-, Σ-, and !-types. An account of additive disjunctions and identity types is missing entirely. Ontheotherhand,similarideas,thistimeatthelevelofcategoricalsemantics andspecificmodels(fromhomotopytheory,algebra,andphysics),haveemerged in the mathematical community [9,10,11,12]. In these models, as with Girard,a notion of comprehension was missing and, with that, a notion of identity type. Although, in the past year, some suggestions have been made on the nLab and nForum of possible connections between the syntactic and semantic work, no account of the correspondence was published, as far as the author is aware. Thepointofthispaper1istoclosethisgapbetweensyntaxandsemanticsand topavethewayforapropersemanticanalysisoflineartypedependency,treating a range of type formers including the crucial Id-types2. Firstly, in section 2, we presentasyntax,intuitionisticlineardependenttypetheory(ILDTT),anatural blendofthedualintuitionisticlinearlogic(DILL)[15]anddependenttypetheory (DTT)[16]whichgeneralisesboth.Secondly,insection3,wepresentacomplete categorical semantics, an obvious combination of linear/non-linear adjunctions [15] and comprehension categories [17]. Finally, in section 4, an important class of models is studied: families with values in a symmetric monoidal category. 1 Thispaperisbasedonthetechnicalreport[13]whereproofsandmorediscussioncan be found. Independently, Krishnaswami et al. [14] developed a roughly equivalent syntax and gave an operational rather than a denotational semantics. There, type dependencyis added toBenton’s LNL calculus, rather than to DILL. 2 Tobeprecise:extensionalId-types.IntensionalId-typesremainatopicofinvestiga- tion, dueto thesubtlety of dependentelimination rules in a linear setting. A Categorical Semantics for Linear Logical Frameworks 3 2 Syntax We assume the readerhas somefamiliaritywith the formalsyntaxofdependent type theory and linear type theory. In particular, we will not go into syntactic details like α-conversion,name binding, capture-free substitution of a for x in t (writet[a/x]),andpre-syntax.Detailsonallofthesetopicscanbefoundin[16]. We next present the formal syntax of ILDTT. We start with a presentation of the judgements that will representthe propositions in the language and then discuss its rules of inference: first its structural core, then the logical rules for a seriesofoptionaltype formers.We concludethissectionwithafew basicresults about the syntax. Judgements We adopt a notation ∆;Ξ for contexts, where ∆ is ‘an intuition- istic region’ and Ξ is ‘a linear region’, as in DILL [15]. The idea will be that we have an empty context and can extend an existing context ∆;Ξ with both intuitionistic and linear types that are allowed to depend on ∆. Our language will express judgements of the following six forms. ILDTTjudgement Intended meaning ⊢∆;Ξctxt ∆;Ξ isavalidcontext ∆;·⊢Atype Aisatypein(intuitionistic)context∆ ∆;Ξ⊢a:A aisatermoftypeAincontext∆;Ξ ⊢∆;Ξ≡∆′;Ξ′ctxt ∆;Ξ and∆′;Ξ′ arejudgementallyequalcontexts ∆;·⊢A≡A′type AandA′ arejudgementallyequaltypesin(intuitionistic)context∆ ∆;Ξ⊢a≡a′:A aanda′ arejudgementallyequaltermsoftypeAincontext∆;Ξ Fig.1. Judgements of ILDTT. Structural Rules We will use the following structural rules, which are essen- tially the structural rules of dependent type theory where some rules appear in both an intuitionistic and a linear form. We present the rules per group, with their names, from left-to-right, top-to-bottom. Rulesforcontextformation(C-Emp,Int-C-Ext,Int-C-Ext-Eq,Lin-C-Ext,Lin-C-Ext-Eq): ·;·ctxt ⊢∆;Ξctxt ∆;·⊢Atype ∆;Ξ≡∆′;Ξ′ctxt ∆;·⊢A≡Btype ⊢∆,x:A;Ξctxt ⊢∆,x:A;Ξ≡∆′,y:B;Ξ′ctxt ⊢∆;Ξctxt ∆;·⊢Atype ∆;Ξ≡∆′;Ξ′ctxt ∆;·⊢A≡Btype ⊢∆;Ξ,x:Actxt ⊢∆;Ξ,x:A≡∆′;Ξ′,y:Bctxt Variabledeclaration/axiomrules(Int-Var,Lin-Var): ∆,x:A,∆′;·ctxt ∆;x:Actxt ∆,x:A,∆′;·⊢x:A ∆;x:A⊢x:A Fig.2. Context formation and variable declaration rules. 4 Matthijs V´ak´ar The standard rules expressing that judgemental equality is an equivalence relation (C-Eq-R, C-Eq-S,C-Eq-T,Ty-Eq-R,Ty-Eq-S,Ty-Eq-T,Tm-Eq-R,Tm-Eq-S,Tm-Eq-T): ⊢∆;Ξctxt ⊢∆;Ξ≡∆′;Ξ′ctxt ⊢∆;Ξ≡∆;Ξctxt ⊢∆′;Ξ′≡∆;Ξctxt ⊢∆;Ξ≡∆′;Ξ′ctxt ⊢∆′;Ξ′≡∆′′;Ξ′′ctxt ⊢∆;Ξ≡∆′′;Ξ′′ctxt ∆;Ξ⊢Atype ∆;Ξ⊢A≡A′type ∆;Ξ⊢A≡Atype ∆;Ξ⊢A′≡Atype ∆;Ξ⊢A≡A′type ∆;Ξ⊢A′≡A′′type ∆;Ξ⊢A≡A′′type ∆;Ξ⊢a:A ∆;Ξ⊢a≡a′:A ∆;Ξ⊢a≡a:A ∆;Ξ⊢a′≡a:A ∆;Ξ⊢a≡a′:A ∆;Ξ⊢a′≡a′′:A ∆;Ξ⊢a≡a′′:A Thestandardrulesrelatingtypingandjudgementalequality(Tm-Conv,Ty-Conv): ∆;Ξ⊢a:A ⊢∆;Ξ≡∆;Ξ′ctxt ∆;·⊢A≡A′Type ∆′;Ξ′⊢a:A′ ∆′;·⊢Atype ⊢∆;·≡∆′;·ctxt ∆′;·⊢Atype Fig.3. A few standard rules for judgemental equality. Exchange,weakening,andsubstitutionrules(Int-Weak,Int-Exch,Lin-Exch,Int-Ty-Subst,Int-Ty- Subst-Eq,Int-Tm-Subst,Int-Tm-Subst-Eq,Lin-Tm-Subst,Lin-Tm-Subst-Eq): ∆,∆′;Ξ⊢J ∆;·⊢Atype ∆,x:A,∆′;Ξ⊢J ∆,x:A,x′:A′,∆′;Ξ⊢J ∆;Ξ,x:A,x′:A′,Ξ′⊢J ∆,x′:A′,x:A,∆′;Ξ⊢J ∆;Ξ,x′:A′,x:A,Ξ′⊢J (ifxisnotfreeinA′) ∆,x:A,∆′;·⊢Btype ∆;·⊢a:A ∆,x:A,∆′;·⊢B≡B′type ∆;·⊢a:A ∆,∆′[a/x];·⊢B[a/x]type ∆,∆′[a/x];·⊢B[a/x]≡B′[a/x]type ∆,x:A,∆′;Ξ⊢b:B ∆;·⊢a:A ∆,x:A,∆′;Ξ⊢b≡b′:B ∆;·⊢a:A ∆,∆′[a/x];Ξ[a/x]⊢b[a/x]:B[a/x] ∆,∆′[a/x];Ξ⊢b[a/x]≡b′[a/x]:B[a/x] ∆;Ξ,x:A⊢b:B ∆;Ξ′⊢a:A ∆;Ξ,x:A⊢b≡b′:B ∆;Ξ′⊢a:A ∆;Ξ,Ξ′⊢b[a/x]:B ∆;Ξ,Ξ′⊢b[a/x]≡b′[a/x]:B Fig.4.Exchange,weakening,andsubstitutionrules.Here,J representsastatementof theformBtype,B≡B′,b:B,orb≡b′:B,suchthatalljudgementsarewell-formed. A Categorical Semantics for Linear Logical Frameworks 5 Logical Rules We describe some (optional) type and term formers, for which wegivetypeformation(denoted-F),introduction(-I),elimination(-E),compu- tationrules(-C),and(judgemental)uniqueness principles(-U). We alsoassume the obvious rules to hold that state that the type formers and term formers re- spect judgemental equality. Moreover, Σ , Π , λ , and λ are name !x:!A !x:!A !x:!A x:A binding operators, binding free occurences of x within their scope. We demand -U-rules for the various type formers in this paper, as this al- lowsus to givea naturalcategoricalsemantics.This includes Id-types:we study extensional identity types. In practice, when building a computational imple- mentation of a type theory like ours, one would probably drop some of these rules to make the system decidable, which would correspond to switching to weak equivalents of the categorical constructions presented here.3 ∆,x:A;·⊢Btype ∆;·⊢Ctype ∆;·⊢Σ!x:!ABtype ∆;Ξ⊢t:Σ!x:!AB ∆;·⊢a:A ∆;Ξ⊢b:B[a/x] ∆,x:A;Ξ′,y:B⊢c:C ∆;Ξ⊢!a⊗b:Σ!x:!AB ∆;Ξ,Ξ′⊢lettbe!x⊗yinc:C ∆;Ξ⊢let!a⊗bbe!x⊗yinc:C ∆;Ξ⊢lettbe!x⊗yin!x⊗y:Σ!x:!AB ∆;Ξ⊢let!a⊗bbe!x⊗yinc≡c[a/x,b/y]:C ∆;Ξ⊢lettbe!x⊗yin!x⊗y≡t:Σ!x:!AB ∆,x:A;·⊢Btype ∆;·⊢Π!x:!ABtype ⊢∆;Ξctxt ∆,x:A;Ξ⊢b:B ∆;·⊢a:A ∆;Ξ⊢f :Π!x:!AB ∆;Ξ⊢λ!x:!Ab:Π!x:!AB ∆;Ξ⊢f(!a):B[a/x] ∆;Ξ⊢(λ!x:!Ab)(!a):B ∆;Ξ⊢λ!x:!Af(!x):Π!x:!AB ∆;Ξ⊢(λ!x:!Ab)(!a)≡b[a/x]:B[a/x] ∆;Ξ⊢f≡λ!x:!Af(!x):Π!x:!AB ∆;·⊢a:A ∆;·⊢a′:A ∆∆,,xz::AA;,Ξx′⊢:Ad;:·D⊢[zD/xty,pz/ex′] ∆;·⊢Id!A(a,a′)type ∆;·⊢a:A ∆;·⊢a′:A ∆;·⊢a:A ∆;Ξ′⊢p:Id!A(a,a′) ∆;·⊢refl!a:Id!A(a,a) ∆;Ξ[a/z],Ξ′⊢let(a,a′,p)be(z,z,refl!z)ind:D[a/x,a′/x′] ∆;Ξ⊢let(a,a,refl!a)be(z,z,refl!z)ind:D[a/x,a/x′] ∆;Ξ⊢let(a,a,refl!a)be(z,z,refl!z)ind≡d[a/z]:D[a/x,a/x′] ∆,x:A,x′:A;Ξ,z:Id!A(x,x′)⊢let(x,x′,z)be(x,x,refl!x)inc[x/x′,refl!x/z]:C ∆,x:A,x′:A;Ξ,z:Id!A(x,x′)⊢let(x,x′,z)be(x,x,refl!x)inc[x/x′,refl!x/z]≡c:C Fig.5.RulesforlinearequivalentsofsomeoftheusualtypeformersfromDTT(Σ-F, -I,-E, -C, -U,Π-F,-I, -E,-C, -U,Id-F,-I, -E,-C, -U). 3 In that case, in DTT, one would usually demand some stronger ‘dependent’ elimi- nation rules, which would make propositional equivalents of the -U-rules provable, adding some extensionality to thesystem, while preserving its computational prop- erties. Such rules are problematic in ILDTT, however, both from a syntactic and semantic point of view and a furtherinvestigation is warranted here. 6 Matthijs V´ak´ar ∆;·⊢Itype ∆;Ξ′⊢t:I ∆;Ξ⊢a:A ∆;·⊢∗:I ∆;Ξ,Ξ′⊢lettbe ∗ ina:A ∆;Ξ⊢let ∗ be ∗ ina:A ∆;Ξ⊢lettbe ∗ in∗:I ∆;Ξ⊢let ∗ be ∗ ina≡a:A ∆;Ξ⊢lettbe ∗ in∗≡t:I ∆;·⊢Atype ∆;·⊢Btype ∆;·⊢A⊗Btype ∆;Ξ⊢a:A ∆;Ξ′⊢b:B ∆;Ξ⊢t:A⊗B ∆;Ξ′,x:A,y:B⊢c:C ∆;Ξ,Ξ′⊢a⊗b:A⊗B ∆;Ξ,Ξ′⊢lettbex⊗yinc:C ∆;Ξ⊢leta⊗bbex⊗yinc:C ∆;Ξ⊢lettbex⊗yinx⊗y:A⊗B ∆;Ξ⊢leta⊗bbex⊗yinc≡c[a/x,b/y]:C ∆;Ξ⊢lettbex⊗yinx⊗y≡t:A⊗B ∆;·⊢Atype ∆;·⊢Btype ∆;·⊢A⊸Btype ∆;Ξ,x:A⊢b:B ∆;Ξ⊢f:A⊸B ∆;Ξ′⊢a:A ∆;Ξ⊢λx:Ab:A⊸B ∆;Ξ,Ξ′⊢f(a):B ∆;Ξ⊢(λx:Ab)(a):B ∆;Ξ⊢λx:Afx:A⊸B ∆;Ξ⊢(λx:Ab)(a)≡b[a/x]:B ∆;Ξ⊢λx:Afx≡f :A⊸B ∆;Ξctxt ∆;Ξ⊢t:⊤ ∆;·⊢⊤type ∆;Ξ⊢hi:⊤ ∆;Ξ⊢t≡hi:⊤ ∆;·⊢Atype ∆;·⊢Btype ∆;Ξ⊢a:A ∆;Ξ⊢b:B ∆;·⊢A&Btype ∆;Ξ⊢ha,bi:A&B ∆;Ξ⊢t:A&B ∆;Ξ⊢t:A&B ∆;Ξ⊢fst(t):A ∆;Ξ⊢snd(t):B ∆;Ξ⊢fst(ha,bi):A ∆;Ξ⊢snd(ha,bi):B ∆;Ξ⊢fst(ha,bi)≡a:A ∆;Ξ⊢snd(ha,bi)≡b:B ∆;Ξ⊢hfst(t),snd(t)i:A&B ∆;Ξ⊢hfst(t),snd(t)i≡t:A&B ∆;Ξ⊢t:0 ∆;Ξ⊢t:0 ∆;·⊢0type ∆;Ξ,Ξ′⊢false(t):B ∆;Ξ⊢false(t)≡t:0 ∆;·⊢Atype ∆;·⊢Btype ∆;·⊢A⊕Btype ∆;Ξ⊢a:A ∆;Ξ⊢b:B ∆;Ξ⊢inl(a):A⊕B ∆;Ξ⊢inr(b):A⊕B ∆;Ξ,x:A⊢c:C ∆;Ξ,y:B⊢d:C ∆;Ξ′⊢t:A⊕B ∆;Ξ,Ξ′⊢casetofinl(x)→c||inr(y)→d:C ∆;Ξ,Ξ′⊢caseinl(a)ofinl(x)→c||inr(y)→d:C ∆;Ξ,Ξ′⊢caseinl(a)ofinl(x)→c||inr(y)→d≡c[a/x]:C ∆;Ξ,Ξ′⊢caseinr(b)ofinl(x)→c||inr(y)→d:C ∆;Ξ,Ξ′⊢caseinr(b)ofinl(x)→c||inr(y)→d≡d[b/y]:C ∆;Ξ,Ξ′⊢casetofinl(x)→inl(x)||inr(y)→inr(y):A⊕B ∆;Ξ,Ξ′⊢casetofinl(x)→inl(x)||inr(y)→inr(y)≡t:A⊕B A Categorical Semantics for Linear Logical Frameworks 7 ∆;·⊢Atype ∆;·⊢!Atype ∆;·⊢a:A ∆;Ξ⊢t:!A ∆,x:A;Ξ′⊢b:B ∆;·⊢!a:!A ∆;Ξ,Ξ′⊢lettbe!xinb:B ∆;Ξ⊢let!abe!xinb:B ∆;Ξ⊢lettbe!xin!x:!A ∆;Ξ⊢let!abe!xinb≡b[a/x]:B ∆;Ξ⊢lettbe!xin!x≡t:!A Fig.6.Rulesfortheusuallineartypeformersineachcontext(I-F,-I,-E,-C,-U,⊗-F, -I,-E,-C,-U,⊸-F,-I,-E,-C,-U,⊤-F,-I,-U,&-F,-I,-E1,-E2,-C1,-C2,-U,0-F,-E, -U,⊕-F, -I1,-I2, -E, -C1, -C2, -U, !-F,-I, -E, -C, -U). Finally, we add rules that say we have all the possible commuting conver- sions,which from a syntactic point of view restorethe subformulaproperty and from a semantic point of view say that our rules are natural transformations (between hom-functors),whichsimplifies the categoricalsemantics significantly. We representthese schematically, following [15]. That is, if C[−] is a linear pro- gram context, i.e. a context built without using !, then (abusing notation and dealingwith allthe let be in-constructorsin onego)the followingrules hold. ∆;Ξ⊢C[letabebinc]:D ∆;Ξ⊢C[false(t)]:D ∆;Ξ⊢C[letabebinc]≡letabebinC[c]:D ∆;Ξ⊢C[false(t)]≡false(t):D ifC[−]doesnotbindanyfreevariablesinaorb; ifC[−]doesnotbindanyfreevariablesint; ∆;Ξ⊢C[casetofinl(x)→c||inr(y)→d]:D ∆;Ξ⊢C[casetofinl(x)→c||inr(y)→d]≡casetofinl(x)→C[c]||inr(y)→C[d]:D ifC[−]doesnotbindanyfreevariablesintorxory. Fig.7. Commuting conversions. Remark 1. Note that all type formers that are defined context-wise (I, ⊗, ⊸, ⊤,&,0, ⊕,and!)areautomaticallypreservedunderthe substitutions fromInt- Ty-Subst (up to canonicalisomorphism4), in the sense that F(A ,...,A )[a/x] 1 n is isomorphic to F(A [a/x],...,A [a/x]) for an n-ary type former F. Similarly, 1 n for T = Σ or Π, we have that (T C)[a/x] is isomorphic to T C[a/x] !y:!B !y:!B[a/x] and (Id (b,b′))[a/x] is isomorphic to Id (b[a/x],b′[a/x]). This gives us !B !B[a/x] Beck-Chevalley conditions in the categoricalsemantics. Remark 2. ThereadercannotethattheusualformulationofuniversesforDTT transfers very naturally to ILDTT, giving us a notion of universes for linear types.This allowsus to write rules for formingtypes as rules for formingterms, as usual.We do not choosethis approachanddefine the varioustype formersin the setting without universes. 4 By an isomorphism of types ∆;·⊢Atype and ∆;·⊢B type in context ∆, we here mean a pair of terms ∆;x :A⊢ f :B and ∆;y :B ⊢g :A together with a pair of judgemental equalities ∆;x:A⊢g[f/y]≡x:A and ∆;y:B⊢f[g/x]≡y:B. 8 Matthijs V´ak´ar Some Basic Results As the focus of this paper is the syntax-semanticscorre- spondence, we will only briefly state a few syntactic results. For some standard metatheoretic properties for (a system equivalent to) the ⊸,Π,⊤,&-fragment of our syntax, we refer the reader to [4]. Standard techniques and some small adaptationsofthesystemshouldbeenoughtoextendtheresultstoallofILDTT. We will only note the consistency of ILDTT both as a type theory (not, for all ∆;Ξ ⊢ a,a′ : A, ∆;Ξ ⊢ a ≡ a′ : A) and as a logic (ILDTT does not prove that every type is inhabited). Theorem 1 (Consistency). ILDTT with all its type formers is consistent, both as a type theory and as a logic. Proof (sketch). This follows from model-theoretic considerations. Later, in sec- tion 3, we shall see that our model theory encompasses that of DTT, for which we have models exhibiting both types of consistency. TogivethereadersomeintuitionfortheselinearΠ-andΣ-types,wesuggest the following two interpretations. Theorem 2 (Π and Σ as Dependent !(−)⊸(−) and !(−)⊗(−)). Suppose we have !-types. Let ∆,x:A;·⊢B type, where x is not free in B. Then, 1. Π B is isomorphic to !A⊸B, if we have Π-types and ⊸-types; !x:!A 2. Σ B is isomorphic to !A⊗B, if we have Σ-types and ⊗-types. !x:!A In particular, we have the following stronger version of a special case. Theorem 3 (! as ΣI). Suppose we have Σ- and I-types. Let ∆;· ⊢ A type. Then, Σ I satisfies the rules for !A. Conversely, if we have !- and I-types, !x:!A then !A satisfies the rules for Σ I. !x:!A AsecondinterpretationisthatΠ andΣ generalise&and⊕.Indeed,theidea is that that (or their infinitary equivalents) is what they reduce to when taken overdiscretetypes.Thesubtletyinthisresultisthedefinitionofadiscretetype. The same phenomenon is observed in a different context in section 4. For our purposes, a discrete type is a strong sum of ⊤ (a sum with a de- pendent -E-rule). Let us for simplicity limit ourselves to the binary case. For us, the discrete type with two elements will be 2 = ⊤ ⊕ ⊤, where ⊕ has a strong/dependent -E-rule (note that this is not our ⊕-E). Explicitly, 2 is a type with the following -F-, -I-, and -E-rules (and the obvious -C- and -U-rules): ∆;·⊢2type ∆;·⊢tt:2 ∆;·⊢ff:2 ∆,x:2;·⊢Atype ∆;·⊢t:2 ∆;Ξ⊢att:A[tt/x] ∆;Ξ⊢aff :A[ff/x] ∆;Ξ⊢iftthenattelseaff :A[t/x] Fig.8.Rulesforadiscretetype2,with -C-and-U-rulesomitted forreasons ofspace. Theorem 4 (Π and Σ as Infinitary Non-Discrete & and ⊕). If we have a discrete type 2 and a type family ∆,x:2;·⊢A, then 1. Π A satisfies the rules for A[tt/x]&A[ff/x]; !x:!2 2. Σ A satisfies the rules for A[tt/x]⊕A[ff/x]. !x:!2 A Categorical Semantics for Linear Logical Frameworks 9 3 Categorical Semantics We now introduce a notion of categorical model for which soundness and com- pleteness results hold with respect to the syntax of ILDTT in presence of I- and ⊗-types5. This notion of model will prove to be particularly useful when thinking about various (extensional) type formers. Definition 1. By a strict indexed symmetric monoidal category with compre- hension, we will mean the following data. 1. A category C with a terminal object ·. 2. A strict indexed symmetric monoidal category L over C, i.e. a contravariant functorLintothecategorySMCatof(small) symmetricmonoidal categories and strong monoidal functors Cop −L→ SMCat. We will also write −{f} := L(f) for the action of L on a morphism f of C. 3. A comprehension schema, i.e. for each ∆ ∈ ob(C) and A ∈ ob(L(∆)) a representation for the functor x7→L(dom(x))(I,A{x}):(C/∆)op −→Set. We will write its representing object6 ∆.A p−∆→,A ∆ ∈ ob(C/∆) and univer- sal element v ∈ L(∆.A)(I,A{p }). We will write a 7→ hf,ai for the ∆,A ∆,A isomorphism L(∆′)(I,A{f})∼=C/∆(f,p ), if ∆′ −f→∆. ∆,A Remark 3. Notethatthisnotionofmodelreducestoastandardnotionofmodel forDTTinthecasethemonoidalstructuresonthefibrecategoriesareCartesian: a reformulation of split comprehension categories with 1- and ×-types. To get a precise fit with the syntax, the extra demand called “fullness” is usually put on these [17]. The fact that we leave out this last condition precisely allows for non-trivial !-types (i.e. ones such that !A ≇ A) in our models of ILDTT. Every modelofDTTis,inparticular,a(degenerate)modelofILDTT,though.Wewill see that the type formers of ILDTT also generalise those of DTT. Theorem 5 (Soundness). We can soundly interpret ILDTT with I- and ⊗- typesinastrictindexedsymmetricmonoidalcategory(C,L)withcomprehension. Proof (sketch). The ideais thatacontext∆;Ξ willbe (inductively)interpreted byapairofobjects[[∆]] ∈ob(C),[[Ξ]] ∈ob(L([[∆]]),atypeAincontext∆;·byan [[a]] object [[A]] of L([[∆]]), and a term a:A in context∆;Ξ by a morphism[[Ξ]] −→ [[A]] ∈L[[∆]]).Generally,theinterpretationofthepropositionallineartypetheory in intuitionistic context ∆;· will happen in L(∆) as would be expected. The crux is that Int-C-Ext ([[∆,x : A]] := dom(p )), Int-Var ([[∆,x : [[∆]],[[A]] A;· ⊢ x : A]] := v ), and Int-Subst (by L(hid ,ai) are interpreted through ∆,A ∆ the comprehension, as is Int-Weak (through L of the obvious morphism in C). Finally, Soundness is a trivial verification. 5 In case we are interested in the case without I- and ⊗-types, the semantics easily generalises to strict indexed symmetric multicategories with comprehension. 6 Really,∆.MAp∆−,→MA∆wouldbeabetternotation,wherewethinkofL⊣M asan adjunction inducing!, butit would be veryverbose. 10 Matthijs V´ak´ar Theorem 6 (Completeness). In fact, this interpretation is complete. Proof (sketch). We see this through the construction of a syntactic category. Infact,wewouldliketosaythatthesyntaxisevenaninternallanguageforsuch categories. This is almost true, can be made entirely true by either putting the restrictionon our notionof model that excludes any non-trivialmorphisms into objects that are not of the form ∆.A. Alternatively, we can extend the syntax to talk about context morphisms explicitly [18]. Following the DTT tradition, we have opted against the latter. Wewillnextcharacterisethecategoricaldescriptionofthevarioustypeformers. First, we note the following. Theorem 7 (Comprehension Functor). A comprehension schema (p,v) on M astrictindexedsymmetricmonoidal category(C,L)definesamorphism L−→I of indexed categories, where I is thefull sub-indexedcategory of C/−(by making a choice of pullbacks) on the objects of the form p and where ∆,A M∆(A−a→B):=p∆,A hp∆,A,a{p∆,A}◦v∆,A✲i p∆,B. NotethatI isadisplaymapcategoryandhenceamodelofDTT[17].Wewill think ofit asthe intuitionistic contentofL. We willsee thatthe comprehension functor will give us a unique candidate for !-types: ! := LM, where L ⊣ M is a monoidal adjunction. We conclude that, in ILDTT, the !-modality is uniquely determinedbytheindexing.Thisisworthnoting,because,inpropositionallinear type theory, we might have many different candidates for !-types. Theorem 8 (Semantic Type Formers). For the other type formers, we have the following. A model (C,L,p,v) of ILDTT with I- and ⊗-types... 1. ...supports Σ-types iff all the pullback functors L(p ) have left adjoints ∆,A Σ that satisfy the Beck-Chevalley condition in the sense that the canon- !A ical map Σ ◦L(q ) −→ L(f)◦Σ is an iso, where ∆′ −f→ ∆ and !A{f} f,A !A qf,A :=hf◦p∆′,A{f},v∆′,A{f}i, and that satisfy Frobenius reciprocity in the sense that the canonical morphism Σ (Ξ′{p }⊗B)−→Ξ′⊗Σ B is an !A ∆,A !A isomorphism , for all Ξ′ ∈L(∆), B ∈L(∆.A) . 2. ...supports Π-types iff all the pullback functors L(p ) have right adjoints ∆,A Π that satisfy the dual Beck-Chevalley condition for pullbacks of the form !A (∗): the canonical L(f)◦Π −→Π ◦L(q ) is an iso. !A !A{f} f,A 3. ...supports ⊸-types iff L factors over the category SMCCat of symmetric monoidal closed categories and their homomorphisms. 4. ...supports ⊤- and &-types iff L factors over the category SMCCat of Carte- siancategorieswithsymmetricmonoidalstructureandtheirhomomorphisms. 5. ...supports 0- and ⊕-types iff L factors over the category dSMcCCat of co- Cartesian categories with a distributive symmetric monoidal structure and their homomorphisms.