Modal type theory

Just as type theory can be regarded as a generalization of logic, with types being a generalization of propositions, modal type theory is a generalization of modal logic. Specifically, just as modal logic is enhanced with one or more modal operators, which are unary operations on propositions, modal type theory is enhanced with similar unary operations on types.

Mode theories

The most classical operators in modal logic are “it is necessary that” (traditionally written □) and “it is possible that” (traditionally written ◇), but modern modal logic studies many other operators as well. Similarly, in modal type theory there are many different kinds of modal operators, with names like “discrete”, “codiscrete”, “shape”, “later”, “always”, “opposite”, “twisted”, and others.

Narya implements an extension of Multimodal Type Theory (MTT), which is a general framework for describing type theories equipped with modal operators. MTT is parametrized by a mode theory, which specifies not only the modal operators, but also the classes of types they can be applied to and their relationships.

The basic ingredient of a mode theory is a 2-category. Its objects are called modes, and specify the “classes of types” that exist in the theory: each mode has its own separate ordinary type theory. The morphisms of the mode theory are called modalities: each may induce a modal operator that is a functor mapping types of its source mode to types of its target mode. Finally, the 2-cells of the mode theory specify natural transformations relating the modal operators to each other. Just as ordinary dependent type theory has semantics in any (∞-)topos, modal type theory has semantics in any diagram of (∞-)toposes indexed by its mode 2-category: the functors between such toposes are required to preserve finite limits, but in general nothing more.

Although Narya supports arbitrary mode theories, at present there is no way for the user to specify a mode theory directly: all mode theories have to be coded in OCaml and built in to Narya at compile-time. This limitation will be overcome in the future, but it is tricky because specifying a mode theory involves not only defining a 2-category but also giving algorithms for computing with it, specifically for finding 2-cells and testing whether two composites of 2-cells are equal.

Fortunately, AI coding agents are quite good at implementing new mode theories, given a description of the 2-category and using the existing ones as templates. So if you want a mode theory that Narya doesn’t supply yet, just ask, and you may get it quickly. (Although if your mode theory is complicated, you may need to do some work specifying an algorithm for computing with the 2-cells; AI can’t always figure out such an algorithm itself.)

The currently available mode theories are selected by command-line flags, and are summarized in a table under Mode theories, below. For illustration purposes, in the rest of this section we will use the following example mode theories:

• -functor, which has two modes DomType and CodType and a morphism ○ : DomType → CodType.

• -composable-functors, which has three modes AType, BType, and CType, and morphisms ○ : AType → BType and ▱ : BType → CType.

• -adjunction, which has two modes Type and Disc, and morphisms △ : Disc → Type and □ : Type → Disc that are adjoint, △ ⊣ □.

Modes

In Narya, the name of a mode is the same as the name of the universe whose elements are types at that mode. In particular, the usual universe name Type is actually the name of the unique mode of the default trivial mode theory (as well as the mode of most single-moded theories). Each mode theory specifies default names for its modes, as shown in the table at Mode theories. But you can override these defaults with the -modes command-line flag; this should be passed a comma-separated list of names to be used in place of the defaults, in the order listed in the table for each mode theory.

Because universes are types, their names inhabit the same name domain as keywords and constant names. But they are not namespaced, and take precedence over user-defined constants. For instance, in a mode theory with a mode called Type, you cannot also define a constant named Type unless you have renamed that mode.

In general, the mode of a compound type or term is deduced automatically from those of its components. It may occasionally happen that Narya is unable to do this and will report an error; in that case you can add an explicit ascription such as : Type (this is one rare situation in which you may want to write a : A : Type, although a : (A : Type) is still easier to read).

Modalities

For technical reasons, the underlying category of a mode theory 2-category in Narya is always a freely generated category (a 2-category with this property is called flexible or cofibrant). This is not a semantically significant restriction, because every 2-category is equivalent to one whose underlying 1-category is free (known as its “strictification” or “cofibrant replacement”).

Thus, each mode theory specifies a “directed multigraph” or “quiver”, whose vertices are the modes and whose edges are generating modalities. General modalities are then free composites of generating ones. (The identity modality at each mode is, of course, the composite of zero generators.)

