nLab !-modality



Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction setinternal homfunction type
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian productdependent productdependent product type
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijectionisomorphism/adjoint equivalenceequivalence of types
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Modalities, Closure and Reflection



In full linear logic/linear type theory there is assumed a (comonadic) modality denoted “!” and called the exponential modality, whose role is, roughly, to give linear types also a non-linear interpretation. This is also called the “of course”-modality or the storage modality, and sometimes the “bang”-operation.

In classical linear logic (meaning with involutive de Morgan duality), the de Morgan dual of “!” is denoted “?” and called the “why not”-modality.

In categorical semantics of linear type theory the !-modality typically appears as a kind of Fock space construction. If one views linear logic as quantum logic (as discussed there), then this means that the !-modality produces free second quantization.

Categorical semantics

Everyone agrees that ! should be a comonad (and ? should be a monad, see also at monads in computer science), but there are different ways to proceed from there. The goal is to capture the syntactic rules allowing assumptions of the form !A!A to be duplicated and discarded.

Intuitionistic case

The original definition from Seely, adapted to the intuitionistic case and modernized, is:


Let CC be an symmetric monoidal category with cartesian products. A Seely comonad on CC is a comonad that is a strong monoidal functor from the cartesian monoidal structure to the symmetric monoidal structure, i.e. we have !(A×B)!A!B!(A\times B)\cong !A \otimes !B and !1I!1\cong I coherently. (There is also an additional coherence axiom that should be imposed; see Mellies, section 7.3.)

(Note that in linear logic, the cartesian monoidal structure ×\times is sometimes denoted by &\&.) This implies that the Kleisli category of ! (i.e.\ the category of cofree !-coalgebras) is cartesian monoidal. If CC is closed symmetric monoidal then the Kleisli category of a cartesian closed category, which is a categorical version of the translation of intuitionistic logic into linear logic.

Of course, the above definition depends on the existence of the cartesian product. A different definition that doesn’t require the existence of ×\times was given by Benton, Bierman, de Paiva, and Hyland:


Let CC be a symmetric monoidal category; a linear exponential comonad on CC is a lax monoidal comonad such that every cofree !-coalgebra naturally carries the structure of a comonoid object in the category of coalgebras (i.e. the cofree-coalgebra functor lifts to the category of comonoids in the category of coalgebras).

It follows automatically that all !-coalgebras are comonoids, and therefore that the category of all !-coalgebras (not just the cofree ones) is cartesian monoidal. Note that for a comonad on a poset, every coalgebra is free; thus the world of pure propositional “logic” doesn’t tell us whether to consider the Kleisli category or the Eilenberg-Moore category for the translation.

A more even-handed approach is the following (see Benton (1995) and Mellies (2009)), based on the observation that both Kleisli and Eilenberg-Moore categories are instances of adjunctions.


A linear-nonlinear adjunction is a monoidal adjunction F:ML:GF \colon M \rightleftarrows L \colon G in which LL is symmetric monoidal and MM is cartesian monoidal. The induced !-modality is the comonad FGF G on LL.

This includes both of the previous definitions where MM is taken respectively to be the Kleisli category or the Eilenberg-Moore category of !. Conversely, in any linear-nonlinear adjunction the induced comonad FGF G can be shown to be a linear exponential comonad. Moreover, if !! is a linear exponential comonad on a symmetric monoidal category CC with finite products, then the cofree !-coalgebra functor is a right adjoint and hence preserves cartesian products; but the cartesian products of coalgebras are the tensor product in CC, so we have !(A×B)!A!B!(A\times B) \cong !A \otimes !B, the Seely condition.

Classical case

For “classical” linear logic, we want CC to be not just (closed) symmetric monoidal but *\ast-autonomous. If an *\ast-autonomous category has a linear exponential comonad !! one can derive a ? from the ! by de Morgan duality, ?A=(!(A *)) *?A = (!(A^*))^*. The resulting relationship between ! and ? was axiomatized in a way not requiring the de Morgan duality by Blute, Cockett & Seely (1996):


Let CC be a linearly distributive category with tensor product \otimes and cotensor product \parr. A (!,?)-modality on CC consists of:

  1. a \otimes-monoidal comonad ! and a \parr-comonoidal monad ?
  2. ? is a !-strong monad, and ! is a ?-strong comonad
  3. all free !-coalgebras are naturally commutative \otimes-comonoids, and all free ?-algebras are naturally commutative \parr-monoids.

Here a functor FF is strong with respect to a lax monoidal functor GG if there is a natural transformation FAGBF(AGB)F A \otimes G B \to F(A\otimes G B) satisfying some natural axioms, and we similarly require compatibility of the monad and comonad structure transformations. BCS96 showed that if CC is in fact *\ast-autonomous, it follows from the above definition that ?A=(!(A *)) *?A = \big(!(A^*)\big)^* as expected.


