0009 Instances in tt
This RFC is essentially about #1246.
1 Summary
The vision for CatColab is to integrate theories, their models, and their instances into one general system; the purpose of this RFC is to open a plan on extending DoubleTT to include instances, especially to allow for gluing of instances via instantiation, as we already support for models of discrete double theories.
2 The intended semantics
Fixing a (perhaps modal) double theory \mathbb{D}, the category \mathbb{D}-\mathrm{Mod} of \mathbb{S}\mathsf{pan}-valued models of \mathbb{D} is the base of a fibration \mathrm{Inst}\to \mathbb{D}-\mathrm{Mod} whose fiber over a \mathbb{D}-model X is the category \mathrm{Inst}_X of instances of X. The discrete case of this fibration (actually a trifibration) is studied in (Carlson and Patterson 2026, Corollary 4.8), while the modal case is not yet mathematically established.
Now the fibration \mathrm{Inst} \to \mathbb{D}-\mathrm{Mod} admits a morphism to the codomain fibration of \mathbb{D}-\mathrm{Mod}, given by sending an X-instance H to its model of elements or Grothendieck construction \int H\to X.1 This is handled in 5.1 of (Carlson and Patterson 2026).
A morphism of fibrations into a codomain fibration is precisely a comprehension category, see nLab, one of the standard semantics of dependent type theory. In a comprehension category the base of the fibration is the category of contexts, while the fibers are the categories of types in a given context, and the morphism into the codomain fibration gives the context extension operation
\dfrac{\Gamma \vdash A\texttt{ type}}{\Gamma, x : A\texttt{ ctx}}
The vertical morphisms f:A\to B between types in context \Gamma are (for us, at least) terms of B with context extended by A; in particular the closed terms of B are just the morphisms 1\to B. For instance if X is the schema for graphs, a closed term of an instance is a vertex equipped with a self-loop; we see that non-closed terms are important, since we’re working in something at least as general as a presheaf category. It is also possible to hink about contexts as separating the base from the fiber types, so you have a two-level type theory. This is closer to how things are currently implemented, but this is just an implementation detail–the comprehension category structure ensures that it’s not type-theoreticallys necessary to distinguish between a variable of instance type x:A versus of elements type x:\int A.
3 Instances are not diagrams
While the comprehension category does give a way to interpret an instance as a diagram, via \int, the result will always be a discrete opfibration, whereas in catlog::dbl until now a diagram has been, at least in the mind of the developer, a presentation of an instance. In fact a diagram f:E\to B of models is not that great of a data structure for presenting an instance of B, because in a discrete opfibration the morphisms in E are entirely determined by those in B and the objects of E, so that morphism data in E is at best redundant. Instead, an instance H of the model X is most efficiently presented by giving the fibers H_x over objects of X together with, as necessary, relations between the actions of morphisms of X on these fibers. For instance, one might generate the path graph of length 2 as something like \langle e_1,e_2\mid e_1\cdot t = e_2\cdot s\rangle. I’ve been working on augmenting the type theory to allow for precisely such specifications, which are well-adapted to the comprehension category semantics and introducing explicit judgments for populating the fibers of an instance.
4 Some examples
Here’s an example of the current implementation in the text elaborator
set_theory ThSchema
model Graph := [...]
instance PP : Graph := [
E := [e1,e2]
src(e1) := src(e2)
tgt(e1) := tgt(e2)
]This is the parallel pair graph and you can see the analogy with the math above. We can import instances:
instance PathPath : Graph := [
P1 : PP
P2 : PP
tgt(P1.e2) := src(P2.e1)
]The choices of e1 vs e2 in the equation are arbitrary. These imports are accomplished via propositional equalities, not the declarative ones that the specialization type mechanism for models effectively supports, because an instance is a rich algebraic structure (especially once it’s modal) and I do not think it’s possible to have canonical names for every element in a glueing of instances as we do for objects of glued models. This does mean that identifications for instances are accomplishing less, in the type theory, and leaving more to computer algebra further down the pipe.
Here’s an example of what the modal language looks like. It’s not really much harder to implement than the discrete case since we already had lists of terms available.
set_theory ThMulticategory
model SigRig := [
R : Object,
Add : SigMonoid & [ .M := R ],
Mul : SigMonoid & [ .M := R ]
]
instance Z2TheRig : SigRig := [
Add.op([Mul.unit([]),Mul.unit([])]) := Add.unit([]),
Add.op([Mul.unit([]),Add.unit([])]) := Mul.unit([]),
Add.op([Add.unit([]),Mul.unit([])]) := Mul.unit([]),
Mul.op([Add.unit([]),Add.unit([])]) := Add.unit([]),
Mul.op([Mul.unit([]), Add.unit([])]) := Add.unit([]),
Mul.op([Add.unit([]), Mul.unit([])]) := Add.unit([])
]5 Implementation
Newly as of the last few days of June, this is implemented in DoubleTT by making a new kind of judgment: we now have base types and base terms as well as fiber types and fiber terms. This seems like the right way to do type theory in a comprehension category where we don’t want to collapse all the types into the base; the fiber type theory is quite lightweight at this point, though. ## Model generation
tt:modelgen builds a DblInstance from an instance declaration. This is a new trait matching the “generators and equations” idea from above, with implementations for the discrete and the modal cases thus far.
6 Questions and to-dos
- Next up and low risk is the notebook elaborator, so we can put these into the app.
References
Footnotes
Though we don’t do it explicitly in the paper, it’s easy to check that \int sends cartesian instance morphisms to pullback squares of model: in fact the whole fibration of instances is a subfibration of the codomain fibration of categories via the collage category affiliated to a model.↩︎