Each generating modality has a name, which must be a valid identifier but belongs to a separate name domain from keywords and user constants. Thus, there can be both a modality named ♭ and a constant named ♭. In fact, this sort of “punning” is actually recommended, with the constant ♭ being the internalized modal operator (see Modal datatypes and Modal records and codata) induced by the modality ♭. Each mode theory specifies default names for its modalities, shown in the table at Mode theories; you can override these with the -modalities command-line flag, which should be passed a comma-separated list of names to be used in place of the defaults, in the order listed in the table for each mode theory.

Composite modalities are named by a space-separated sequence of generators, in “applicative order”: if μ is a modality from mode p to mode q, and ν is a modality from mode q to mode r, then ν μ is the composite modality from mode p to mode r. In addition, if all the modalities in a mode theory have single-unicode-character names (as is the case for the default names of most mode theories), then they can be written without spaces in between, for instance △□ in the coreflection theory.

The primary place that modality names appear in code is as annotations, which are written as

(x :μ| A)

where x is a variable, or sometimes a term, and A is a type, or sometimes a placeholder _. (Modality names can also appear in the names of composite keys; see Modal cells.)

Such annotations appear as the domains of Modal function-types, as the arguments of constructors of Modal datatypes, as discriminees in Windowed matches, as self-variables and projection heads for Modal records and codata, and in Modal let-bindings. Since modality names are required to be valid identifiers, they are lexed separately from the symbols : and |, so no spaces are required in :μ| no matter what the name of μ. However, if the modality is a composite and not all modality names are single characters, then spaces are required between the generators.

In addition, a mode theory can mark some modalities as having further properties, which will be discussed below in appropriate sections.

• A tangible modality can appear in the domain of Modal function-types and the arguments of constructors of Modal datatypes.

• A pellucid modality can appear as the window in Windowed matches.

• A transparent modality can appear as the window in Windowed matches against non-recursive datatypes.

• A translucent modality can appear as the window in Windowed matches against non-recursive datatypes with only one constructor.

• A sinister modality must be a left adjoint in the mode theory, and can appear on the self variable of Modal records and codata.

• A discrete modality trivializes parametricity on its image; see Discrete modalities.

• A locker modality, which must be discrete, guards the application of parametricity; see Modally guarded parametricity.

Modal cells

The 2-cells in the mode theory are also specified by generators. For instance, in the -adjunction mode theory there are generating cells η : 1 ⇒ □△ and ε : △□ ⇒ 1. “Horizontal” composites of these 2-cells (that is, composites along 0-cells, i.e. along modes), in applicative order (same order as modality composition) are named by combining them with a dot ., so for instance η.η : 1 ⇒ □△□△. Horizontal composites with identity cells, a.k.a. “whiskering”, are notated by combining generating cells with modality names, so for instance □△.η : □△ ⇒ □△□△.

Accordingly, cell names inhabit the same domain as modality names, and cannot conflict with them; and if all modalities are single characters, cell names cannot be concatenations of modality names. Each mode theory gives names to all its generators; those that are “important” can be renamed appear in the tables at Mode theories and can be renamed with the command-line -modalcells flag.

There is no syntax for notating “vertical” composites (composites along 1-cells, i.e. along modalities), because the only place that 2-cell names appear in code is as key operations on terms, and keying by a vertical composite is the same as keying by each cell individually. See Keys.

The 2-cells are not freely generated by the generators; in most cases they satisfy some equations. However, those equations are not implemented by any sort of reduction but only when testing for equality.

It is also worth noting that many mode theories are locally posetal, meaning that there is at most one 2-cell (up to equality) between any two parallel modalities. In this case, it is never necessary for the user to refer to 2-cells at all; they are always found automatically when they exist.

Modal contexts

Using modal type theory requires a bit more attention to “contexts” than using ordinary type theory. The context of a term is what would be displayed above the line if you replace that term by a hole and display the hole: it lists all the variables that are in scope at that point.

Locks and annotations