Relation to Chu construction


Suppose F:MC:GF \colon M \rightleftarrows C : G is a linear-nonlinear adjunction, where CC is closed symmetric monoidal with finite limits and colimits, and C\bot\in C is an object. Then there is an induced linear-nonlinear adjunction MChu(C,)M \rightleftarrows Chu(C,\bot) where Chu(C,)Chu(C,\bot) is the Chu construction Chu(C,)Chu(C,\bot), which is *\ast-autonomous with finite limits and colimits. Hence Chu(C,)Chu(C,\bot) admits a !-modality.


The embedding of CC in Chu(C,)Chu(C,\bot) as A(A,[A,],ev)A \mapsto (A, [A,\bot], ev) is coreflective: the coreflection of (B +,B ,e B)(B^+, B^-, e_B) is (B +,[B +,],ev)(B^+, [B^+,\bot], ev). Moreover, this subcategory is closed under the tensor product of Chu(C,)Chu(C,\bot), i.e. the embedding CChu(C,)C\hookrightarrow Chu(C,\bot) is strong monoidal, hence the adjunction is a monoidal adjunction. Therefore, the composite adjunction MCChu(C,)M \rightleftarrows C \rightleftarrows Chu(C,\bot) is again a linear-nonlinear-adjunction.

Since a Chu construction is *\ast-autonomous, this !-modality implies a dual ?-modality.


If CC is a cartesian closed category with finite limits and colimits and C\bot\in C is an object, then there is a linear-nonlinear adjunction CChu(C,)C \rightleftarrows Chu(C,\bot), and hence Chu(C,)Chu(C,\bot) admits a !-modality.


Apply the previous theorem to the identity adjunction CCC\rightleftarrows C.

Note that the !-modality obtained from the corollary is idempotent, while that obtained from the theorem is idempotent if and only if the original one was. Other ways of constructing !-modalities, such as by cofree coalgebras, may produce examples that are not idempotent.

Realization in linear homotopy type theory

In dependent linear homotopy type theory the “linear-nonlinear adjunction” is naturally identified (Ponto & Shulman (2012), Ex. 4.2, see also Schreiber (2014), Sec. 4.2) with the stabilization adjunction between homotopy types and stable homotopy types (Riley (2022), Prop. 2.1.31), whose left adjoint (forming suspension spectra Σ + \Sigma^\infty_+) is equivalently given (cf. Riley (2022), Rem. 2.4.13) by sending B:TypeB \,\colon\, Type to the linear dependent sum B𝟙(p B) !(p B) *𝟙\star_B \mathbb{1} \;\coloneqq\; (p_B)_! (p_B)^\ast \mathbb{1} over the monoidal unit in the context BB. In terms of quantum modal logic this is forming the “linear randomization” of the given classical homotopy type (its “motive”):

Girard’s original presentation of linear logic involved rules that explicitly assumed the presence of !! on hypotheses or on entire contexts, such as , dereliction?, weakening and contraction:

Γ,ABΓ,!ABΓBΓ,!ABΓ,!A,!ABΓ,!AB\frac{\Gamma, A \vdash B}{\Gamma, !A \vdash B} \qquad \frac{\Gamma \vdash B}{\Gamma, !A\vdash B} \qquad \frac{\Gamma,!A,!A \vdash B}{\Gamma, !A\vdash B}

and “promotion”:

!ΓA!Γ!A \frac{!\Gamma \vdash A}{!\Gamma\vdash !A}

If this is translated into a natural deduction style term calculus, the resulting rules are more complicated than those of most type formers. This can be avoided using adjoint type theory with two context zones, one “nonlinear” one where contraction and weakening are permitted (and admissible) and one “linear” one where they are not, with !! as a modality relating the two zones.

Such a “modal” presentation of linear logic was first introduced by Girard in his work on LU? and then developed by a number of other people such as Plotkin, Wadler, Benton, and Barber. See the references for details.

This presentation also generalizes naturally to dependent linear type theory, with the nonlinear type theory being dependent, and the linear types depending on the nonlinear ones but nothing depending on linear types. In this context, the !!-modality decomposes into “context extension” and a “dependent sum”.

