0002 DoubleTT
1 Summary
DoubleTT is a type theory for specifying models of double theories. It combines standard judgments and rules of dependent type theory, such as dependent records, with specialized rules for double-categorical models, such as type constructors for object and morphism types. A key design objective is to enable composing models by identifying their objects, an instance of the “variable sharing” paradigm of composition. To perform such compositions, DoubleTT uses the type-theoretic concepts of record types and singleton types, along with a normalization-by-evaluation algorithm.
2 Motivation
Composing open systems is at the heart of applied category theory. Of the known paradigms of composition, most fundamental is variable sharing, formalized by the category-theoretic concept of colimit. DoubleTT is the first design for composing systems to be implemented in CatColab. It enables models of a fixed double theory to be composed by identifying their objects, following the variable sharing paradigm.
When implemented on a computer, composition in the variable sharing paradigm ultimately reduces to computing colimits of finite sets. The design space for doing that is larger than one might think, as there are many ways to represent finite sets and compute colimits of them.
The most obvious strategy represents a finite set using the union-find data structure and computes coequalizers using the union operation. This technique has been widely used in Catlab.jl and AlgebraicJulia. It has the advantage of being easy to implement, as the union-find data structure is simple and readily available in most programming languages. It also admits a powerful and flexible extension through the e-graph data structure, implemented in tools like egg and egglog.
A union-find is a data structure for storing and manipulating equivalence classes. No element of an equivalence class is privileged; any representative of the class will do as well as any other. While rarely given a second thought in mathematics, this feature is a nuisance in implementation, as the only way to display an element is by giving it some name, yet an equivalence class offers no guidance on which name to choose. Most symmetric would be to display all the names, but that would also be confusing and verbose.
DoubleTT sidesteps this problem by not explicitly constructing equivalence classes at all. Instead, it uses nested record types along with singleton types to ensure that, by construction, every element has a canonical name (normal form). In a typical usage, the user wanting to instantiate two models, while sharing a variable between them, creates a new variable in the top-level record type and then, via singleton types, specializes both variables in the instantiated models to be equal to the new variable. This hierarchical construction of a colimit breaks the symmetry: the name of the top-level variable is the canonical name.
In CatColab, we envision users building complex models by recursively composing simpler models. Thus, we must manage not just colimits, but colimits of colimits and so on. In AlgebraicJulia, we wrote procedures to compute colimits of diagrams of arbitrary shape, but relied on the host programming language, Julia, to orchestrate sequences of composition operations. No such escape hatch is available in CatColab. The hierarchical approach to composition in DoubleTT means that such recursive composition has first-class status.
Finally, DoubleTT provides the first purely text-based interface to models in CatColab, complementing the structure editor based on interactive notebooks. To be more precise, DoubleTT encompasses both formats. It has both a text elaborator and notebook elaborator, converting notation (plain text or a notebook) into a common intermediate representation (syntax). A single evaluator then converts syntax type and terms into value types and terms, respectively. This design is in keeping with the “semantics first” philosophy of CatColab, making surface syntax secondary to categorical semantics.
3 Mathematical specification
We have said that DoubleTT is a type theory for models of double theories. To be more precise, DoubleTT is a family of type theories parameterized by double theories: for each double theory \mathbb{T}, there is a type theory \mathsf{DoubleTT}(\mathbb{T}) describing models of \mathbb{T}.
3.1 Background: Double theories for type theory
For the purpose of parameterizing DoubleTT, we reformulate double theories to be as syntactical as possible. That means preferring extra primitive structure over equipping a simpler base structure with algebraic operations or universal properties. The same spirit is taken in Shulman’s “Categorical logic from a categorical point of view” (M. Shulman 2016), where generalized multicategories are preferred over cartesian categories or monoidal categories as the categorical semantics of simple type theories.
Here we adopt not just virtual double categories (VDCs) but even Koudenburg’s augmented VDCs (Koudenburg 2020) as an alternative to unital VDCs. Units in a VDC are elegantly but indirectly defined by a universal property. In an augmented VDC, much of the complexity of units is sidestepped by adding co-nullary cells as primitive structure.
Definition 1 (Simple double theory) A simple double theory is an augmented virtual double category with all restrictions, i.e., having both unary and nullary restrictions.
Definition 2 (Model of simple double theory) Let \mathbb{S} be a virtual double category with restrictions. A model of a simple double theory \mathbb{T} in \mathbb{S} is a functor (of augmented virtual double categories) M: \mathbb{T} \to \mathbb{M}\mathsf{od}(\mathbb{S}) that preserves restrictions.
The definition of a model makes sense because:
For any VDC \mathbb{S}, the module construction \mathbb{M}\mathsf{od}(\mathbb{S}) is a unital VDC (M. A. Shulman and Cruttwell 2010, Proposition 5.5), hence admits the structure of an augmented VDC (Koudenburg 2020, Example 2.2).
For any VDC \mathbb{S} with restrictions, \mathbb{M}\mathsf{od}(\mathbb{S}) also has restrictions (M. A. Shulman and Cruttwell 2010, Proposition 7.4).
When the semantics is not specified, we assume it is \mathbb{S} = \mathbb{S}\mathsf{et}.
3.2 Judgments of DoubleTT
DoubleTT has the four standard sorts (meta types) of dependent type theory:
Context: the judgment \vdash \Gamma\ \mathsf{cx} asserts that \Gamma is a context.
Substitution: presupposing \vdash \Delta\ \mathsf{cx} and \vdash \Gamma\ \mathsf{cx}, the judgment \Delta \vdash \gamma: \Gamma asserts that \gamma is a substitution from context \Delta to \Gamma.
Type: presupposing \vdash \Gamma\ \mathsf{cx}, the judgment \Gamma \vdash A\ \mathsf{ty} asserts that A is a type in context \Gamma.
Term: presupposing \vdash \Gamma\ \mathsf{cx} and \Gamma \vdash A\ \mathsf{ty}, the judgment \Gamma \vdash a: A asserts that a is a term of type A in context \Gamma.
In addition, there are judgments of equality between substitutions, between types, and between terms. Thus, DoubleTT has the sorts and judgments of a standard dependent type theory (see, e.g., (Angiuli and Gratzer 2025)).
3.3 Generic rules of DoubleTT
One part of DoubleTT is just a fragment of standard Martin-Löf type theory. These generic rules are collected here.
3.3.1 Contexts
Empty context:
Context extension:
3.3.2 Unit type
Unit type former:
Unit introduction:
Uniqueness rule:
3.3.3 Record types
We use letters m, n, \dots for the field names of record, not to be confused with variables in contexts.
Record type former:
Record introduction:
Elimination rules, restriction and projection:
For names m \neq n, restrictions and projections can be passed down:
Computation rules for restriction and projection:
And, for names m \neq n:
Uniqueness rule:
3.4 Special rules of DoubleTT
The following rules are specific to DoubleTT.
3.4.1 Object types
Object type former: For each object in the double theory, there is an object type:
Functor application:
3.4.2 Hom types
Hom type former: For each object in the double theory, there is a family of Hom types, parameterized by pairs of object terms:
Functor application:
Identity:
Composition:
3.4.3 Morphism types
Morphism type former: For each proarrow in the double theory, there is a family of morphism types, parameterized by pairs of object terms:
Pre-composition:
Post-composition:
3.5 Modalities in DoubleTT
Of the following modalities on the double theory, the codiscrete modality is particularly important as it makes admissible a truncation modality on the type theory itself.
3.5.1 Codiscrete modality
The codiscrete modality is an idempotent monad (\mathbb{T}, \mathop{\mathrm{coDisc}}, \eta) on the double theory.
Computation rules for object types:
Computation rules for Hom types:
Note that the first judgment makes the other two judgments admissible.
Computation rules for morphism types:
TODO: Admissible rule for cell applications
3.5.2 List modality
The list modality is a monad (\mathbb{T}, \mathrm{List}, \mu, \eta) on the double theory. We use the standard description of lists as an inductive data type, except that we write [\,\,] for \mathtt{nil} and [x, \underline{x}] for \mathtt{cons}(x, \underline{x}).
Introduction rules for object types:
Introduction rules for Hom types:
Introduction rules for morphism types:
3.6 Truncation modality on DoubleTT
The codiscrete modality in DoubleTT induces an admissible modality on DoubleTT: a meta-level operation that truncates a type generically involving both object and morphism types to one involving only object types. This is useful for type checking because the object part of DoubleTT is a simple type theory, hence types and terms can be normalized using standard normalization-by-evaluation algorithms.
The idea behind this meta-level modality, denoted \bigcirc, is to apply the codiscrete functor to types, apply the unit of the codiscrete monad to terms, and then apply the computation rules for the codiscrete modality to normalize the result.
To be more precise, we define \bigcirc by structural induction on contexts, types, and terms, with the following definitions as base cases:
on object types and terms:
on Hom types and terms:
on morphism types and terms:
For example, on a context, we can compute
4 Examples
For numerous examples of DoubleTT in both the plain text and notebook formats, see the packages/catlog/examples/tt folder in the CatColab repository.
5 Rationale and alternatives
5.1 Two-level type theory
We have seen that DoubleTT uses the standard sorts and judgments of dependent type theory. Another approach would be to introduce a base sort for object types, denoted \vdash A\ \mathsf{ty}_0 or \vdash A\ \mathsf{ob}\,\mathsf{ty}, along with a coercion to the general sort for types:
This approach, a kind of two-level type theory, has the virtue of making explicit that object types in DoubleTT do not depend on contexts, i.e., object types are the types of a simple type theory. However, we find that we can achieve much the same benefit by working in a standard dependent type theory that admits a truncation modality.
DoubleTT was originally conceived by Owen as a two-level type theory. This vision was reflected in early documentation (removed in commit ccbaf75) that described DoubleTT as the internal language of a fibration, but did not survive contact with implementation.
6 Prior art
6.1 Dependent type theory
As noted above, about half of DoubleTT is “just” concepts judiciously selected from dependent type theory. DoubleTT also uses a fairly standard normalization-by-evaluation (NbE) algorithm. For an excellent modern presentation of dependent type theory, emphasizing mathematics over implementation, see the book (Angiuli and Gratzer 2025).
6.2 Module systems
Another major source of inspiration for DoubleTT are module systems, as found in Standard ML and other programming languages in the ML family. DoubleTT is effectively a module system implementing both signatures (here models of double theories) and “functors” (not described above, but here functors for real, being morphisms of models). The use of record types and singleton types to formalize module systems is also precedented. For a slightly dated but still useful survey of module systems, see the PhD thesis (Dreyer 2005, 1).
Interestingly, the contrast between methods of computing colimits mentioned in the Motivation has its counterpart in the history of type sharing in the Standard ML module system. The SML ’90 spec realizes type sharing through sharing type clauses that treat identified types completely symmetrically, like in an equivalence class. In SML ’97, this approach was largely replaced in favor of asymmetric type sharing based on where type clauses, similar to the approach taken in DoubleTT.