In modal type theory, every context has a mode, which is the same as the mode of the term being defined in that context (and its type). MTT additionally extends the notion of context in two ways: locks and annotations.

• If μ is a modality from mode p to mode q, then a context at mode q can be locked by μ to produce a context at mode p.

• Every variable in a context is annotated by some modality whose target is the mode of the context. A variable of type A annotated by μ is denoted x :μ| A. If μ is a modality from mode p to mode q, so that the context has mode q, then the type A has mode p, and is defined in a context consisting of the previous variables that is locked by μ to make it be at mode p.

Semantically, a variable x :μ| A is equivalent to a variable belonging to μ A, meaning the modal operator associated to μ applied to A. But syntactically, modally annotated variables are more primitive, with modal operators being characterized by a universal property that refers to modal variables and context locks. The semantic meaning of a context lock is a “left adjoint” to the modal operator.

When displaying a context, such as the context of a hole, variable annotations are printed x :μ| A as above, while each variable that is behind nonidentity locks is shown as locked by the composite of those locks. Ordinary variables x : A are simply those annotated by an identity modality.

Keys

Annotations and locks interact by way of key 2-cells: when a variable in a context is accessed, there must be a key 2-cell from its annotation to the composite of all locks to its right in the context. (Hence, in particular, those two modalities must have the same source; they always have the some target, namely the mode of the context at the point when the variable was added to it.)

More generally, a key can be applied to any term. The effect of a key by some 2-cell α : μ ⇒ ν is that if the context in which that term is being typechecked ends with a lock by ν, then that lock is replaced by a lock by μ while typechecking the body of the term itself. This generalizes the previous remark about variables if we take as basic that a variable can always be used when the composite of locks to its right is exactly equal to its annotation.

In full generality, the user must specify the 2-cell to use as a key. The notation for keys is #keyname, applied to a term postfix with the same parsing behavior as a field projection .fld. Multiple keys in sequence are applied from left to right, like function arguments and fields, and since key action is covariant that means a multiple key like #α #β indicates the composite of α first and then β. Thus, for instance, to key x by the vertical composite of △.η : △ ⇒ △□△ and ε.△ : △□△ ⇒ △, write x #△.η #ε.△ (which is equal to x, by an adjunction identity). Note also that since the key need only match the tail end of the locks in the context, this can also be written as x #η #ε.△.

However, often it is not necessary to specify keys explicitly: if Narya can determine that there is a unique 2-cell that would work as a key, it will insert it automatically and silently. Each mode theory supplies an algorithm for finding such unique 2-cells, and often this is all you need. In particular, many of the supplied mode theories are locally posetal, meaning that any two parallel 2-cells are equal, and so all extant 2-cells can always be found uniquely. And even for mode theories that are not locally posetal, in small cases keys are often unique.

Modal function-types

Since the only Built-in types are universes and functions, in modal type theory we must make both of these modally-aware. As mentioned in Modes, each mode induces an eponymous universe type. For functions, we have a modal function-type written

(x :μ| A) → B

In this syntax:

• μ is a modality (perhaps a generating one or a composite of generators) from some mode p to some mode q. To be used this way, the modality μ must be tangible. (In most mode theories, most or all modalities are tangible.)

• A is a type at mode p, defined in the current context locked by μ.

• B is a type at mode q defined in the current context extended by a variable x of type A that is annotated by μ.

The entire expression (x :μ| A) → B is then a type at mode q. And since parameters of a definition are really just function arguments, the same syntax can be used for them:

def foo (x :μ| A) : B ≔ ...

Elements of the type (x :μ| A) → B, called modal functions, are defined by abstraction and used by application, like ordinary functions. However:

• In an application f a where f : (x :μ| A) → B, the argument a is typechecked in the current context locked by μ.

• In an abstraction (x ↦ M) : (x :μ| A) → B, the body M is typechecked in the current context extended by a variable x of type A annotated by μ. Modally, ascribed abstractions such as (x :μ| A) ↦ M are also allowed, and synthesize if the body M synthesizes.

