0004 Internal languages for models
This RFC is tracked in #1212.
1 Summary
Any pragmatic tool for programming inside categorical structures will allow morphisms to be denoted using variables and function applications, as in conventional programming languages. In the jargon, such a notation based on variables is called the internal language of the categorical structure. This RFC seeks a uniform method to construct the internal languages of different categorical structures, suitable for implementation in CatColab. The technical approach involves a two-level type theory parameterized by a modal double theory.
2 Motivation
Several styles of notation are commonly used to denote morphisms in a categorical structure. Among text-based notations, the most important distinction is between point-free notations, which do not involve “elements” or “variables,” and pointful notations, which do. To illustrate, suppose that f: X \to Y and g: Y \to Z are composable morphisms in a category. Their composite is denoted in point-free notation as g \circ f or f \cdot g, or in pointful notation as |x: X| g(f(x)) (to use a Rust-style programming syntax) or x: X \vdash g(f(x)): Z (to use a type-theoretic syntax).
In a bare category, the most general data that can be composed is a path of morphisms, and there is little practical difference between point-free and pointful notations. However, in richer categorical structures, the difference can be dramatic. As another illustration—still tiny by practical standards—suppose that f: X \times Y \to W, g: X \to W', and h: W \times W' \to Z are morphisms in a cartesian category. The composite morphism with signature X \times Y \to Z can be written in point-free notation as
(\Delta_X \times 1_Y) \cdot (1_X \times \sigma_{X, Y}) \cdot (f \times g) \cdot h,
which the reader must exert some effort to compile in their head, in contrast to the pointful notation
(x, y): X \times Y \vdash h(f(x, y), g(x)) : Z,
which is just the familiar syntax for composing functions. Besides its familiarity, a key ergonomic advantage of pointful notation is that operations like copying and permuting, which must be explicitly stated in point-free notation, become implicit.
A less obvious benefit of pointful notation is finding canonical forms for morphisms in free categorical structures. Consider again morphisms in a bare category. Using point-free syntax based on the standard biased axioms for a category, a ternary composite of morphisms f, g, and h admits two different expressions, h
\circ (g \circ f) and (h \circ g) \circ f, that denote the same morphism, by the associativity law. Yet, using pointful notation, it is possible to form only one term denoting this morphism, namely x : X \vdash h(g(f(x))): Z. The pointful notation thus gives a canonical form for morphisms in a free category. Of course, in this case, it is just as easy to produce a canonical form without using variables. That’s what the Path data structure in catlog does.
As categorical structure accumulates, finding canonical forms becomes more difficult. For example, let X \xrightarrow{f} Y \xrightarrow{g} Z and X' \xrightarrow{f'} Y' \xrightarrow{g'} Z' be morphisms in a monoidal category. In point-free syntax, two different expressions,
(g \circ f) \otimes (g' \circ f') \qquad\text{and}\qquad (g \otimes g') \circ (f \otimes f'),
denote the same morphism, by the interchange law. Moreover, due to the symmetry of the situation, there is no obvious reason to prefer one over the other. In the pointful notation of a suitable type theory, this symmetry is broken: of the corresponding two ways to denote this morphism,
(x, x'): X \otimes X' \vdash (g(f(x)), g'(f'(x'))): Z \otimes Z'
and
(x, x'): X \otimes X' \vdash \mathsf{let}\;{(y, y') = (f(x), f(x'))}\;\mathsf{in}\; (g(y), g(y')): Z \otimes Z',
the former is canonical as it contains no eliminable let bindings, whereas the latter does. This general point of view—that type theory is a toolkit to find canonical forms for morphisms—is a theme in Shulman’s lecture notes on categorical logic (Shulman 2016).
In short, among textual notations, pointful notation has both practical advantages, being familiar and ergonomic, as well as theoretical ones, inasmuch as it can help find canonical forms.
In CatColab, we plan to use pointful notation in several places. First, to specify equations between morphisms when finitely presenting a model. From the perspective that a model of a double theory is a theory in the sense of (one-dimensional) categorical logic, such equations are axioms of the theory. This feature is covered by the type theory presented in this RFC. In addition, we intend to use pointful notation in specifying the morphism part of a morphism between models, i.e., an interpretation of one theory in another, and also, moving up a dimension, in specifying the components of a transformation between model morphisms. The details of these features are beyond the scope of this RFC.
Before moving on, it’s worth acknowledging that point-free notation is not without its own merits. Conveniently for computer implementation, point-free notation can be mechanically extracted for categorical structures defined in any reasonable formal language, such as GATs or double theories. In contrast, finding the internal language of a new categorical structure—a type theory whose types and terms correspond precisely to the structure’s objects and morphisms—is often a research problem in its own right. The research problem behind this RFC is that while CatColab has a uniform meta-logic for (parts of) categorical logic at the level of semantics, we now seek a uniform account of the corresponding type-theoretic syntax.
In addition to being readily available for any categorical structure, point-free notation is equivariant under categorical duality. Pointful notation, on the other hand, is intrinsically biased toward the domain of a morphism (its inputs) and also, to a lesser extent, toward cartesian logics, in which variables can be freely duplicated and discarded. The further one departs from the ideal semantics of a cartesian multicategory, the more likely standard techniques are to break down. Nevertheless, we aim to push a uniform approach as far as we are able, as providing a familiar pointful notation seems indispensable to the vision of CatColab as a family of interoperable programming languages.
3 Technical approach
In many traditional type theories, especially those without function types,1 the sorts and operations available to use in contexts and terms are external data that parameterize the type theory. For example, the (mainly pedagogical) type theory for categories is parameterized by a graph (Shulman 2016, sec. 1.2), and the type theory for multicategories is parameterized by a multigraph (Shulman 2016, sec. 2.4.1). In more loaded terminology, such a graph or multigraph is called a signature; its vertices, sorts; and its (multi)edges, function symbols. A key feature of the present type theory will be to internalize the signature, i.e., to make it part of the type theory itself.
In fact, we will need to keep straight three different levels:
- Double theories
- Models of a double theory
- Morphisms in a model, denoted by terms in an internal language for the model.
The first of these levels will be external to the type theory. That is, the present type theory, like the original DoubleTT, is parameterized by a double theory. The second and third levels belong to the type theory itself. Depending on the double theory, models will be categorical structures like categories or multicategories; in fact, since they are finitely presented, such models are given by combinatorial structures like graphs or multigraphs, along with generating equations. So it is free models, internalized in this type theory, that play the role of signatures external to traditional type theories.
Models of a double theory are described by a dependent type theory combining standard and specialized rules. The judgmental structure is exactly that of standard dependent type theory. The type theory has record types (equivalent to dependent sums but more ergonomic) and singleton types (to enable model composition); it does not have dependent products, equality types, or universes. To this base is added specialized rules for the object and morphisms types of the double theory. All of this follows the original DoubleTT, with an important exception described below.
New here are two additional kinds of judgments:
- object terms over an object type in the theory, and
- morphism terms, or just terms, over a morphism type in the theory.
Morphism terms are the usual terms of an internal language. Object terms are less conventional, playing the role that contexts usually do.
In both simple and dependent type theory, contexts are lists of typed variables, with the list structure belonging to the meta-theory. We depart from this tradition since our internal languages encompass both unary type theories (Shulman 2016, 1) and multiary (“simple”) type theories (Shulman 2016, 2). Depending on which object type it is over, an object term may or may not be a list. To avoid confusion, we therefore avoid calling object terms “contexts.”2 Here the list structure is supplied by a modality available in modal double theories. So, again, a structure usually external to the type theory is internalized. The price paid is that operations like flattening nested lists, usually swept under the meta-theoretic rug, must now be explicitly handled within in the type theory.
Another design goal is that the type theory for morphisms be cut-free. That is, composition of morphisms should be not a primitive operation but an admissible rule: a meta-theoretic operation derivable from the other rules of the system. Eliminating primitive rules in favor of admissible ones is how type theory can produce canonical forms. Similarly, the type theory will allow constructing lists of morphism terms, but not lists of morphism generators. So, a major difference with the original DoubleTT is that point-free operations on morphisms like f \cdot g and [f, g] are not part of the type theory.
4 Mathematical specification
Turning to the mathematical spec, we present its three levels in the logical order: first, double theories; then models of a double theory, the subject of the outer type theory; and finally morphisms in a model, the subject of the inner type theory. That is the only sensible way to write the document. Still, the reader may find it easier to proceed in the opposite order, starting with the examples and working backward through the three levels of the spec.
4.1 Double theories
This RFC builds on the framework for double-categorical logic studied by the author and collaborators for some time now. However, needs from the type theory have led to us subtly reformulate the main definitions, so we present them again in a self-contained if terse style.
4.1.1 Almost representability
We refine the notion of double theory to interpolate between an arbitrary virtual double category (VDC) and a representable VDC (equivalent to a genuine double category).
Definition. A virtual double category is almost representable if for every multicell, every subpath of proarrows in its domain has a composite.
Equivalently, by the universal property of composites, a VDC is almost representable if every multicell factors through a composition cell and, moreover, every composition cell can be factored arbitrarily as a tight composite of binary and nullary composition cells. Thus, while such a VDC is not necessarily representable—there may be composable proarrows that do not have a composite—this failure is anodyne in that it cannot affect any multicell actually appearing in the VDC.
The analysis of an arbitrary multicell in an almost representable VDC reduces to three simpler cases: (1) unary cells, as in a genuine double category; (2) binary composition cells; and (3) nullary composition cells, i.e., extension cells for units. This case decomposition will appear directly in the rules of our type theory.
To avoid needless complications with coherence, we will also ask that our double theories be as strict as possible.3
Definition. An almost representable VDC is strict when it is equipped with a strictly associative and unital choice of composites, for all subpaths of proarrows in the domain of a multicell.
Whenever we write loose composites or identities in a double theory, we will mean the chosen ones.
Definition.
- The 2-category of almost representable VDCs, denoted \mathbf{arVDC}, has as objects, almost representable VDCs; as morphisms, functors (of VDCs) that preserve composites whenever they exist; and as 2-morphisms, natural transformations.
- The 2-category of strict almost representable VDCs, denoted \mathbf{arVDC}_{\mathrm{str}}, has as objects, strict almost representable VDCs; as morphisms, functors that strictly preserve the chosen composites; and as 2-morphisms, natural transformations.
Notice that \mathbf{arVDC} is a locally full sub-2-category of \mathbf{VDC}, the 2-category of VDCs, whereas \mathbf{arVDC}_{\mathrm{str}} merely has a locally fully faithful 2-functor to \mathbf{VDC}.
4.1.2 Simple theories
The most basic notion of double theory is:
Definition (cf. Lambert and Patterson 2024, sec. 3).
- A simple double theory is a strict almost representable virtual equipment, i.e., a strict almost representable VDC having all units and restrictions.
- A model of a simple double theory \mathbb{T} is a functor4 of VDCs M: \mathbb{T} \to \mathbb{S}\mathsf{et}; equivalently, a model of \mathbb{T} is a functor of virtual equipments M: \mathbb{T} \to \mathbb{C}\mathsf{at}, i.e., a normal functor of VDCs.
In practice, double theories are finitely presented. A type theory for models, including this one, should really be parameterized by a finite presentation of a theory rather than by the theory itself. However, we leave the problem of formalizing such presentations to future work.
4.1.3 Flatness
Recall that a (virtual) double category is flat, also called locally thin, if a cell is determined by its boundary, i.e., if for each possible cell boundary, there is at most one cell filling it (Grandis 2019, sec. 3.2.1).
Assumption. The double theory parameterizing this type theory is assumed to be flat.
This assumption might seem both strong and strange, but it’s not hard to motivate. Recall that the (tight) arrows of a double theory are viewed as operations acting on objects and the cells as operations acting on morphisms. In a pointful notation, then, arrows should act on types, which correspond to objects, and also on variables and terms, which represent elements of types. For example, a product operation in the double theory should act on types to form product types and on terms to form pairs. But in pointful notation, types and elements are all there is! As there is nothing else in the syntax for cells to act on, any cell being applied must be unambiguously determined by its boundary. That’s exactly what flatness says.
When a double theory is given by finite presentation, proving flatness can be nontrivial, amounting to a coherence theorem.
4.1.4 Modal theories
Besides simple double theories, the other double-categorical doctrine that we will need is modal double theories. In particular, the family of list modalities is essential to extract familiar-looking internal languages for “multiary” categorical structures like multicategories and monoidal categories. For the vast majority of the examples below, the following special case of the definition suffices. The reader may wish to take this as the definition on a first reading.
Definition (special case).
- A modal double theory is a monad (\mathbb{T},T) in \mathbf{arVDC}_{\mathrm{str}}, the 2-category of strict almost representable VDCs, whose underlying object \mathbb{T} is a virtual equipment.
- Let S be a monad on \mathbb{S}\mathsf{et} in the 2-category of VDCs. A model of a modal double theory (\mathbb{T},T) in (\mathbb{S}\mathsf{et},S) is a strict morphism of monads M: (\mathbb{T},T) \to (\mathbb{S}\mathsf{et},S) in the 2-category of VDCs.
Occasionally we need a double theory equipped with multiple modalities, possibly related to each other. Generalizing the idea of a double theory equipped with a single monad, a mode theory is used to axiomatize the available modalities, which could be monads, comonads, or other things besides.
Definition (general).
- A mode theory is a strict monoidal category \mathsf{M}.
- A modal double theory with mode theory \mathsf{M} is a 2-functor \cal{T}: \mathbf{B}(\mathsf{M}) \to \mathbf{arVDC}_{\mathrm{str}} from the delooping of \mathsf{M} to the 2-category of strict almost representable VDCs, such that the image \mathbb{T} \coloneqq \cal{T}(*) of the unique object is a virtual equipment.
- Let \cal{S}: \mathbf{B}(\mathsf{M}) \to \mathbf{VDC} be a 2-functor such that \cal{S}(*) = \mathbb{S}\mathsf{et}. A model of a modal double theory \cal{T} in \cal{S} is a 2-natural transformation:
This definition recovers the previous one by taking the mode theory to be the walking monoid. Thinking of the mode theory as a 2-category with one object, this choice corresponds to the walking monad.
4.1.5 List modalities
The list monad, or free monoid monad, is among the most famous examples of a monad. Upgrading the list monad on \mathsf{Set} to a double monad on \mathbb{S}\mathsf{et} creates new degrees of freedom in how a list of arrows relates to its lists of sources and targets.
One such degree of freedom is captured by the following data. Let \mathsf{F} be any wide subcategory of the skeleton of \mathsf{FinSet} that is a faithful cartesian club (Shulman 2016, Definition 2.6.3). Examples of interest are the subcategories consisting of identity functions, bijections, injections, surjections, or all functions.
There is a double monad \operatorname{List}_{\mathsf{F}}: \mathbb{S}\mathsf{et}\to \mathbb{S}\mathsf{et} that is the ordinary list monad in degree zero,
(\operatorname{List}_{\mathsf{F}})_0 \coloneqq \operatorname{List}: \mathsf{Set}\to \mathsf{Set},
and that sends a family of elements P: A \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}B to the family \operatorname{List}_{\mathsf{F}} P: \operatorname{List}A \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\operatorname{List}B whose elements
(\sigma, \underline{p}): (a_1, \dots, a_n) \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}(b_1, \dots, b_m)
consist of a function \sigma: [m] \to [n] together with a list \underline{p} = (p_1, \dots, p_m) of form
p_i: a_{\sigma(i)} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}b_i, \qquad i = 1,\dots,m.
This double monad is more precisely a monad in the 2-category \mathbf{VDC}, or, equivalently since \mathbb{S}\mathsf{et} is representable, in the 2-category of double categories, lax double functors, and (tight) natural transformations. For details and generalizations, see the math docs.
By convention, rules below that reference the double monad \operatorname{List} without further adornment are taken to mean \operatorname{List}_{\mathsf{F}} for any choice of \mathsf{F}.
4.2 Outer type theory: models
The outer type theory, a dependent type theory, has the standard judgments for contexts, types in context, and terms in context, as well as for equalities between types and between terms. We are agnostic as to whether substitutions are implicit or explicit. Moreover, the outer type theory has dependent record types and singleton types, though neither feature is actually needed for this RFC. For details, see RFC-0002 and references therein.
We state the special rules for DoubleTT in full, as there are changes from the original spec. In what follows, let \mathbb{T} be a double theory.
4.2.1 Object types
Object type former: For each object \cal{X} in the double theory, there is a type of objects of type \cal{X}:
Operation application:
4.2.2 Morphism types
Morphism type former: For each proarrow P: \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{Y} in the double theory, there is a type of generating morphisms of type P, depending on a pair of objects of types \cal{X} and \cal{Y}:
In particular, each object \cal{X} in \mathbb{T} has an identity proarrow \operatorname{id}_{\cal{X}}: \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{X}, which we denote \operatorname{Hom}_{\cal{X}} and call the Hom type on \cal{X}. Thus the following rule is derivable:
We emphasize that, in contrast to the original version of DoubleTT, a term of type P(X,Y) in the outer type theory represents a morphism generator from X to Y. That’s why morphism operations (unary cells in \mathbb{T}) cannot be applied to terms of type P(X,Y). An arbitrary morphism from X to Y is represented by a term u: X \vdash_P t: Y in the inner type theory.
4.2.3 Morphism equality types
Morphism equality type former: For each proarrow P in the double theory, there is a type of equalities between morphism terms over P:
Intuitively, a term of this type witnesses an equality between the morphisms denoted by t and s.
The type above is not an equality type in the usual sense of dependent type theory (Angiuli and Gratzer 2025). Indeed, the outer type theory does not have equality types, i.e., there is no type of equalities between a pair of outer terms of the same type. Rather, there is an type of equalities between a pair of inner terms (morphism terms) with the same domain and codomain.
4.2.4 List modality
Formation rules:
Computation rule, monad unit:
Computation rules, monad multiplication:
In the spirit of type theory, the rules above define the list monad, including the monad’s unit (singleton list) and multiplication (flattening), by induction, but this presentation is not very important. In fact, the rules for terms in the inner type theory will describe lists in an unbiased style. What is important is that the list operations compute: by iteratively applying the computation rules, any applications of \mu_{\cal{X}} and \eta_{\cal{X}} in terms can be eliminated.
4.3 Inner type theory: morphisms
We now assume that \mathbb{T} is a flat double theory.
4.3.1 Judgments
The inner type theory introduces two new judgments, both depending on contexts from the outer type theory.
Object terms: Presupposing that \cal{X} is an object type of \mathbb{T} and that \Gamma \vdash X: \operatorname{Ob}_{\cal{X}} is an object, the judgment
\Gamma \mid u: X
asserts that “u is an (object) term of type X, in context \Gamma and over \cal{X}”.
Morphism terms: Presupposing that P: \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{Y} is a morphism type of \mathbb{T}, that \Gamma \vdash X: \operatorname{Ob}_{\cal{X}} and \Gamma \vdash Y: \operatorname{Ob}_{\cal{Y}} are objects, and that \Gamma \mid u: X is an object term of type X, the judgment
\Gamma \mid u: X \vdash_P t: Y
asserts that “t is a (morphism) term of type Y with domain u: X, in context \Gamma and over P”.
When \cal{X} = \cal{Y} and P = \operatorname{Hom}_{\cal{X}}, the subscript P on the turnstile can be dropped.
In addition, there are judgments of equality between object terms and between morphism terms.
4.3.2 Object terms
Contexts are typically defined inductively to be lists of typed variables (i.e., variable-type pairs), but despite playing an analogous role, the object terms of this type theory are structured differently. First of all, object terms need not be lists at all. Only over an object type of form \operatorname{List}\cal{X} can we build object terms like
\Gamma \mid [x_1, x_2, x_3] : [X_1, X_2, X_3],
where the x_i are variables and the X_i are objects over \cal{X} in context \Gamma. Especially in examples, we might be lulled into writing this more conventionally as
\Gamma \mid x_1: X_1,\, x_2: X_2,\, x_3: X_3,
but we caution that the latter has no official meaning in this type theory; it is only syntactic sugar for the former.
4.3.2.1 Core rules
Formation rule:
where x is a variable assumed not to appear in the context \Gamma.
Operation application:
4.3.2.2 Lists
Formation rules:
where in the latter rule, the variables appearing anywhere in u and \underline{u} are assumed to be disjoint.
Computation rule, monad unit:
Computation rules, monad multiplication: like the above rule, mirrors the the computation rules for the list modality in the outer type theory.
4.3.3 Morphism terms
4.3.3.1 Core rules
Identity rule:
where x is a variable assumed not to appear in the context \Gamma. This rule can be interpreted as applying the nullary composition cell out of \cal{X}.
Post-composition rule:
where the first premise tacitly includes the assumption that the proarrows P and Q have a composite. This rule can then be interpreted as applying the binary composition cell out of P and Q. In our application syntax here and elsewhere, parentheses are optional; thus the expressions f(t) and f\,t are identical terms.
Operation application: for each unary cell \alpha in \mathbb{T} as on the left, there is a rule as on the right:
Notice that the cell’s name \alpha does not appear on the right-hand side, hence the need to assume that \mathbb{T} is flat.
Two special cases are worth recording. First, for each arrow F: \cal{X} \to \cal{Y} in \mathbb{T}, there is an identity cell \operatorname{id}_F = \operatorname{Hom}_F and hence a derived rule:
Second, each niche in \mathbb{T} as on the left can be filled with a restriction cell with domain P(F,G): \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{Y}. Hence, there is a derived rule:
Universal property of restriction: for each niche in \mathbb{T} as on the left, there is a rule as on the right:
Consequently, terms \Gamma \mid u: X \vdash_{P(F,G)} t: Y and \Gamma \mid F(u): F(X) \vdash_P G(t): G(Y) are in bijection.
4.3.3.2 Further composition rules
In type theory, composition of morphisms manifests primarily as the post-composition rule. This rule should always be present. However, one or both of the following extra rules related to composition may be needed depending on the categorical structure at hand. The pre-composition rule, enabling pre-composition with structural morphisms, is needed for non-planar multiary languages, like those of symmetric or cartesian multicategories. The let binding or “general composition” rule, enabling destructuring of outputs, is needed for co-multiary languages, like those of comulticategories or monoidal categories. Both rules are needed in languages like those of symmetric or cartesian monoidal categories.
Pre-composition rule:
where \gamma is a function from the set of variables contained in v to the set of variables contained in u. Here v[\gamma] denotes the morphism term given by substituting in the object term v along \gamma, which makes sense because object terms are included in morphism terms in that, whenever \Gamma \mid v: X, the identity term \Gamma \mid v: X \vdash_{\operatorname{Hom}_{\cal{X}}} v: X is derivable. As usual, s[\gamma] denotes the (morphism) term given by substituting in the (morphism) term s along \gamma.5
Let binding, or general composition rule:
where the first premise includes the assumption that P and Q have a composite. This rule can be interpreted as destructuring the value t and binding it to the variables in v.
Any type theory, including this one, should exhibit some notion of \alpha-equivalence. Here \alpha-conversion appears as the variable renaming rule:
Without the pre-composition rule, variable renaming is only an admissible rule, in that establishing it requires an induction over all possible derivations. With the pre-composition rule, variable renaming becomes a derivable rule, a special case of pre-composition given by taking X' = X and t = u to be an identity term, which forces \gamma to be a bijection.
4.3.3.3 Lists
Formation rule:
where it is implicitly assumed that the domain of the morphism term in the conclusion is well-formed, i.e., the variables appearing at any level among the object terms \Gamma \mid u_j : X_j are disjoint.
Computation rule, monad unit:
Computation rules, monad multiplication: extending the computation rules for lists of objects and lists of object terms, there are computation rules that govern the monad multiplication for lists of morphism terms. We omit the details.
5 Examples
5.1 Categories
Simplest among type theories are the unary ones—so simple, in fact, that they are rarely considered by type theorists outside of pedagogy. Yet from the categorical point of view, unary type theories are quite natural, being the internal languages of categories that do not have products, genuine or virtual (Shulman 2016, 1). For us, they are the internal languages of models of simple double theories.6
As a first example, taking the double theory to be the point, i.e., to be freely generated by one object, recovers the internal language a bare category (Shulman 2016, sec. 1.2).
5.2 Database schemas
For a unary type theory that’s a bit more interesting, consider the internal language of a database schema, axiomatized in idealized form by the walking proarrow, i.e., by the freely generated double theory
\mathbb{T} \coloneqq \big\{\mathsf{Entity}\overset{\mathrm{Attr}}{\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}} \mathsf{AttrType}\big\}.
Writing \mathrm{Mapping}\coloneqq \operatorname{Hom}_{\mathsf{Entity}} for the type of mappings (foreign keys) between entities, we can form the context representing a simple schema involving people and dogs:
\begin{aligned} \Gamma \coloneqq [ &\mathrm{String}: \operatorname{Ob}_{\mathsf{AttrType}}, \\ &\mathrm{Person}: \operatorname{Ob}_{\mathsf{Entity}}, \\ &\text{first-name}: \mathrm{Attr}(\mathrm{Person}, \mathrm{String}), \\ &\text{last-name}: \mathrm{Attr}(\mathrm{Person}, \mathrm{String}), \\ &\mathrm{Dog}: \operatorname{Ob}_{\mathsf{Entity}}, \\ &\text{owner}: \mathrm{Mapping}(\mathrm{Dog}, \mathrm{Person}) ]. \end{aligned}
We can then derive the terms with domain \Gamma \mid p: \mathrm{Person}:
- \Gamma \mid d: \mathrm{Dog}\vdash_{\mathrm{Mapping}} d: \mathrm{Dog}
- \Gamma \mid d: \mathrm{Dog}\vdash_{\mathrm{Mapping}} \text{owner}(d): \mathrm{Person}
- \Gamma \mid d: \mathrm{Dog}\vdash_{\mathrm{Attr}} \text{first-name}(\text{owner}(d)): \mathrm{String}
where step 1 uses the identity rule and steps 2 and 3 use the post-composition rule. The final term denotes the morphism that maps a dog to the first name of its owner.
5.3 Promonads
A promonad is a categorical structure with two kinds of morphisms, one of which (sometimes called tight) can be cast to the other (called loose). For example, a monad or a comonad on a category \mathsf{C} gives rise to a promonad whose tight morphisms are the morphisms of \mathsf{C} and loose morphisms are the Kleisli or co-Kleisli morphisms. As an example of the example, there is a promonad whose objects are measurable spaces, tight morphisms are measurable maps, and loose morphisms are Markov kernels.
Promonads are axiomatized by the simple double theory of promonads (see also the blog post Patterson 2024). The theory is generated by an object \cal{X}, a proarrow P: \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{X}, and a globular cell, the unit
such that the composite P \odot P = P exists and subject to a couple equations, the effect of which is to make the theory flat.
In the internal language of a promonad, we can build unary terms while tracking whether the morphism denoted is tight or loose. Taking the context
\Gamma \coloneqq [ X: \operatorname{Ob}_{\cal{X}},\ Y: \operatorname{Ob}_{\cal{X}},\ Z: \operatorname{Ob}_{\cal{X}},\ f: \operatorname{Hom}_{\cal{X}}(X,Y),\ g: P(Y,Z),\ h: \operatorname{Hom}_{\cal{X}}(Z,X) ],
we can derive the terms
- \Gamma \mid x: X \vdash_{\operatorname{Hom}_{\cal{X}}} x: X
- \Gamma \mid x: X \vdash_{\operatorname{Hom}_{\cal{X}}} f(x): Y
- \Gamma \mid x: X \vdash_P g(f(x)): Z
- \Gamma \mid x: X \vdash_P h(g(f(x))): X
by applying the identity rule and then repeatedly post-composing.
We can also invoke the operation application rule with the cell \theta to cast tight morphisms to loose. For example:
\Gamma \mid x: X \vdash_{\operatorname{Hom}_{\cal{X}}} f(x): Y \qquad\leadsto\qquad \Gamma \mid x: X \vdash_P f(x): Y.
Then post-composing with g, using the composite P \odot P = P, we derive the term \Gamma \mid x: X \vdash_P g(f(x)): Z again but by a different means. We see now why flatness of the double theory is important: the axioms of a promonad ensure that the two derivations yield morphisms that are equal in the intended categorical semantics. We will return to this point after examining the internal language of multicategories.
5.4 Multicategories
Perhaps the simplest multiary language is the internal language of a (planar) multicategory. In this highly substructural language, variables must be used exactly once and in the same order that they are declared. The type theory here should be compared with the cut-free type theory for multicategories in (Shulman 2016, sec. 2.4.1).
Let’s begin by reviewing the modal double theory of generalized multicategories, to be instantiated with the list modality T = \operatorname{List}= \operatorname{List}_{\operatorname{id}}. The generators of this double theory are an object \cal{X} and a proarrow P: \operatorname{List}(\cal{X}) \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\cal{X}. There are two key axioms, the composition and normalization axioms:
\operatorname{List}P \odot P = P(\mu_{\cal{X}}, 1_{\cal{X}}) \qquad\text{and}\qquad \operatorname{Hom}_{\cal{X}} = P(\eta_{\cal{X}}, 1_{\cal{X}}).
By the universal property of restriction, the composition axiom amounts to having a cell
giving the composition operation in the multicategory. Recall, however, that this binary cell cannot be directly applied in the internal language; instead, one uses the proarrow composite \operatorname{List}P \odot P, equal to the restricted proarrow P(\mu_{\cal{X}},1), then applies the restriction cell. The normalization axiom
says that the unary multimorphisms of P are in natural bijection with the morphisms of \cal{X}. For the remaining axioms of the double theory, see the page linked above.
To illustrate the type theory, we construct the associativity axiom of a monoid as a morphism equality type
\Gamma \vdash \mathsf{eq}([x,y,z]: [X,X,X],\ X,\ m[m[x,y],z],\ m[x,m[y,z]])\ \mathsf{ty}
in the context
\Gamma \coloneqq [X: \operatorname{Ob}_{\cal{X}},\ m: P([X, X], X),\ e: P([\,], X)]
that is the signature of the theory of monoids. We build the left-hand side as a term with domain \Gamma \mid [x,y,z]: [X,X,X]. The right-hand side is similar.
To start, use the identity rule to form the term \Gamma \mid x: X \vdash_{\operatorname{Hom}_{\cal{X}}} x: X and similarly for a second variable y. Combining these, form the list
\Gamma \mid [x,y]: [X,X] \vdash_{\operatorname{List}\operatorname{Hom}_{\cal{X}}} [x,y]: [X,X].
Apply the post-composition rule at the composable proarrrows \operatorname{List}\operatorname{Hom}_{\cal{X}} = \operatorname{Hom}_{\operatorname{List}\cal{X}} and P to build the term
\Gamma \mid [x,y]: [X,X] \vdash_P m[x,y]: X.
Next, apply the restriction rule at the theory’s normalization axiom to obtain a variable
\Gamma \mid [z]: [X] \vdash_P z: X
but viewed now as a unary multimorphism of P rather than as a morphism of \cal{X}. We can thus form the list
\Gamma \mid [[x,y],[z]]: [[X,X],[X]] \vdash_{\operatorname{List}P} [m[x,y],z]: [X,X],
apply the post-composition rule at the composable proarrows P and P
\Gamma \mid [[x,y],[z]]: [[X,X],[X]] \vdash_{P(\mu_{\cal{X}}, 1)} m[m[x,y],z]: X,
and finally apply the restriction rule again to derive the term
\Gamma \mid [x,y,z]: [X,X,X] \vdash_P m[m[x,y],z]: X.
As promised, this term is the left-hand side of the associativity axiom. It would be written more conventionally as
\Gamma \mid [x: X, y: X, z: X] \vdash m[m[x,y],z]: X
but we caution again that in our type theory, this expression can only be understood as an abbreviation for the previous one.
There was another, slightly longer way we could have derived the term m[x,y], parallel to how we derived the final term m[m[x,y],z]. Namely, after introducing the variables x and y, apply the restriction rule to obtain terms \Gamma \mid [v]: [X] \vdash_P v: X for variables v = x,y, then form the list \Gamma \mid [[x],[y]]: [[X],[X]] \vdash_{\operatorname{List}P} [x,y]: [X,X] and proceed as before to build the term \Gamma \mid [x,y]: [X,X] \vdash_P m[x,y] \vdash X.
By the theory’s compatibility axiom for the left action of P (contributing to the theory’s flatness), both derivations denote the same multimorphism in any model of the theory. Thus, the type theory is sound in allowing the two derivations to produce identical terms.
Turning this around, we see that terms in this type theory do not have unique derivations. While that’s not necessarily a problem, it can be a desideratum of a type theory that any (derivable) term has a unique derivation. For this particular double theory, we could achieve uniqueness of derivations by ad hocly prohibiting use of P’s left and right actions. The same trick would work for the theory of promonads. In general, though, we should not expect to have unique derivations.
5.5 Symmetric multicategories
Symmetric multicategories are also models of the modal double theory of generalized multicategories, now instantiated with the list modality T = \operatorname{List}_{\mathrm{bij}}. To illustrate, we derive the commutativity axiom of a commutative monoid as an equality type
\Gamma \vdash \mathsf{eq}([x,y]: [X,X],\ X,\ m[x,y],\ m[y,x])\ \mathsf{ty},
where \Gamma is the signature of the theory of monoids as before. We’ve already derived the left-hand side, so let’s derive the right-hand side.
Start with the variables \Gamma \mid x: X \vdash x: X and \Gamma \mid y: X \vdash y: X and apply the list formation rule using the swap permutation \sigma: [2] \xrightarrow{\cong} [2] to obtain the term
\Gamma \mid [x,y]: [X,X] \vdash_{\operatorname{List}_{\mathrm{bij}} \operatorname{Hom}_{\cal{X}}} [y,x]: [X,X].
Then post-compose with the generator m to obtain
\Gamma \mid [x,y]: [X,X] \vdash_P m[y,x]: X.
5.6 Cartesian multicategories
For non-planar multicategories, the list formation and post-composition rules used above do not suffice to build all of the expected terms; the pre-composition rule is also needed. To illustrate, using the internal language of a cartesian multicategory, we construct the distributivity axiom of a module over a rig
\Gamma \vdash \mathsf{eq}([r,x,y]: [R,X,X],\ X,\ r \cdot (x + y),\ (r \cdot x) + (r \cdot y) )\ \mathsf{ty}
in the context
\Gamma \coloneqq [ R: \operatorname{Ob}_{\cal{X}},\ X: \operatorname{Ob}_{\cal{X}},\ (+): P([X,X], X),\ 0: P([\,], X),\ (\cdot): P([R,X], X) ]
that is a fragment of the signature of the theory of modules over rigs. As is customary, the expressions x + y and r \cdot x are merely abbreviations for (+)[x,y] and (\cdot)[r,x]. We are again working with the modal double theory of generalized multicategories, now instantiated with the list modality T = \operatorname{List}_{\mathrm{fun}}.
The left-hand side of the distributivity axiom
\Gamma \mid [r,x,y]: [R,X,X] \vdash_P r \cdot (x + y): X
is constructed using only the language of planar multicategory. For the right-hand side, we proceed as before to build the intermediate term
\Gamma \mid [r,x,s,y]: [R,X,R,X] \vdash_P (r \cdot x) + (s \cdot y): X.
We must now apply the pre-composition rule to restrict the domain. To do so, first form the list
\Gamma \mid [r,x,y]: [R,X,X] \vdash_{\operatorname{List}_{\mathrm{fun}} \operatorname{Hom}_{\cal{X}}} [r,x,r,y]: [R,X,R,X]
using the function \sigma = [1,2,1,3]: [4] \to [3]. Then pre-compose with this term, with respect to the variable mapping \gamma: \{r,s,x,y\} \to \{r,x,y\} sending both r and s to r and preserving x and y, to derive
\Gamma \mid [r,x,y]: [R,X,X] \vdash_P (r \cdot x) + (r \cdot y): X.
Alternatively, we can use record types to compositionally construct the signature of the theory of modules. Defining the record types
\begin{aligned} \mathtt{SigRig} &\coloneqq \{ X: \operatorname{Ob}_{\cal{X}},\ \mathtt{add}: P([X,X], X),\ \mathtt{zero}: P([], X),\ \mathtt{mul}: P([X,X], X)\ \mathtt{one}: P([], X) \} \\ \mathtt{SigMod} &\coloneqq \{ R: \mathtt{SigRig},\ X: \operatorname{Ob}_{\cal{X}}, \mathtt{add}: P([X,X], X),\ \mathtt{zero}: P([], X),\ \mathtt{mul}: P([R.X, X], X) \} \end{aligned}
for the signatures of rigs and of modules over rigs, the distributivity axiom for scalar multiplication becomes
\begin{aligned} [M: \mathtt{SigMod}] \vdash \mathsf{eq}( & [r,x,y]: [M.R.X, M.X, M.X], \\ & M.\mathtt{mul}[r, M.\mathtt{add}[x, y]], \\ & M.\mathtt{add}[M.\mathtt{mul}[r, x], M.\mathtt{mul}[r, y]] ). \end{aligned}
Similarly, the associativity axiom for scalar multiplication is
\begin{aligned} [M: \mathtt{SigMod}] \vdash \mathsf{eq}( & [r,s,x]: [M.R.X, M.R.X, M.X], \\ & M.\mathtt{mul}[M.R.\mathtt{mul}[r, s], x], \\ & M.\mathtt{mul}[r, M.\mathtt{mul}[s, x]] ). \end{aligned}
5.7 Comulticategories
Our first example of a categorical structure with “co-multiary” morphisms is a comulticategory. This choice is rather silly as a comulticategory, having single-input, multiple-output morphisms, is maximally ill-adapted to pointful notation; moreover, since comulticategories are dual to multicategories, any morphism expressed in the internal language of a mulicategory could just as well be interpreted as a morphism in a comulticategory. Nevertheless, the example is worth considering, first, because our type theory does furnish an internal language for comulticategories, and, more importantly, because this language illustrates features like let binding also needed in more useful languages, such as those of PROPs or monoidal categories.
We work with the modal double theory of generalized comulticategories. I’ve not written down this theory explicitly, but it is just the loose dual of the theory of generalized multicategories. The theory is again instantiated with the list modality T = \operatorname{List}= \operatorname{List}_{\operatorname{id}}.
Consider the associativity axiom of a comonoid
\Gamma \vdash \mathsf{eq}(x: X,\ [X,X,X],\ \mathsf{let}\;{[y, c] = \delta x}\;\mathsf{in}\; \mathsf{concat}[\delta y, [c]],\ \mathsf{let}\;{[a, y] = \delta x}\;\mathsf{in}\; \mathsf{concat}[[a], \delta y] )\ \mathsf{ty}
in the context
\Gamma \coloneqq [X: \operatorname{Ob}_{\cal{X}},\ \delta: P(X,[X,X]),\ \varepsilon: P(X,[\,])]
that is the signature of the theory of comonoids. Here we write \mathsf{concat} for the list monad multiplication \mu_{\cal{X}} to avoid confusing Greek letters in the signature and in the type theory itself.
To construct, say, the left-hand side of the axiom, post-compose a variable with \delta to form \Gamma \mid y: X \vdash_P \delta y: [X,X] and apply the normalization axiom of a generalized comulticategory (where the unit \eta_{\cal{X}} now appears on the right boundary of the restriction cell) to form \Gamma \mid c: X \vdash_P [c]: [X]. Combining these two terms, form the list
\Gamma \mid [y,c]: [X,X] \vdash_{\operatorname{List}P} [\delta y, [c]]: [[X,X],[X]].
Now apply the let binding rule to the term \Gamma \mid x: X \vdash_P \delta x: [X,X] and to the term above, at the composable proarrows P and \operatorname{List}P, in order to derive
\Gamma \mid x: X \vdash_{P(1,\mu_{\cal{X}})} \mathsf{let}\;{[y,c] = \delta x}\;\mathsf{in}\; [\delta y, [c]]: [[X,X],[X]].
Finally, apply the restriction rule to obtain the desired term
\Gamma \mid x: X \vdash_P \mathsf{let}\;{[y,c] = \delta x}\;\mathsf{in}\; \mathsf{concat}[\delta y, [c]]: [X,X,X].
5.8 PROPs
A minimal categorical structure admitting both multiary and co-multiary morphisms is a PRO. However, it seems that nothing very interesting can be said in a PRO that can’t already be said in a multicategory or comulticategory. We proceed directly to the internal language of a (multisorted) PROP.
PROPs are models of the modal double theory of generalized PROs, instantiated with the list modality T = \operatorname{List}_{\mathrm{bij}}. The generators of this double theory are an object \cal{X}, a proarrow M: \operatorname{List}_{\mathrm{bij}} \cal{X} \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}\operatorname{List}_{\mathrm{bij}} \cal{X}, and a cell
Key axioms include the composition and normalization axioms:
M \odot M = M \qquad\text{and}\qquad \operatorname{Hom}_{\cal{X}} = M(\eta_{\cal{X}}, \eta_{\cal{X}}).
For the remaining axioms and other details, see the linked page.
We record the most interesting axiom of a bimonoid, namely that comultiplication commutes with multiplication (equivalently, that multiplication commutes with comultiplication), as the morphism equality type
\begin{aligned} \Gamma \vdash \mathsf{eq}( & [x,y]: [X,X],\ [X,X], \\ & \delta\, m [x, y], \\ & \mathsf{let}\;{[a,b,c,d] = \mathsf{concat}[\delta[x], \delta[y]]}\;\mathsf{in}\; \mathsf{concat}[m[a,c], m[b,d]]) \end{aligned}
in the context
\Gamma \coloneqq [ X: \operatorname{Ob}_{\cal{X}},\ m: M([X,X],[X]),\ e: M([\,], [X]),\ \delta: M([X],[X,X]),\ \varepsilon: M([X],[\,]) ]
that is the signature of the theory of bimonoids.
The left-hand side of this equation is built in the now familiar way: first form the list [x,y] over \operatorname{List}_{\mathrm{bij}} \operatorname{Hom}_{\cal{X}}, then post-compose with m to obtain \Gamma \mid [x,y]: [X,X] \vdash_M m[x,y]: [X], and post-compose again with \delta to obtain
\Gamma \mid [x,y]: [X]^2 \vdash_M \delta\, m [x,y]: [X]^2,
where we introduce [X]^k as an abbreviation for the list [X,\dots,X] with X repeated k times.
The right-hand side is derived by applying the let binding rule to the terms
\Gamma \mid [x,y]: [X]^2 \vdash_M \mathsf{concat}[\delta[x], \delta[y]]: [X]^4 \quad\text{and}\quad \Gamma \mid [a,b,c,d]: [X]^4 \vdash_M \mathsf{concat}[m[a,c], m[b,d]]: [X]^2.
For the first of these, apply the restriction cell from the normalization axiom to the variable x to make the term \Gamma \mid [x]: [X] \vdash_{\operatorname{List}_{\mathrm{bij}} \operatorname{Hom}_{\cal{X}}} [x]: [X], then post-compose with \delta to obtain \Gamma \mid [x]: [X] \vdash_M \delta [x]: [X]^2. We do the same for the variable y, then form the list
\Gamma \mid [[x],[y]]: [[X],[X]] \vdash_{\operatorname{List}_{\mathrm{bij}} M} [\delta[x], \delta[y]]: [[X]^2, [X]^2].
Finally, apply the cell \otimes representing the tensor to obtain the first of the above terms.
As for the second term, proceed similarly to construct the term
\Gamma \mid [[a,c], [b,d]]: [[X]^2, [X]^2] \vdash_{\operatorname{List}_{\mathrm{bij}} M} [m[a,c],m[b,d]]: [[X], [X]],
apply the tensor operation, and finally pre-compose with the term \Gamma \mid [a,b,c,d] \vdash_{\operatorname{List}_{\mathrm{bij}} \operatorname{Hom}_{\cal{X}}} [a,c,b,d] induced by the permutation \sigma = [1,3,2,4]: [4] \xrightarrow{\cong} [4].
5.9 Monoidal categories
At last we come to a categorical structure whose internal language has a non-trivial type constructor. In a monoidal category, we can form the monoidal product X \otimes Y of objects X and Y, the linear analogue of a product type. In fact, as objects of categorical doctrines, symmetric monoidal categories (SMCs) and (multi-sorted) PROPs are interchangeable: any theory that can be expressed as an SMC can just as well be expressed as a PROP, and vice versa. The difference is between their morphisms, or interpretations of theories: a symmetric monoidal functor, even a strict one, is more general than a morphism of PROPs. Such morphisms are, however, beyond the scope of this RFC. So, rather than recapitulating everything above in the language of monoidal categories, we will focus on what changes about the syntax and how the associators and other structure isomorphisms work.
The internal language of monoidal categories having a non-trivial type constructor corresponds to the modal double theory of generalized monoidal categories having a non-structural tight morphism. This theory is better known as the theory of monad pseudoalgebras or T-pseudoalgebras, where for T we can take a list double monad. For bare monoidal categories, we take the plain list monad T = \operatorname{List}= \operatorname{List}_{\operatorname{id}}. The generators of the theory are an object \cal{X}, an arrow \otimes: \operatorname{List}\cal{X} \to \cal{X}, and associator and unitor cells
and their loose inverses. The cells obey three coherence axioms.
Starting with contexts, suppose \Gamma \coloneqq [X: \operatorname{Ob}_{\cal{X}}, Y: \operatorname{Ob}_{\cal{X}}] and form the object term \Gamma \mid [x,y]: [X,Y] over \operatorname{List} \cal{X} as before. Applying the arrow \otimes: \operatorname{List}\cal{X} \to \cal{X} yields a new object term over \cal{X} that appears literally as
\Gamma \mid \otimes [x,y]: \otimes [X,Y].
Following the common practice for unbiased monoidal products, we abbreviate a product \otimes [X_1, \dots, X_k], with k > 1, as X_1 \otimes \cdots \otimes X_k, and we write the empty product \otimes [\,] as I. We then introduce the tuple notation (x_1,\dots,x_k) for the product element \otimes [x_1,\dots,x_k] for any k \geq 0. The object term above then appears in more familiar style as
\Gamma \mid (x, y): X \otimes Y.
We emphasize though that the latter is only syntactic sugar for the former.
In the context
\Gamma \coloneqq [ A, B, W, X, Y: \operatorname{Ob}_{\cal{X}},\ f: \operatorname{Hom}_{\cal{X}}(A, X \otimes W),\ g: \operatorname{Hom}_{\cal{X}}(W \otimes B, Y) ],
let’s construct a term denoting the morphism7 that is, rather unpleasantly, written in point-free notation as
(f \otimes 1_B) \cdot \alpha_{X,W,B} \cdot (1_X \otimes g): A \otimes B \to X \otimes Y,
where \alpha_{X,W,B} is a component of the (biased) associator natural isomorphism.
First, form the terms
\Gamma \mid a: A \vdash_{\operatorname{Hom}_{\cal{X}}} fa: X \otimes W \qquad\text{and}\qquad \Gamma \mid b: B \vdash_{\operatorname{Hom}_{\cal{X}}} b: B,
then the list
\Gamma \mid [a,b]: [A,B] \vdash_{\operatorname{List}\operatorname{Hom}_{\cal{X}}} [fa, b]: [X \otimes W, B],
and then apply the cell \operatorname{Hom}_{\otimes} induced by the tensor \otimes: \operatorname{List}\cal{X} \to \cal{X} to obtain
\Gamma \mid (a,b): A \otimes B \vdash_{\operatorname{Hom}_{\cal{X}}} (fa, b): (X \otimes W) \otimes B.
Now, intuitively, we want to apply the let binding rule to compose this term with
\Gamma \mid (x,(w,b)): X \otimes (W \otimes B) \vdash_{\operatorname{Hom}_{\cal{X}}} (x,g(w,b)) \vdash X \otimes Y
constructed similarly. But the types (X \otimes W) \otimes B and X \otimes (W \otimes B) don’t quite match up.
To proceed, we must use the associators and unitors to reshape the tuples. Semantically, this amounts to applying the following chain of isomorphisms
(X \otimes W) \otimes B \xrightarrow{\cong} (X \otimes W) \otimes (\otimes [B]) \xrightarrow{\cong} (X \otimes W \otimes B) \xrightarrow{\cong} (\otimes [X]) \otimes (W \otimes B) \xrightarrow{\cong} X \otimes (W \otimes B).
Let’s put this plan into action. Applying the unitor cell to a variable b gives \Gamma \mid b: B \vdash (b,): \otimes [B]. Tensor that with the pair (x,w) to get the term
\Gamma \mid ((x,w),b): (X \otimes W) \otimes B \vdash ((x,w),(b,)): (X \otimes W) \otimes (\otimes [B])
denoting the first isomorphism. Next, form the list of lists
\Gamma \mid [[x,w],[b]]: [[X,W],[B]] \vdash_{\operatorname{List}\operatorname{List}\operatorname{Hom}_{\cal{X}}} [[x,w],[b]]: [[X,W],[B]]
and apply the associator cell to derive the term
\Gamma \mid ((x,w),(b,)): (X \otimes W) \otimes (\otimes [B]) \vdash (x,w,b): X \otimes W \otimes B
denoting the second iso. Combining the two terms using the pre-composition rule yields a new term
\Gamma \mid ((x,w),b): (X \otimes W) \otimes B \vdash (x,w,b): X \otimes W \otimes B
representing the composite of the first two isomorphisms. Repeating this procedure for the inverse associator and unitor cells and applying the pre-composition rule a final time yields a term
\Gamma \mid ((x,w),b): (X \otimes W) \otimes B \vdash_{\operatorname{Hom}_{\cal{X}}} (x,(w,b)): X \otimes (W \otimes B)
denoting the composite of all four structure isomorphisms. Intuitively, this term represents the function that destructures the nested tuple on the left side of the turnstile and then restructures it into the nested tuple on the right side.
To complete the derivation, pre-compose the original term (x,g(w,b)) with the preceding term to obtain
\Gamma \mid ((x,w),b): (X \otimes W) \otimes B \vdash_{\operatorname{Hom}_{\cal{X}}} (x,g(w,b)) \vdash X \otimes Y,
then apply the let binding rule to derive
\Gamma \mid (a,b): A \otimes B \vdash_{\operatorname{Hom}_{\cal{X}}} \mathsf{let}\;{((x,w),b) = (fa,b)}\;\mathsf{in}\; (x,g(w,b)): X \otimes Y.
While this derivation was rather long, it is the job of the type checker, not the programmer, to check that a given term has a valid derivation. The term itself is short and readable. In fact, it is nearly identical to the following idiomatic Rust code:
fn f(a: A) -> (X, W) { ... }
fn g(input: (W, B)) -> Y { ... }
|(a, b): (A, B)| -> (X, Y) {
let (x, w) = f(a);
(x, g((w, b)))
}5.10 Symmetric monoidal categories
By now should there should be no surprises about how symmetric monoidal categories (SMCs) arise in this framework: take the modal double theory of generalized monoidal categories, now with the symmetric variant T = \operatorname{List}_{\mathrm{bij}} of the list double monad.
Besides the associators and unitors, SMCs have a new kind of structure isomorphisms, the symmetries. Let’s see how these appear in the internal language. Taking \Gamma \coloneqq [X: \operatorname{Ob}_{\cal{X}},\ Y: \operatorname{Ob}_{\cal{X}}] to have two objects, we can form the list
\Gamma \mid [x,y]: [X,Y] \vdash_{\operatorname{List}_{\mathrm{bij}} \operatorname{Hom}_{\cal{X}}} [y,x]: [Y,X]
using the swap permutation \sigma: [2] \xrightarrow{\cong} [2], just as we did for symmetric multicategories. But now we can apply the cell \operatorname{Hom}_{\otimes} induced by the tensor \otimes: \operatorname{List}_{\mathrm{bij}} \cal{X} \to \cal{X} to construct a new term
\Gamma \mid (x,y): X \otimes Y \vdash_{\operatorname{Hom}_{\cal{X}}} (y,x): Y \otimes X.
This term denotes the symmetry isomorphism \sigma_{X,Y}: X \otimes Y \to Y \otimes X.
5.11 Cartesian categories
Cartesian categories, by which we mean cartesian monoidal categories, arise from the modal double theory of generalized monoidal categories, for the cartesian variant T = \operatorname{List}_{\mathrm{fun}} of the list double monad.
Diagonals and projections are constructed in the same manner as symmetries: one forms the appropriate lists and then applies the cell \operatorname{Hom}_{\cal{X}} induced by the product operation \otimes: \operatorname{List}_{\mathrm{fun}} \cal{X} \to \cal{X}, conventionally written \times. For example, to construct the diagonal in the context \Gamma \coloneqq [X: \operatorname{Ob}_{\cal{X}}], first form the list
\Gamma \mid [x]: [X] \vdash_{\operatorname{List}_{\mathrm{fun}} \operatorname{Hom}_{\cal{X}}} [x,x]: [X,X]
using the function \sigma: [2] \xrightarrow{!} [1], then apply the cell \operatorname{Hom}_{\cal{X}}, and finally pre-compose with the unitor to derive
\Gamma \mid x: X \vdash_{\operatorname{Hom}_{\cal{X}}} (x,x): X \times X.
The internal language for cartesian categories here differs from the standard presentation of product types (e.g., Shulman 2016, fig. 2.4) in that, while it has the standard introduction rule for product types (pairing), it does not have the standard elimination rules (projections). That is, given a term t: X \times Y, there are no terms \pi_1(t): X or \pi_2(t): Y constructed by post-composing t with projection operations. Instead, projecting out a component of an arbitrary term t is a special case of destructuring, so that, say, the first component of t is given by \mathsf{let}\;{(x, y) = t}\;\mathsf{in}\; x: X or, permitting the use of anonymous variable names, \mathsf{let}\;{(x, \_) = t}\;\mathsf{in}\; x: X.
On the other hand, the latter term is a notation supported by many programming languages. For example, the Rust syntax is:
let (x, _) = t;5.12 Markov categories
Our final example, the internal language for a version of a Markov category, is the most complex logic treated here. The modal double theory for Markov categories, requiring a mode theory more elaborate than that of a single monad, axiomatizes a Markov category8 effectively as
- a cartesian category (of deterministic maps), which maps into
- a semicartesian category (of stochastic maps), via
- a monoidal promonad.
The double theory therefore combines several features used previously in isolation.
Complexity of the double theory aside, the internal language itself is no more difficult to use than the preceding ones. To illustrate, we write down a simple term denoting the sampling distribution of an abstract “surface plus noise” regression model (Efron 2020). Such a model has a deterministic component, the regression function, and a stochastic component, the noise distribution. Introducing the suggestive notation \mathsf{Determ}\coloneqq \operatorname{Hom}_{\cal{X}} and \mathsf{Stoch}\coloneqq P, this setup is captured by the context
\begin{aligned} \Gamma \coloneqq [\ & \mathrm{Predictors}: \operatorname{Ob}_{\cal{X}}, \\ & \mathrm{Response}: \operatorname{Ob}_{\cal{X}}, \\ & \mathrm{Coefficients}: \operatorname{Ob}_{\cal{X}}, \\ & \mathrm{Dispersion}: \operatorname{Ob}_{\cal{X}}, \\ & f: \mathsf{Determ}(\mathrm{Predictors}\times \mathrm{Coefficients},\, \mathrm{Response}) \\ & \mathrm{noise}: \mathsf{Stoch}(\mathrm{Response}\otimes \mathrm{Dispersion}, \mathrm{Response})\ ]. \end{aligned}
The sampling distribution, as a function of both the predicators and the parameters, is then:
\begin{aligned} &\Gamma \mid (x, \beta, \phi): \mathrm{Predictors}\otimes \mathrm{Coefficients}\otimes \mathrm{Dispersion} \vdash_{\mathsf{Stoch}} \\ & \qquad \text{noise}(f(x, \beta), \phi): \mathrm{Response}. \end{aligned}
Deriving this term is left as an exercise for the reader.
6 Rationale and alternatives
6.1 Bespoke internal languages
An obvious alternative to this RFC is to apply the standard methodology: for each categorical structure of interest, find its internal language and then implement that specific type theory. In this approach, every logic in CatColab requiring an internal language would have its own custom type-theoretic frontend.
From the “semantics first” perspective of CatColab, this approach is not unreasonable. By carefully separating the textual syntax, the data structures for models and morphisms to which the syntax compiles, and the analyses that can be run on those data structures, we could hope to retain many of the benefits of a uniform meta-logic, at least outside of the frontend. Indeed, this has been our intended approach to graphical editors for graphs, Petri nets, and so forth, whose variety seems to defy systematization. Yet I would still rather see the ad hoc approach to internal languages as a fallback option—at best a pragmatic compromise to the vision of CatColab as an interoperable family of programming languages.
6.2 String diagrams
Type theory is one methodology to find canonical forms for morphisms, but it’s not the only one. Among applied category theorists, the usual recipe to find canonical forms for morphisms in monoidal categories is to use string diagrams (Selinger 2010) or their combinatorial counterparts, wiring diagrams (Patterson et al. 2020). Incidentally, string diagrams are a point-free syntax, demonstrating that pointfulness is not a necessary property of normalizing syntax.
String diagrams are not so much an alternative to type-theoretic textual notation as a complement to it. Graphical and textual syntaxes each have their pros and cons, and both should be available in CatColab. Making multiple kinds of syntax work together seamlessly poses engineering challenges, if not also mathematical ones. This document,however, is solely about textual syntax.
7 Prior art
7.1 Frameworks for substructural types theories
To my knowledge, the most relevant prior art is Licata-Shulman-Riley’s “fibrational framework for substructural and modal logics” (Licata et al. 2017). Not only do both frameworks aim to unify a range of cartesian and substructural type theories, they share high-level features in their technical approaches. The details diverge significantly, though.
Both frameworks are parameterized by two-dimensional categorical structures that determine the rules of a sequent calculus. For LSR, a cartesian 2-multicategory (i.e., a category-enriched cartesian multicategory) plays the role that a modal double theory does here. Moreover, a locally discrete fibration over a cartesian 2-multicategory plays the role that a model of a modal double theory does here. The latter analogy can be made tighter by recalling that a \mathbb{S}\mathsf{et}-valued lax double functor is equivalent to a discrete double fibration (Lambert 2021), and presumably a similar correspondence holds for \mathbb{S}\mathsf{et}-valued functors of VDCs.
A difference in philosophy between the two accounts is that LSR start from the standard context structure of cartesian logic (i.e., the internal language of a cartesian multicategory) and then pass to substructural logics by tracking the use of variables through annotations on the turnstile. In contrast, we start from the trivial context structure of unary type theory and move up the hierarchy of substructural logics using different versions of the list double monad on \mathbb{S}\mathsf{et}. The only annotation on the turnstile is the morphism type. An advantage of LSR is that it hews much closer to how contexts are typically treated in type theory. An advantage of this account is that the bookkeeping for variable use shows up only in the derivations of terms, rather the terms themselves. It also avoids privileging cartesian multicategories over other categorical structures, at least not more than pointful notation does intrinsically.
7.2 Mode theories
The concept of a mode theory has also appeared in work by Licata and Shulman (2015; Licata et al. 2017). Moreover, we use essentially the same definition of a mode theory as in the first reference (a 2-category). Yet the high-level comparison is easily confused as there is a level shift in how mode theories are invoked here and in LSR. What LSR call the mode theory (a cartesian 2-multicategory) corresponds to a double theory, as just explained. We use a mode theory to organize the various modalities available in modal double theories and their models, principally the list double monads but possibly also others not discussed here, such as the codiscrete modality. To see the difference, in our framework the mode theory and its intended semantics in \mathbb{S}\mathsf{et} could be fixed for all logics, and that’s exactly what we intend to do in implementation. In contrast, for LSR, one chooses a different mode theory for each logic of interest, like we choose a double theory.
7.3 Split contexts and two-level type theories
Our contexts \Gamma \mid u: X are a kind of split context \Gamma \mid \Delta, where the judgments in \Delta can depend on those in \Gamma but not the other way around. In a similar spirit, our type theory can be seen as a two-level type theory (2LTT), and we have borrowed the terms “outer type theory” and “inner type theory” from this area. With that said, the specific work on split contexts or 2LTT that we know of has very different goals, leading to very different mathematics. Work on 2LTT, for instance, has aimed to embed homotopy type theory in Martin-Löf type theory. We will not attempt to survey this literature here, but see the linked nLab pages and references therein.
8 Future possibilities
8.1 Meta-theoretic results
We have a presented a type theory and demonstrated by example that it can reconstruct the internal languages of a range of categorical structures. However, we have proved almost nothing about it.
First, the type theory assumes that the parameterizing double theory is flat. For the simpler double theories, like those of database schemas or promonads, flatness is often obvious, but it’s generally nontrivial to see that a double theory given by finite presentation is flat. For example, flatness of the theory of generalized monoidal categories amounts to a coherence theorem about the associator and unitor cells. These and other flatness results should be proved.
As for the type theory itself, at minimum, it should be proved that the type theory is sound for models of any fixed double theory. That is, every context \Gamma \mid u: X should denote a well-defined object in the model generated by \Gamma, and every term \Gamma \mid u: X \vdash_P t: Y should denote a well-defined morphism in that model. The type should also be complete in the sense that every morphism in the model generated by \Gamma is denoted by some term. Beyond this, it should be possible to establish the expected meta-theoretic properties of particular internal languages. For example, the internal languages of planar, symmetric, and cartesian multicategories (omitting the let binding rule) should make the cut rule admissible.
8.2 Validation against more theories
We are far from exhausting the categorical structures within reach of this formalism. Here a few examples going beyond those presented here but still fitting neatly in the framework.
Representable multicategories. Arguably the categorical structure most faithful to programming syntax is neither a multicategory nor a monoidal category but a representable multicategory.9 In most programming languages, functions have multiple inputs and a single output, and there are product types. That’s exactly what you get in a representable multicategory. It is straightforward to axiomatize representable (generalized) multicategories as a modal double theory extending that of generalized multicategories; see the math docs and references therein.
Adjoint logics. All of the double theories considered here have a single generating object, \cal{X}. This restriction is by no means fundamental. We can just as well consider categorical structures involving multiple categories related by functors or adjunctions. Indeed, monads and adjunctions are both axiomatized as 2-theories, hence also as simple double theories (Lambert and Patterson 2024, sec. 3). As a specific example, the categorical semantics of mixed linear/non-linear logic (LNL) is a cartesian closed category and a symmetric monoidal closed category, connected by a symmetric monoidal adjunction (Benton 1994). Apart from the monoidal closedness, this structure would be straightfoward to axiomatize as a modal double theory. It would then be interesting to unwind the type theory for LNL furnished by this double theory.
References
Footnotes
Type theories with function types and enough inductive types to generate standard data types such as the booleans and natural numbers commonly omit a parameterizing signature entirely, under the idea that all other types and operations should be built out of the provided ones. In this RFC, however, we are exclusively concerned with type theories that do not have function types, i.e., with the internal languages of categorical structures that are not closed.↩︎
Thanks to Mitchell Riley for pointing out that the “contexts” in the inner type theory are more like terms.↩︎
This is consistent with Lambert and Patterson (2024), who, while using genuine rather than virtual double categories for double theories, still assume them to be strict. Thanks to tslil clingman for noticing the complications that arise in the type theory when we do not assume strictness.↩︎
A functor (of VDCs) between virtual equipments automatically preserves restrictions, a not-so-obvious fact (Shulman and Cruttwell 2010, Theorem 7.24). On the other hand, such a functor need not preserve any composites, including units. Both of these properties are intended of a model of a double theory.↩︎
A more careful treatment, not on offer here, would define the substitution operations on both kinds of terms by induction on their constructors. Still, it should be intuitively clear what it means to simultaneously substitute one set of variables for another.↩︎
We regret that our usage of “simple” departs from the type theorist’s. All of the internal languages covered by this RFC are simple type theories.↩︎
As it happens, this morphism appears as a string diagram in (Fritz 2020, Lemma 11.12).↩︎
Be warned that this definition is not equivalent to, but is slightly more than general than, the standard definition of a Markov category (Fritz 2020, Definition 2.1). It makes the deterministic maps be structure rather than property.↩︎
That representable multicategories are equivalent to monoidal categories makes them indistinguishable to the category theorist, but such a semantic equivalence does not imply that their internal languages are equally ergonomic.↩︎