\phantom{-}symbol\phantom{-}\phantom{-}in logic\phantom{-}
A\phantom{A}\inA\phantom{A}element relation
A\phantom{A}:\,:A\phantom{A}typing relation
A\phantom{A}\vdashA\phantom{A}A\phantom{A}entailment / sequentA\phantom{A}
A\phantom{A}\topA\phantom{A}A\phantom{A}true / topA\phantom{A}
A\phantom{A}\botA\phantom{A}A\phantom{A}false / bottomA\phantom{A}
A\phantom{A}\LeftrightarrowA\phantom{A}logical equivalence
A\phantom{A}\neqA\phantom{A}negation of equality / apartnessA\phantom{A}
A\phantom{A}\notinA\phantom{A}negation of element relation A\phantom{A}
A\phantom{A}¬¬\not \notA\phantom{A}negation of negationA\phantom{A}
A\phantom{A}\existsA\phantom{A}existential quantificationA\phantom{A}
A\phantom{A}\forallA\phantom{A}universal quantificationA\phantom{A}
A\phantom{A}\wedgeA\phantom{A}logical conjunction
A\phantom{A}\veeA\phantom{A}logical disjunction
symbolin type theory (propositions as types)
A\phantom{A}\toA\phantom{A}function type (implication)
A\phantom{A}×\timesA\phantom{A}product type (conjunction)
A\phantom{A}++A\phantom{A}sum type (disjunction)
A\phantom{A}00A\phantom{A}empty type (false)
A\phantom{A}11A\phantom{A}unit type (true)
A\phantom{A}==A\phantom{A}identity type (equality)
A\phantom{A}\simeqA\phantom{A}equivalence of types (logical equivalence)
A\phantom{A}\sumA\phantom{A}dependent sum type (existential quantifier)
A\phantom{A}\prodA\phantom{A}dependent product type (universal quantifier)
symbolin linear logic
A\phantom{A}\multimapA\phantom{A}A\phantom{A}linear implicationA\phantom{A}
A\phantom{A}\otimesA\phantom{A}A\phantom{A}multiplicative conjunctionA\phantom{A}
A\phantom{A}\oplusA\phantom{A}A\phantom{A}additive disjunctionA\phantom{A}
A\phantom{A}&\&A\phantom{A}A\phantom{A}additive conjunctionA\phantom{A}
A\phantom{A}\invampA\phantom{A}A\phantom{A}multiplicative disjunctionA\phantom{A}
A\phantom{A}!\;!A\phantom{A}A\phantom{A}exponential conjunctionA\phantom{A}



Brief survey in a context of computer science/linear type theory:

  • Daniel Mihályi, Valerie Novitzká, Section 2.2 of: What about Linear Logic in Computer Science?, Acta Polytechnica Hungarica 10 4 (2013) 147-160 [pdf, pdf]

On the semantics of exponential conjunction as a comonad:

Construction of such comonads based on cofree comonoids can be found in (among other places):

  • Mellies and Tabareau and Tasson, An explicit formula for the free exponential modality of linear logic. Mathematical Structures in Computer Science, 28(7), 1253-1286. doi:10.1017/S0960129516000426

  • Sergey Slavnov, On Banach spaces of sequences and free linear logic exponential modality, Math. Struct. Comp. Sci. 29 (2019) 215-242, arXiv:1509.03853

The relation to Fock space is discussed in:

The interpretation of Ω Σ + \Omega^\infty \Sigma^\infty_+ as an exponential in the context of Goodwillie calculus is due to

  • Gregory Arone, Marja Kankaanrinta, The Goodwillie tower of the identity is a logarithm, 1995 (web)

based on

The modal approach to a term calculus for the !!-modality can be found in:

  • Jean-Yves Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201-217, 1993.

  • G. Plotkin. Type theory and recursion. In Proceedings of the Eigth Symposium of Logic in Computer Science, Montreal , page 374. IEEE Computer Society Press, 1993.

  • Nick Benton, A mixed linear and non-linear logic: Proofs, terms and models, in Computer Science Logic. CSL 1994, Lecture Notes in Computer Science 933 [doi:10.1007/BFb0022251, pdf]

  • Gavin Bierman, On Intuitionistic Linear Logic, Cambridge (1993) [pdf]

  • Philip Wadler. A syntax for linear logic. In Ninth International Coference on the Mathematical Foundations of Programming Semantics , volume 802 of LNCS . Springer Verlag, April 1993

  • Andrew Barber, Dual Intuitionistic Linear Logic, Technical Report ECS-LFCS-96-347, University of Edinburgh, Edinburgh (1996), web

A quantum programming language based on this linear/non-linear type theory adunction is QWIRE:

theoretical background:

applied to verified programming after implementation in Coq:

and using ambient homotopy type theory:

In dependent linear type theory

Discussion of the exponential modality via stabilization in dependent linear homotopy type theory:

category: logic

Last revised on November 11, 2022 at 20:53:32. See the history of this page for a list of all contributions to it.