Semantically, a modal function in (x :μ| A) → B is equivalent to a function (x : μ A) → B where μ A denotes application of the modal operator associated to the modality μ. However, syntactically modal functions are, in a sense, more basic, with the modal operator determined by a universal property using modal functions.

In general, higher-dimensional versions of modal function-types behave like those of ordinary function-types. For instance, if f : (x :μ| A) → B then

refl f : {x₀ :μ| A} {x₁ :μ| A} (x₂ :μ| Id A x₀ x₁) → Id B (f x₀) (f x₁)

For the exception, see Discrete modalities.

Modal datatypes

The semantic equivalence between (x :μ| A) → B and (x : μ A) → B suggests that μ A is characterized by a positive universal property, making it similar to a datatype. Taking this seriously, Narya allows the definition of arbitrary modal datatypes, of which positive modal operators are a simple special case.

Modal constructors

Any argument of any constructor of any datatype can be modally annotated, as with the domain of a modal function. (As in that case, the modality must be tangible.) A modal operator is then the particular case of a single-argument single-constructor datatype (which is trivial if not modally annotated). For instance, the functor operator induced by the modality ○ : DomType → CodType in the -functor mode theory can be defined by

def ○ (A :○| DomType) : CodType ≔ data [ circ. (x :○| A) ]

Note that the type A must be a modal variable, so that it can be accessed behind the lock induced by the annotation in the argument.

The constructor circ. then behaves like a modal function (x :○| A) → ○ A. And we can match against an element of ○ A, obtaining a modal variable:

def foo (A :○| DomType) (u : ○ A) : B ≔ match u [ circ. x ↦ ? ]

Here in the hole we have a variable x :○| A. This says essentially that circ. : (x :○| A) → ○ A is the “universal modal function” with its domain.

In general, higher-dimensional versions of modal datatypes behave like those of ordinary datatypes. For instance, we have

Id ○ : {A₀ :○| DomType} {A₁ :○| DomType} (A₂ :○| Id DomType A₀ A₁)
         →⁽ᵉ⁾ Id CodType (○ A₀) (○ A₁)

and Id ○ A₂ behaves like an indexed datatype ○ A₀ → ○ A₁ → CodType with a single constructor

circ. {x₀ :○| A₀} {x₁ :○| A₁} (x₂ :○| A₂ x₀ x₁) : Id ○ A₂ (circ. x₀) (circ. x₁)

For the exception, see Discrete modalities.

Windowed matches

Ordinary matches on modal datatypes, however, are insufficient in general to prove basic facts like the functoriality of modal operators. For instance, in the -composable-functors mode theory, with modalities ○ : AType → BType and ▱ : BType → CType, if we define modal operators for both generating modalities and their composite:

def ○ (X :○| AType) : BType ≔ data [ circ. (_ :○| X) ]

def ▱ (Y :▱| BType) : CType ≔ data [ par. (_ :▱| Y) ]

def ▱○ (X :▱○| AType) : CType ≔ data [ parcirc. (_ :▱○| X) ]

then we can define a transformation from ▱○ X to ▱ (○ X):

def colax (X :▱○| AType) (u : ▱○ X) : ▱ (○ X) ≔ match u [
| parcirc. x ↦ par. (circ. x)]

but attempting to define a transformation the other way runs into a problem. We start with the obvious

def lax (X :▱○| AType) (u : ▱ (○ X)) : ▱○ X ≔ match u [
| par. y ↦ ? ]

We would now like to match on y, destructing it into circ. x, and return parcirc. x. But in the hole context we have y :▱| ○ X, and in fact y doesn’t even live at the mode CType where we are working, so it seems that an ordinary match y would be impossible.

In MTT this problem is solved by window modalities. The discriminee of a match can be annotated by a modality, called a “window modality”. In this case it is checked or synthesized in a context locked by that window modality, and the window modality is composed with any annotations on the pattern variables in the baranches of the resulting match (to put them at the correct mode).

In particular, in the above case we can write

def lax (X :▱○| AType) (u : ▱ (○ X)) : ▱○ X ≔ match u [
| par. y ↦ match (y :▱| _) [ circ. x ↦ ? ]]

