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{M}\mathsf{od}(\mathbb{D}) of \mathbb{S}\mathsf{pan}-valued models of \mathbb{D} is the base of an opfibration \mathsf{Inst}\to \mathbb{M}\mathsf{od}(\mathbb{D}) whose fiber over a \mathbb{D}-model X is the category \mathsf{Inst}_X of instances of X. The discrete case of this opfibration (actually a trifibration–we’re thinking of the left-Kan opfibration) is studied in (Carlson and Patterson 2026, Corollary 4.8), while the modal case is not yet mathematically established. But hopefully it exists!
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{ cx}}. We can build comprehension categories out of opfibrations, too, by thinking of them as fibrations over the opposite base.
It’s then loosely correct to say that our intended semantics is simply the comprehension category determined by the domain opfibration of \mathsf{Inst}. That is, a context is a pair (X,H) of a \mathbb{D}-model X and an X-instance H, a type in context (X,H) is an \mathsf{Inst}-map (X,H)\to (X',H'), thus, a model map f:X\to X' and an instance map f_! H \to H'. The comprehension is tautological here, and the action of an \mathsf{Inst}-morphism on types is by pushout.
It’s crucial to observe that this story is essentially a boxing-up of a two-level type theory. Specifically, since \mathsf{Inst} is already a Grothendieck construction, it comes with the cocartesian-vertical factorization system. The types carried by cocartesian maps look like (X,H) \to (X',f_!H), so are basically just models under X, while the types carried by vertical maps look like (X,H)\to (X,H'). We derive two comprehension categories based on \mathsf{Inst}^\mathrm{op}, that is, two opfibrations over \mathsf{Inst} given by (X,H)\mapsto X/\mathbb{M}\mathsf{od}(\mathbb{D}) and (X,H)\mapsto H/\mathsf{Inst}_X. These are the and type theories we’ve implemented.
To get the semantics more precisely aligned with the syntax, we should admit that not all maps are really display maps, that is, the two opfibrations of base and fiber types shouldn’t really be arbitrary model or instance maps, but only ones we can actually build with our available tools. For base types, the only syntactically reachable display maps are those constructed by adjoining an object or a morphism, identifying morphisms, coproduct injections (which makes the first case redundant), and gluing objects. For instance types, they are similarly the coproduct injections, especially coproducts with instances freely generated by an element in a particular fiber, and identifications in fibers.
How about terms? In any comprehension category given by a fibration \pi:\mathcal{E}\to \mathcal{B}, the terms of a type E in context B are by definition the sections of the canonical projection \int E\to B from the comprehension of E. Now, for us, \mathcal{B}=\mathsf{Inst}^\mathrm{op}, so again the canonical projection is either essentially a model map X\to X', or essentially a map H\to H' of instances of the same model X, and a term becomes a of this display map. In particular, if d\in \mathbb{D} and \bar d is the cyclic model at d, then a term of \bar{d} in context X is precisely an element of X of type d, while similarly if m:d\mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}d' in \mathbb{D} and \bar m is freely generated by a morphism of type m, then a term of \bar m in context X is precisely a morphism of X of type m. Even if X\to X' freely identifies two parallel morphisms, it will have a unique term if and only if those morphisms were already equal in X, so we get extensional equality types for parallel morphisms. So the comprehension category naturally recovers the kinds of terms of models we’re used to. Terms work right for instances, as well, in much the same way.
2.1 Prior art
This idea of stacking fibrations is quite familiar from Bart Jacobs notion of a logic over a type theory, though of course we have some funny variances.
3 Presentation of the type theory
3.1 Judgments and generic rules
3.1.1 Judgments for contexts, substitutions, types, and terms:
- Contexts: \Gamma\texttt{ cx} Semantically, \Gamma is a model X of the background theory \mathbb{D} together with an instance H. In code, context.Context. Actually, the
context.scopeis more precisely what we think of type-theoretically as the context, and theenvis a substitution into it. - Substitutions: f: \Gamma\to \Delta. Semantically, f is a morphism of \mathsf{Inst}. RFC 0002, more fastidiously, avoids notating this as if \Gamma \to \Delta existed in its own right, but I think the abuse of notation is defensible here as otherwise it can be hard to tell the difference between a substitution and a term. In code, these are currently democratic and only implemented for base types, via Def.
- Base types: \Gamma \vdash X\texttt{ btype}. Semantically, X is a model under the model part of \Gamma. In code, see BaseTyV_ and friends.
- Fiber types: \Gamma \vdash H\texttt{ ftype}. An instance under the instance part of \Gamma. In code, see FiberTyV_ and friends.
- Base terms and fiber terms, with semantics in retractions as above.
3.1.2 How to build contexts
We have \cdot\texttt{ cx}, which semantically is the initial model with its empty instance.
Base extensions:
See bind_neu.
Fiber extensions:
There is no implementation of fiber extension yet in the kernel. The closest thing is push_fiber in the evaluator. The lack of a fiber bind_neu reflects significant constraints on the use of fiber-typed variables in the present implementation: base record types are closures over an environment, but fiber record types store their field type values directly, which is a big simplification but means instances can only be defined at top level, not, for instance, in defs, for now. Claude’s summary of the situation: “The fiber zone has syntax and conversion but no evaluator — five functions (eval_fiber_ty/tm, quote_fiber_ty/tm, bind_fiber_neu), one struct extension, and one representation change (fiber records as closures) are missing.” To re-emphasize, we never actually evaluate fiber syntax in the current situation! But it wouldn’t be very hard to zhuzh this up to match the base situation.
Observe that contexts can be interleaved between base and fiber variables. That said, it’s easy to recursively define a normal form \Gamma \equiv (\Gamma_b,\Gamma_f) in which all the base variables come first, since as we shall see, or as the semantics implies, a base type never depends on fiber data.
3.1.3 Substitution calculus
The substitution calculus was not outlined in RFC 0002 but may be taken to coincide with that detailed in (Angiuli and Gratzer 2025, sec. 2.3), which also provides the variable rule via weakening. Now that we have two type families, we need substitutions to act on both base and fiber terms.
Variance: Note what a substitution like
means, for our semantics. Since our context category is \mathsf{Inst}^\mathrm{op}, the substitution \gamma corresponds to a model morphism \gamma:|\Gamma|\to |\Delta|, while A is a further model under |\Gamma|, and then the substitution happens by pushout, which is easy on presented models (and instances.)
It’s a good place to note that base judgments don’t see fiber weakenings: substitution along a fiber weakening gives a bijection up to judgmental equality on base types, terms, and substitutions into fiberless contexts. The proof is that no rule producing any base judgment has any fiber premise, so the derivations can be transferred identically in either direction. This is how we prove that contexts have the base-fiber split normal form, and that we’re conservative over RFC 0002.
3.1.4 How to build base types and terms
We have dependent record base types (including unit types, i.e. empty records) as in RFC 0002. There are also singleton types, whose rules aren’t formalized there, but which are the backing for our specialization machinery. We also still have object and hom base types, as in RFC 0002. For all these see BaseTyV_.
If \Gamma is a pure base context, we define its semantics |\Gamma| recursively by sending \cdot to the initial model 0, |\Gamma, x : \operatorname{Ob}_d| to |\Gamma|+ \bar d and similarly for hom types, and |\Gamma, x : \mathsf{Sing}(t)| as |\Gamma|, and |\Gamma, _ : \mathsf{Id}_m(f,g)|, where f and g are morphisms of type m, as the coequalizer of the parallel pair \bar m \rightrightarrows |\Gamma| picking out f and g.
Non-generating terms of object types are acted on by functors, as well as in special doctrines via list formers and tabulators of morphism terms. Furthermore, Sing types introduce definitional equalities between syntactically distinct terms of object types. See BaseTmV_.
From this one can prove by structural induction that the normal forms of \operatorname{Ob}_d in context \Gamma are precisely |\Gamma|(d), for a base context \Gamma. Terms of morphism types are constructed as generators, identities on object terms, by applying functors, or by composition, and are identified by generators of equality types, and we similarly get a sound semantics on mor-types. Equality types themselves have terms built only from generators and functor applications. Extending from the above, if we have a base context \Gamma and \Gamma \vdash X\texttt{ btype} where X is some record, then a term of X in context \Gamma is just a consistent term-in-context of each row of X, semantically, a splitting of |\Gamma|\to |\Gamma,x:X| as intended. In particular, note that nontrivial closed types have no terms, because there are no retractions of the canonical map from the empty model to any nonempty model.
3.1.5 Fiber types and terms
Here we don’t have the specialization machinery and so things are a bit lighter-weight. We return to letting \Gamma be a general context. There are two basic constructors for fiber types:
Beyond this, the only way to make a fiber type is using a dependent record of fiber types. (FiberTyV_)
The semantics of fiber types are defined recursively by, for an Over, extending the realization of the context with a new generator in the appropriate fiber and, for an Id, identifying two elements of the same fiber (plus further equations this implies.)
A term of an Over type is either a generator, a list, an action by a functor in the theory, or an action by a morphism in the model, and we get a soundness theorem. A term of an Id type is always neutral, and equality is extensional. A term of a more general fiber type is an instance morphism, semantically. (FiberTmV_)
4 Remarks and examples
4.1 := overloading
In a model body, := is used as sugar for singleton specialization. For instance in the example
model Graph1 := [
V : Entity,
E : Entity,
src : EntityArr & [ .dom := E, .cod := V ],
tgt : EntityArr & [ .dom := E, .cod := V ],
]we could rewrite the third line as
src : [
dom : @sing E,
cod : @sing V,
arr : (Hom Entity)[dom, cod]
]In an instance body, := introduces an anonymous (necessarily unique) term of an Id type between its left- and right-side terms.
In a def, := means the usual definition thing.
4.2 Kinds of equality
As in RFC 0002, equality of terms of object kind in base types is definitional, using the dtry-based canonical names. Equality of morphisms in base types is propositional, as is equality of Over terms in fiber types. Convertibility of fiber types is purely structural, unlike for base types: the Record case of convertible_fiber_ty will look more like that for convertible_ty once there’s a bind_neu in fibers.
4.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.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([])
]4.5 Implementation
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, since the syntactic ways of building the two kinds of types are distinct; the fiber type theory is quite lightweight at this point, though.
4.6 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.
5 Claude’s appendix: rules, prose, and implementation
Claude wrote all of the below. Kevin’s at least glanced at it but not necessarily checked everything carefully. Caveat lector.
This appendix states the rules of the system as premise–conclusion trees in the style of RFC 0002. Each rule or rule group carries an annotation mapping it to the prose section that motivates it, the code that implements it, and a status: kernel — implemented in the representation-independent core (stx/val/eval/toplevel); elaborator-only — exists only fused into the frontends (text_elab/notebook_elab/fiber_elab), with no kernel counterpart; missing — specified here but not yet implemented; metatheorem — a statement about the system awaiting proof, not code. Code links resolve against the branch preview and should be re-pointed at next.catcolab.org/dev/rust/ after merge. Purely generic rules whose statement is verbatim from the literature (category laws for substitutions, record rules) are cited rather than restated.
5.1 Structural rules
Empty context, which is terminal (in the category of substitutions; initial in \mathsf{Inst}), with the unique substitution into it:
Prose: §How to build contexts. Code: Context::new. Status: kernel.
Base extension, with its weakening and variable:
The general variable rule (x deep in the context) is derived by composing weakenings, as in (Angiuli and Gratzer 2025, sec. 2.3). Prose: §How to build contexts. Code: Evaluator::bind_neu (the frontends wrap it as
intro, adding \eta-expansion); variables are BaseTmS_::Var, resolved by Evaluator::eval_tm. Status: kernel.Fiber extension, with its weakening and variable:
Prose: §How to build contexts, §Fiber types and terms. Code: Context::push_fiber only — there is no fiber
bind_neu, and the value side (FiberTmV_) compares variables by absolute level, which is sound only for toplevel instance elaboration. Status: elaborator-only.Exchange / base-first normal form: every context is isomorphic to one of the form (\Gamma_b, \Gamma_f) with all base entries first. Follows from the descent lemma below. Presupposed by the two-stack Context representation. Status: metatheorem.
5.2 Substitution calculus
We adopt the substitution calculus of (Angiuli and Gratzer 2025, sec. 2.3) for the single-family skeleton — identity and composite substitutions with the category laws — and state here only what our two type families add or change.
Identity and composition (laws as cited):
Prose: §Judgments, §Substitution calculus. Code: substitutions are democratic — user-facing only as record-typed Defs applied at
TopAppin Evaluator::eval_tm; the kernel form of a substitution is an Env, and composition happens implicitly, by evaluation. Status: kernel (base fragment).Action on base types and terms:
with the functoriality equations (stated for types; terms are analogous):
Prose: §Substitution calculus (including the variance remark). Code: Evaluator::eval_ty / Evaluator::eval_tm — under NbE the action is evaluation of quoted syntax (Evaluator::quote_ty / Evaluator::quote_tm) in a new environment, and the functoriality equations hold silently. Status: kernel.
Action on fiber types and terms:
with functoriality equations as above. Prose: §Substitution calculus. Code: would be
eval_fiber_ty/eval_fiber_tm; fiber syntax is currently never evaluated. Status: missing.Extension by a base term, with \beta and \eta laws:
Prose: (Angiuli and Gratzer 2025, sec. 2.3). Code:
Env::snoc— seeTopAppand Evaluator::field_ty. Status: kernel.Extension by a fiber term (\beta/\eta analogous):
Prose: §Substitution calculus. Code: — . Status: missing.
Let \Gamma \vdash H\ \texttt{ftype} and let \pi_H : \Gamma, h : H \to \Gamma be the weakening. Then the substitution actions
- \pi_H^* : \mathrm{Ty}_b(\Gamma) \to \mathrm{Ty}_b(\Gamma, h : H),
- \pi_H^* : \mathrm{Tm}_b(\Gamma, X) \to \mathrm{Tm}_b(\Gamma, h : H,\ X[\pi_H]) for every \Gamma \vdash X\ \texttt{btype},
- \pi_H^* : \mathrm{Sb}(\Gamma, \Delta) \to \mathrm{Sb}((\Gamma, h : H), \Delta) for every fiber-free \Delta,
are bijections modulo judgmental equality. Proof sketch: injectivity because weakening is a renaming; surjectivity by induction on derivations, using that no rule with a base conclusion has a fiber premise — witnessed in code by BaseTyS_ / BaseTmS_ having no fiber-mentioning constructor. Corollaries: the base-first normal form for contexts, and conservativity over RFC 0002. Status: metatheorem.
5.3 Base types and terms
Records — former, introduction, elimination, computation, and uniqueness rules are unchanged from RFC 0002 and not restated. Code: RecordV, BaseTmV_::Cons, Evaluator::proj, Evaluator::eta. Status: kernel.
Singleton types (surface syntax
@sing a) — former, introduction, and the \eta/elimination rule that makes them compute:
Prose: §How to build base types and terms, §Kinds of equality. Code: BaseTyV_::Sing; the \eta rule is the
Singcase of Evaluator::eta_neu. Status: kernel.Subtyping and subsumption — not present in RFC 0002; the design follows singleton kinds à la Stone–Harper. Singletons are the sole source of subtyping, propagated pointwise through records:
plus reflexivity, transitivity, and congruence for record fields (pointwise \leq over a common skeleton). Prose: §Kinds of equality. Code: Evaluator::subtype = Evaluator::convertible_ty (skeleton, Sing-erased)
- Evaluator::element_of (constraints). Status: kernel.
Specialization (single field shown; paths
.m.niterate). The premise is a subtype side condition at the field’s telescope:
The surface form
.m := tabbreviates.m : @sing t. Prose: §:=overloading. Code: Evaluator::try_specialize, RecordV::add_specialization. Status: kernel.Object types — former, and the term formers. Note \operatorname{Ob}_d has no introduction rule ex nihilo: closed nontrivial types are uninhabited, and object terms come only from the context and the formers below.
(the last two in doctrines with the list modality and tabulators, respectively). Prose: §How to build base types and terms. Code: BaseTyS_::Object; BaseTmV_::App,
List,Tab. Status: kernel.Hom types — former, identity, and composition (for m : d \mathrel{\mkern 3mu\vcenter{\hbox{$\shortmid$}}\mkern-10mu{\to}}d' a proarrow of \mathbb{D}; composition when the proarrow types compose):
Prose: §How to build base types and terms. Code: BaseTyV_::Morphism; BaseTmV_::Id,
Compose. Status: kernel.Morphism equality types — former and proof irrelevance:
There is deliberately no reflection rule in conversion: equality hypotheses are realized in |\Gamma| by coequalizer (see §How to build base types and terms) and consumed downstream by modelgen, not by the type checker. Prose: §Kinds of equality. Code: BaseTyV_::Id; irrelevance is the
Idcase of Evaluator::eta_neu. Status: kernel.Canonicity for \operatorname{Ob}_d: for a base context \Gamma, normal forms of type \operatorname{Ob}_d in \Gamma are in bijection with the elements of the presented model |\Gamma| at d. Prose: §How to build base types and terms. Code: operational witness is modelgen. Status: metatheorem.
5.4 Fiber types and terms
Over types — the free-element former:
Note the premise requires an object term (possibly modal, e.g. a list); the prose section states it for a general base type, but the implemented former is exactly this rule. Prose: §Fiber types and terms. Code: FiberTyS_::Over. Status: kernel data; usable only in toplevel instances.
Fiber records — former as for base records (dependency: later fields, typically equations, may mention earlier generators):
Prose: §Fiber types and terms. Code: FiberTyV_::Record — stored as evaluated fields with absolute-level dependency, not as a closure; this is the representation restriction blocking fiber
eval/quote. Status: kernel data (representation restriction).Fiber Id types — former and proof irrelevance; introduced by
:=in instance bodies, deliberately propositional (no canonical names in glued instances):
Prose: §Fiber types and terms, §
:=overloading. Code: FiberTyS_::Id. Status: kernel data; toplevel instances only.Fiber term formers — projection out of an import, lists, theory operations, and the action of a model morphism on fiber elements:
(projection is implemented only for generator fields of imports, whose types are closed; in modal doctrines the morphism action is multi-ary via lists). Prose: §Fiber types and terms. Code: FiberTmS_ / FiberTmV_, built in parallel by fiber_elab — fiber syntax is never evaluated. Status: elaborator-only.
Fiber conversion is structural (no binder-opening); see §Kinds of equality. Code: Evaluator::convertible_fiber_ty, Evaluator::equal_fiber_tm. Status: kernel.
Toplevel instance declaration
instance N : X := [...]packages a fiber record type with its codomain model. Prose: §Some examples. Code: Instance; realization to aDblInstanceby modelgen. Status: kernel (realization downstream of tt).