RFC-0009: Instances in DoubleTT

rfc/0009.md

@@ -0,0 +1,117 @@
+---
+title: |
+  `0009` Instances in tt
+author: Kevin Carlson
+date: 2026-05-08
+bibliography: _references.bib
+---
+
+{{< include _macros.qmd >}}
+
+::: {.callout-note}
+### RFC status
+
+This RFC is essentially about
+[#1246](https://github.com/ToposInstitute/CatColab/pull/1246).
+:::
+
+## 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. 
+
+## Instances are diagrams
+
+As in `catlog::dbl`, we here implement instances basically via diagrams, 
+that is, an instance $I:1\nrightarrow X$ of a model $X$ can be seen as 
+a model morphism $D: Y\to X$ such that the discrete opfibration over $X$
+freely generated by $D$ coincides with the Grothendieck construction $\int I.$
+See my and Evan's [paper](https://arxiv.org/abs/2510.08861) on instances for 
+details on this relationship. However, since a key desideratum is to be able
+to glue instances together using the specialization types of DoubleTT, we do 
+need the type theory to understand that a diagram is really generating a discrete
+opfibration, not to leave it inert.
+
+## Diagrams are pseudo-terms
+
+In the current design, DoubleTT interprets a diagram $I$ over $X$ as a special 
+kind of term of $X$; that is, we are adding to the type theory a new judgment 
+form $I :_D X$ saying that $I$ is a term of $X$ in the diagram sense. 
+These diagrammatic terms are easier to produce than the basic terms of 
+DoubleTT, where for instance there are no closed terms of types corresponding 
+to models. Specifically, for every object type `ot` in our theory, and 
+every declaration `Q : ot` in our model `X`, we provide a new type 
+`Over(Q)`, whose terms are intended to be all the things that might lie over `Q`
+in any `X`-instance, and then we can build diagrams over `X` using generators
+from these types, eg a diagram whose sole generator is `q : Over(Q)`
+corresponds to the $X$-instance freely generated by an element over `Q`. 
+
+## This changes contexts
+
+This means that contexts in the augmented DoubleTT now have variables of 
+two kinds; for instance you might have $x : X , I :_D X, y : Y$ as a context.
+You can see this change reflected in  `tt::context`, where basically `lookup`
+ignores diagram-type variables and `lookup_diagram` ignores ordinary variables.
+
+## Specialization uses the discrete opfibration property
+
+Suppose my model is, say, the schema for graphs `Gr`, and I want to glue together 
+two diagrams, say two copies of the walking edge `Edge : Instance(Gr) = [e : Over(E)]`
+(This is notional syntax, not quite what you type in .dbltt files),
+aiming to produce the walking path of length 2. Well, `Edge` has no names available
+for its vertices! We want to be able to declare something like 
+`Path2 : Instance(Gr) = [e1 : Edge, e2 : Edge] & .tgt(e1) = .src(e2)`. 
+So, we allow for almost exactly that, having the elaborator construct the implicit elements
+of a diagram implied by the discrete opfibration condition. Currently we treat the 
+problem of infinite instances without any neurons, just iterating out to a 
+fixed number of steps. More urgently, I suspect the algorithm as of May 8 is literally
+wrong when the model has equations in it, TBD.
+
+## Text front-end
+
+In `catlog/examples/tt/test_instances.dbltt`, you can see some cases of the intended 
+usage. The main example of substance is this: 
+```
+diagram I2 : @Instance(WeightedGraph) := [
+    v1 : @over .V,
+    v2 : @over .V,
+    w : @over .Weight,
+    we : Edge & [.src(e) := v1, .tgt(e) := v2, .weight(e) := w],
+    wf : Edge & [.src(e) := v2, .tgt(e) := v1, .weight(e) := w]
+]
+```
+
+Here `Edge` is the walking edge, as above, though now considered as a *weighted* graph. 
+Thus `I2` is the weighted graph generated by two edges in opposite directions and with 
+equal weights. The elaborator strips out the `@Instance` decoration once it adds 
+`I2` as a diagram-kind variable to the context, while elaborating `Edge` into a 
+genuine edge, whose vertices *canonically* have the sames `src(e)` and `tgt(e)`. So 
+the evaluation syntax in those names is made of cardboard; we haven't introduced a 
+new kind of term or anything to handle it at this point.
+
+## Model generation
+
+`tt:modelgen` builds a `DisreteDblModelDiagram` from a `diagram` declaration and 
+validates it using the machinery from `catlog::dbl`. 
+
+## Questions and to-dos
+
+- Is this special term kind a good idea? Is it normal? How do plain terms of 
+  models relate to instancey terms? Could the latter subsume the former? I had initially 
+  been imagining `Instance(X)` as a pseudo-universe type with its terms, the instances, 
+  themselves types, since if you think of them as models they feel typey, but that didn't
+  seem to work as well, not least because we don't really want universes in our type theory,
+  so we'd be faking a bit. 
+- How will this interact with Evan's RFC on internal languages, incorporating terms of 
+  models for specifying their morphisms? I kind of hope they're largely orthogonal but they're
+  both substantial modifications to the type theory, and it's not entirely clear to me that 
+  Evan's work is even non-breaking for DoubleTT. It's also notable that Evan doesn't really use 
+  terms and substitutions at the type level in his RFC. What's up with that vis a vis this? 
+- Next up and low risk is the notebook elaborator, so we can put these into the app. 
+- High priority but higher risk is to get thinking about modal instances. We don't understand these
+  real well mathemaically.
+- Mostly blue-sky but exciting to wonder about: what kind of migrations on instances are induced by substitutions
+  between model types?