The placeholder _ stands for the datatype that y belongs to, which can be used instead if desired:

def lax (X :▱○| AType) (u : ▱ (○ X)) : ▱○ X ≔ match u [
| par. y ↦ match (y :▱| ○ X) [ circ. x ↦ ? ]]

Now in the hole we have x :▱○| X, annotated by the composite modality ▱○, so we can fill the hole with parcirc. x as desired.

def lax (X :▱○| AType) (u : ▱ (○ X)) : ▱○ X ≔ match u [
| par. y ↦ match (y :▱| _) [ circ. x ↦ parcirc. x ]]

In general, the correct window modality for a match cannot be deduced automatically, and must be supplied by the user with an annotation of this sort. However, there is one case in which a window modality is inferred automatically: if the term being matched against is a free variable with a modal annotation on it, then it obviously needs some window modality, and the obvious choice is the same one as its annotation. This is the case in the example of lax above, so we actually can also write

def lax (X :▱○| AType) (u : ▱ (○ X)) : ▱○ X ≔ match u [
| par. y ↦ match y [ circ. x ↦ parcirc. x ]]

but it’s important to realize that the window modality is implicitly present even in this case. In addition, even for a variable this is not always the correct choice: you might want to use a different window modality that’s related to the variable’s annotation by a key, in which case the window needs to be given explicitly.

In principle, a window modality can be applied to any match: the datatype doesn’t have to have any modal constructors itself. However, this has consequences for the semantics of the window modality: it necessarily “preserves” all datatypes that it can be a window for. Since this may be undesired, Narya allows a mode theory to specify three levels of “transparency” for modalities governing their applicability as windows. (These are unrelated to the similarly-named attributes of record types.)

• A pellucid modality can be a window for any match at all. This is a very strong property: it implies, for instance, that the modal operator preserves recursive datatypes such as the natural numbers. The only nonidentity pellucid modality in the standard mode theories is △ in -tconn; this is semantically justified because it is the inverse image of a locally connected geometric morphism, so it preserves both colimits and function-types, out of which inductive types are constructed (at least in Grothendieck topoi) by transfinite iteration. (Some additional modalities are pellucid in discrete mode theories.)

• A transparent modality can be a window for a match on any non-recursive datatype. This means that the modal operator preserves finite colimits (or, at least, finite coproducts; other finite colimits must wait for Higher inductive types). Since left adjoints preserve colimits, all the left adjoints in the standard mode theories are transparent, such as △ in most theories that have it. In addition, there is a variant of -functor called -transparent-functor that makes the modality ○ transparent.

• A translucent modality can be a window for a match on any non-recursive single-constructor datatype. This is the minimum necessary to ensure we can prove functoriality of modal operators, as above. All the modalities in the standard mode theories are translucent (though some in discrete mode theories are not).

A translucent modality can also be a window for indexed single-constructor non-recursive datatypes, which in particular means it preserves the Martin-Löf identity type, and therefore preserves finite limits internally. However, even a non-translucent modality preserves finite products, and in the standard categorical semantics it must preserve at least pullbacks of display maps. Moreover, when Higher Observational Type Theory is on, all modal operators preserve the observational identity types; this follows from the remarks above about higher-dimensional versions of modal datatypes. Thus, one should really think of all modal operators as semantically corresponding to finite-limit-preserving functors. (This is particularly convenient for applications to topos theory, in which a geometric morphism is an adjoint pair of finite-limit-preserving functors.)

Modal records and codata

The “positive” modal operators obtained as a special case of modal datatypes are the only ones present in the original theory MTT. Narya also implements an enhancement called Multimodal Adjoint Type Theory (MATT), based on an earlier type theory called FitchTT from Modalities and Parametric Adjoints. FitchTT and MATT add “negative” modal operators to MTT, and in Narya these are a special case of modal records and codatatypes.

Dually to modal constructors of datatypes, any record or codatatype can have modal fields. And just as a modal constructor can be viewed as a modal function, so can a modal field. But now since the domain of a field-qua-function is the record/codata type itself, that is what gets modally annotated.

For technical reasons, the modality which is used in such an annotation is required to have a right adjoint (that is, to be a left adjoint) in the mode 2-category. Each mode theory can mark some of its modalities as sinister by supplying a right adjoint to them; they can then annotate modal fields. All left adjoints in the standard mode theories are sinister.)

The simplest sort of modal codatatype has one field that is modally annotated. For instance, in the mode theory -adjunction the modality △ : Disc → Type is sinister, with left adjoint □ : Type → Disc, and so we can define:

def □ (A :□| Type) : Disc ≔ codata [
| (x :△| _) .unbox : A ]

The placeholder _ stands for the codatatype being defined, which can be used instead if desired:

def □ (A :□| Type) : Disc ≔ codata [
| (x :△| □ A) .unbox : A ]

Note that the △-annotation appears on the self-variable x to which the field .unbox is applied. We have named the modal operator □, the right adjoint of △, because it goes in that direction, and indeed is equivalent to the positive modal operator associated to □. Thus, the modal operators that can be defined negatively are the right adjoints (whose left adjoints are sinister).

Note also that A itself is □-annotated and lives at the mode Type, the domain of □. In general, the type of a modal field is typechecked in a context locked by the right adjoint, which in the above case is □ so that we can use the □-annotated variable A.

Similarly, when defining an element of a modal codatatype by comatching, the value corresponding to a modal field is typechecked in a context locked by the right adjoint:

def box (A :□| Type) (a :□| A) : □ A ≔ [
| .unbox ↦ a ]

When projecting a modal field from an element of a modal datatype, however, the element is typechecked in a context locked by the left adjoint. Unfortunately, Narya can’t infer this modality from the field name, because the same field name could be used by many different codatatypes with different modal annotations: the only way to find the correct codatatype is to synthesize a type for the element being projected, but that can’t be done until we already have the modality to lock the context to synthesize it in! Therefore, the element being projected must be explicitly annotated with that left adjoint modality, mirroring the self variable in the codata definition.

def unbox (A :△□| Type) (u :△| □ A) : A ≔ (u :△| _) .unbox

Once again, you can also write (u :△| □ A) .unbox if desired.

The unit and counit of the adjunction △ ⊣ □ are used in the reduction and equality-checking rules. For instance, with the above definitions, in context of A :△□| Type and a :△□| A we can write unbox A (box A a), which then reduces to a but with the counit cell △□ ⇒ 1 applied as a key.

The unit cell isn’t used for modal codatatypes, but it is used for modal record types which have an η-conversion rule. To have modal fields, a record must be defined using self variables:

def □′ (A :□| Type) : Disc ≔ sig (
  (x :△| _) .unbox : A)

Then we can define

def box_unbox (A :□| Type) (u : □′ A) : □′ A ≔
  (unbox ≔ (u :△| _) .unbox)

This doesn’t reduce, but it should be equal to u by η-conversion. However, to test records for η-equality we need to project out all their fields, and in order to write (box_unbox A u :△| _) .unbox and (u :△| _) .unbox we need them to be defined in a △-locked context. Thus, internally Narya applies the unit 1 ⇒ □△ as a key first, obtaining both box_unbox A u and u in a context locked by □△, then projects out the .unbox field and compares the results for equality in the remaining □-locked context. (As a user you shouldn’t often need to be aware of this, but we mention it to justify the requirement of a full adjunction.)

In general, higher-dimensional versions of modal records and codata behave like those of ordinary records and codata. For instance, we have

Id □′ : {A₀ :□| Type} {A₁ :□| Type} (A₂ :□| Id Type A₀ A₁) → Id Disc (□′ A₀) (□′ A₁)

and Id □′ A₂ behaves like a record type with a single field

(u :△| Id □′ A₂ u₀ u₁) .unbox : A₂ ((u₀ :△| □′ A₀) .unbox) ((u₁ :△| □′ A₁) .unbox)

As before, for the exception see Discrete modalities.

Currently, higher fields cannot also be modal.

Modal let-bindings

The variable in a non-recursive let-binding can also be annotated with a modality, as in

let x :□| A ≔ M in N

As with an ordinary let-binding, this is similar to writing a function redex

((x :□| A) ↦ N) M

In particular, therefore, the type A and the value M are typechecked in a □-locked context, while the body N is checked (or synthesized) in a context extended by an annotated variable x :□| A. And also as in the non-modal case, the difference between a let-binding and a function redex is that x is bound to the value M, not just the type A, already when checking the body N.

Recursive let-bindings can not currently be modal.

Modal HOTT

The interaction of modal features with Higher Observational Type Theory is not yet fully implemented. About all that can be relied on is that the HOTT primitives should work in single-mode theories for types not involving modal features.

Mode theories

We organize the mode theories into groups to make them easier to look up. The default names for the modes, modalities, and 2-cells shown in the table can be overridden by the command-line flags -modes, -modalities, and -modalcells. There are also some additional variant mode theories, such as -transparent-functor mentioned above, and a family of “discrete mode theories” discussed under Modal parametric discreteness.

Testing mode theories

These mode theories are very simple, intended mainly for testing features. They are all locally posetal. In each case we list the modes, the generating modalities, and the generating 2-cells.

Testing mode theories

Command-line flag	Modes	Modalities	2-cells
-functor	DomType, CodType	○ : DomType → CodType	–
-composable-functors	AType, BType, CType	○ : AType → BType, ▱ : BType → CType	–
-transformation	DomMode, CodMode	○ : DomMode → CodMode, ▱ : DomMode → CodMode	α : ○ ⇒ ▱
-composable-transformations	DomMode, CodMode	○ : DomMode → CodMode, ▱ : DomMode → CodMode, ▹ : DomMode → CodMode	α : ○ ⇒ ▱, β : ▱ ⇒ ▹, βα : ○ ⇒ ▹
-interchange	AType, BType, CType	▹, ◃ : AType → BType, ▸, ◂ : BType → CType	α : ▹ ⇒ ◃, β : ▸ ⇒ ◂

Single-mode theories

These mode theories all have only one mode Type. We do not list all the generating 2-cells, but only some of the most important ones and some of their consequences. For non-locally-posetal theories, we give the names of all the generators that can be renamed, in order, followed by other cells that exist.

Single-mode theories

Command-line flag	Modalities	2-cells	Locally Posetal
-coreflector, a.k.a. -crisp	♭ : Type → Type	♭♭ ≅ ♭, ♭ ⇒ 1	yes
-reflector	♯ : Type → Type	♯♯ ≅ ♯, 1 ⇒ ♯	yes
-comonad	♭ : Type → Type	ε : ♭ ⇒ 1, δ : ♭ ⇒ ♭♭	no
-monad	♯ : Type → Type	η : 1 ⇒ ♯, μ : ♯♯ ⇒ ♯	no
-spatial	♭ : Type → Type ♯ : Type → Type	♭♭ ≅ ♭, ♭ ⇒ 1, ♯♯ ≅ ♯, 1 ⇒ ♯, ♯♭ ≅ ♯, ♭♯ ≅ ♭	yes
-cospatial	ʃ : Type → Type ♭ : Type → Type	ʃʃ ≅ ʃ, 1 ⇒ ʃ, ♭♭ ≅ ♭, ♭ ⇒ 1, ʃ♭ ≅ ♭, ♭ʃ ≅ ʃ	yes
-ambiflector	♮ : Type → Type	ø : 1 ⇒ 1, ♮ ⊣ ♮, ♮♮ ≅ ♮, 1 ⇒ ♮, ♮ ⇒ 1, ♮♮ ≅ ♮, ♮ ⊣ ♮	no

On the names for these theories that may not be self-explanatory:

• -spatial type theory was so-called in the paper Brouwer’s fixed-point theorem in real-cohesive homotopy type theory because its intended models were toposes of spaces, with ♭ assigning the discrete topology and ♯ the codiscrete one, and ♭ ⊣ ♯.

• -cospatial is the dual of -spatial, with ʃ ⊣ ♭ instead.

• -crisp type theory was so-called in the paper Internal Universes in Models of Homotopy Type Theory because its ♭-annotated variables (see below) were called “crisp” variables (taken from the previous paper).

• -ambiflector is a single functor that is both a reflector and a coreflector, adjoint to itself, as used in the paper Synthetic Spectra via a Monadic and Comonadic Modality.

Multi-mode theories

These mode theories have more than one mode, so we list the modes, as well as the generating modalities and important/renameable 2-cells. Many of these have one of the above single-mode theories as a sub-theory at the mode Type, for instance ♭ = △□ embeds -coreflector into -coreflection and so on. The common mode name Disc reflects the feature of many models in which types at that mode have “discrete” topological or higher structure; one instance of this that can be turned on in Narya is Parametrically Discrete modalities.

Multi-mode theories

Command-line flag	Modes	Modalities	2-cells	l.p.
-adjunction	Disc, Type	△ : Disc → Type, □ : Type → Disc	η : 1 ⇒ □△, ε : △□ ⇒ 1 △ ⊣ □	no
-coreflection	Disc, Type	△ : Disc → Type, □ : Type → Disc	△□ ⇒ 1, □△ ≅ 1 △ ⊣ □	yes
-local	Disc, Type	△ : Disc → Type, □ : Type → Disc ∇ : Disc → Type	△ ⊣ □ ⊣ ∇, △□ ⇒ 1, 1 ≅ □△, 1 ⇒ ∇□, □∇ ≅ 1	yes
-tconn	Disc, Type	◇ : Type → Disc, △ : Disc → Type, □ : Type → Disc	◇ ⊣ △ ⊣ □, △□ ⇒ 1, 1 ≅ □△, 1 ⇒ △◇, ◇△ ≅ 1	yes
-gwpt	Disc, Type	△ : Disc → Type, □ : Type → Disc, ◇ : Type → Disc, ∇ : Disc → Type	1⇨□△ : 1 ⇒ □△, △□⇨1 : △□ ⇒ 1, 1⇨∇◇ : 1 ⇒ ∇◇, ◇∇⇨1 : ◇∇ ⇒ 1, △ ⊣ □, ◇ ⊣ ∇ ◇∇ ≅ 1, ◇△ ≅ 1, □∇ ≅ 1	no
-ambiflection	Disc, Type	△ : Disc → Type, □ : Type → Disc	η : 1 ⇒ △□, ε : △□ ⇒ 1, ø : 1 ⇒ 1, △ ⊣ □, □ ⊣ △, □△ ≅ 1	no
-guarded	Type, Timed	△ : Type → Timed, □ : Timed → Type, ▹ : Timed → Timed	△ ⊣ □, △□ ⇒ 1, □△ ≅ 1, 1 ⇒ ▹, □▹ ≅ □	yes

On the names for these theories that may not be self-explanatory:

• -local indicates a “local geometric morphism”, which is the name in topos theory for such an adjoint triple of finite-limit-preserving functors between toposes with the outer adjoints △ and ∇ fully faithful. Note that △□ and ∇□ are an adjoint pair of a coreflector and a reflector on Type, so this contains -spatial as a sub-theory.

• -tconn is short for “totally connected geometric morphism”, which is the name in topos theory for such an adjoint triple of finite-limit-preserving functors, with the inner adjoint △ fully faithful. (The mode theory -coreflection is also known as a merely connected geometric morphism.) Dually to -local, here ◇△ and △□ are an adjoint pair of a reflector and coreflector, so this contains -cospatial as a sub-theory.

• -gwpt is short for “geometrically well-pointed topos”, meaning a geometric morphism △ ⊣ □ having a section ◇ ⊣ ∇, in the category of toposes and geometric morphisms, such that the section is a geometric embedding. This may seem like a curious mode theory; its presence is explained in Semantics of modal parametricity.

• -ambiflection is the two-mode analogue of -ambiflector, both a reflection and a coreflection.

• -guarded is a mode theory for “guarded recursion”, with ▸ called “later” and □ (or △□) called “always”; its use is described in the MTT paper.

Requests for, or contributions of, new mode theories are very welcome.