0005 Fibrational definition of model
1 Summary
We demonstrate an obstruction between the equivalence of co-presheaves and discrete op-fibrations in the presence of pseudo-type monad morphisms (a doctrine or modality). This obstruction is used to motivate altering the definition of model from “functor from theory into Set” to “category fibred over theory”, and consequently we differentiate between the previously coinciding notions of modelling. This is a strict generalisation in the presence of modalities but otherwise coincides precisely, and there is room to study and embed the theory of the former gadgets in this new setting.
2 Scope
2.1 This RFC
- Illustrate the need for a broader definition of model in the modal setting
- Propose a mathematical framework for models
2.2 Future Work
- Translate the definition into concrete actions for the code base
- Engage with tabulators in virtual double categories, and other flavours that are of importance
- Provide, as necessary, theorems and definitions to give a “watertight” account of models
- Meet existing theory and work on instances
3 Modal fibrations are more general
Recall that there is a classical equivalence between the categories of co-presheaves and discrete op-fibrations in the purely 1-categorical setting, and that this equivalence is implemented in one direction by “taking sets of fibres over objects”.
The goal of this section is to establish that this correspondence is no longer true in the face of “modalities”: a system of compatible monads with a particular choice of semantics on one or more categories. In particular, we’ll focus on working with the \mathop{\mathrm{Maybe}} modality familiar to Haskell programmers, which we take concretely on set to be the “free pointed set” monad.
To ease notation let us write \mathop{\mathrm{\textsf{Mnd}}} for the category whose objects are monads on categories and whose morphisms are pseudo-type monad morphisms.
With this notation, consider the following two 1-categories at issue:
- \textsf{MDOpFib}, the category described by the below pullback where the comma categories are the usual one-categorical sort
- \textsf{MCPsh}, defined to be the slice category \mathop{\mathrm{\textsf{Mnd}}}/(\mathop{\mathrm{\textsf{Set}}},\mathop{\mathrm{Maybe}})
Note: readers may wish to take the lax slice \mathop{\mathrm{\textsf{Mnd}}}/_{\ell}(\mathop{\mathrm{\textsf{Set}}},\mathop{\mathrm{Maybe}}) instead, or work with 2-categories instead of 1-categories of op-fibrations and monads, but we’re going to exhibit an obstruction on the level of objects so the precise nature of the morphisms not at issue.
Finally with the pieces in play we may turn our attention to the game. We will pick out a particularly boring object of \textsf{MDOpFib} and show that it is not in the image of the category of elements of any object of \textsf{MCPsh}.
Consider then the “free category with the action of a monad on a point” \Delta_+, alternatively known as the augmented simplicial category. More elaborately, we think of \Delta_+ as on object of \mathop{\mathrm{\textsf{Mnd}}} given by the data of [0]\in\ob\Delta_+ and the action of a “generic” monad M\colon\Delta_+\to\Delta_+ defined by M[n]=[n+1], with the unit and multiplication being given by the appropriate morphisms [0]\to [1]\leftarrow [2]. Our particularly boring object of \textsf{MDOpFib} is then the identity \Delta_+=\Delta_+.
To see the obstruction, suppose a generic object \left((\mathsf{C}, M')\in\operatorname{Ob}\mathop{\mathrm{\textsf{Mnd}}}, F\colon(\mathsf{C},M')\to (\mathop{\mathrm{\textsf{Set}}},\mathop{\mathrm{Maybe}})\right)\in\textsf{MCPsh}\quad . If this object is intended to correspond to \Delta_+=\Delta_+ through the category of elements construction, then we must have |F\bullet|=1 for the object \bullet\in\operatorname{Ob}\mathsf{C} which encodes the fibre over [0]. It therefore follows that |FM'\bullet|=|\mathop{\mathrm{Maybe}}F\bullet|=2 for the object M'\bullet\in\operatorname{Ob}\mathsf{C} which encodes the fibre over [1]. However, the cardinality of the fibre over [1]\in\operatorname{Ob}\Delta_+ in \Delta_+=\Delta_+ is 1, so that no possible \mathsf{C},M',F can give rise to the modal discrete op-fibration \Delta_+=\Delta_+.
Remark: there appears to be something far more general at play here about cardinalites and classifying objects, but as presented the obstruction is sufficient for our purposes and we will not pursue a more general account.
To conclude this section, we suggest without proof that this example will embed as an obstruction in any more sophisticated “category-like” objects which in particular admit appropriate forgetful functors back to \mathop{\mathrm{\textsf{Cat}}} and \mathop{\mathrm{\textsf{Mnd}}}, including in particular flavours of double categories and virtual double categories.
4 Proposal
4.1 Background
Let us recall a few fundamental definitions and results from (Leinster 2009) concerning virtual double categories.
Recall the elementary definitions of virtual double categories, monads on virtual double categories, and horizontal Kleisli virtual double categories (Leinster 2009), (Shulman and Cruttwell 2010). We take the perhaps confusing, almost circular definition that the category of virtual double categories “is” \mathbb{H}\textsf{Kl}(\mathop{\mathrm{Psh}}\mathbb G_2, T), where \mathbb G_2 is the 1-globe category, \mathop{\mathrm{Psh}}\mathbb G_2 is the category of graphs, and T is the free category monad on graphs.
In particular this means that a virtual double category \mathbb{C} is equivalently a span of graphs C^0\xleftarrow{C^\ell} C^1\xrightarrow{C^r} TC^0 where C^0 is the “object graph” and C^1 is the arrow graph. That is,
- the elements of C^0_0 are the objects of the virtual double category,
- the elements of C^0_1 are the pro-arrows of the virtual double category,
- the elements of C^1_0 are the vertical morphisms of the virtual double category, and
- the elements of C^1_1 are the cells of the virtual double category.
The reason for this machinery is that we can therefore follow (Leinster 2009) and determine abstractly the following definition.
4.1.1 Definition: discrete op-fibration of virtual double categories
Given the data of pair of virtual double categories \mathbb{C}, \mathbb{D}, and a virtual double functor F\colon\mathbb{D}\to\mathbb{C} as arranged below, we say that F has the structure of a discrete op-fibration when the square marked (1) is a pullback.
In elementary terms this means that a functor F\colon\mathbb{D}\to\mathbb{C} has the structure of a discrete op-fibration when:
given an object d\in\operatorname{Ob}\mathbb{D} and a vertical morphism f\colon Fd\to c there exists a unique vertical morphism \langle f,d\rangle of \mathbb{D} with domain d such that F\langle f,d\rangle=f, and
for all n\in\mathbb N, given pro-arrows of \mathbb{D} arranged as below left and a cell of \mathbb{C} as below right, there exists a unique cell \langle\rho,(q_i)\rangle of \mathbb{D} with top boundary the q_i such that F\langle\rho,(q_i)\rangle=\rho.
We leave it to the reader to observe that under the embedding of categories into virtual double categories \mathbb H\textsf{Kl}(\mathop{\mathrm{Psh}}\mathbb G_1,\operatorname{id})\rightarrowtail \mathbb H\textsf{Kl}(\mathop{\mathrm{Psh}}\mathbb G_2,T) adjunct to the restriction (-)_0\colon\mathop{\mathrm{Psh}}\mathbb G_2\to\mathop{\mathrm{Psh}}\mathbb G_1=\mathop{\mathrm{\textsf{Set}}}, this definition correctly specialises to the usual notion of discrete op-fibration.
4.1.2 Virtual double category of elements
Although in the next section we will give a slick description of the correspondence between discrete op-fibrations and co-presheaves, it will nevertheless prove useful to explicate the category of elements construction.
To that end, given a virtual double functor F\colon\mathbb{C}\to\mathbb{S}\mathsf{et} the virtual double cateogory of elements of F, written \mathop{\mathrm{\mathbb{E}l}}F, is the virtual double category comprising the following data:
- the objects of \mathop{\mathrm{\mathbb{E}l}}F are \operatorname{Ob}\mathop{\mathrm{\mathbb{E}l}}F\coloneqq \sum_{c\in\operatorname{Ob}\mathbb{C}} Fc
- the collection of vertical morphisms (c, x\in Fc)\to(c', x'\in Fc') is the set \left\{f\colon c\to c'\mid Ffx=x'\right\}
- the collection of pro-arrows (c,x\in Fc)\nrightarrow (x',c'\in Fx') is the set \left\{(p,q)\in \sum_{p\colon c\nrightarrow c'}Fp\mid (Fp)_{\ell}q=x\wedge (Fp)_rq=x'\right\} where Fc\xleftarrow{(Fp)_\ell}Fp\xrightarrow{(Fp)_r}Fc' is the span which is the image of p in \mathbb{S}\mathsf{et}
- the collection of cells with the boundary below left is given by the subset of those cells \sigma of \mathbb{C} depicted below right given by \{\sigma \mid F\sigma\langle q_i\rangle=s\}. Note that we assume that the boundary is valid, in the sense that the depicted pro-arrows and vertical arrows meet the conditions expressed above.
Composition and identities are inherited from a combination of the semantics of \mathbb{C} and \mathbb{S}\mathsf{et}.
4.1.3 Discrete op-fibrations correspond to co-preseheaves, even though we haven’t proven it
Let us recall the combination of Theorems 6.3.1 and Theorems 6.4.3 of (Leinster 2009), here specialised to virtual double categories: there is an equivalence of categories \textsf{DOpFib}(\mathbb{C})\simeq\textsf{VDblCat}(\mathbb{C},\mathbb{S}\mathsf{et}) for each virtual double category \mathbb{C}, where \textsf{DOpFib}(\mathbb{C}) is the category of discrete op-fibrations of virtual double categories over \mathbb{C}.
Note that this result, as literally stated, isn’t quite of the shape that we were talking about in the section about the obstruction. Unfortunately we were not able to find a reference which goes through the very painful computation of showing that this point-wise equivalence is the on-objects component of a 2-equivalence between the 2-categories \textsf{DOpFib} and \textsf{VDblCat}/\mathbb{S}\mathsf{et}.
4.2 Models of theories
Given a theory \mathbb{T}, a model (C,\mathbb{C}) of the theory \mathbb{T} is a virtual double functor C\colon \mathbb{C}\to \mathbb{T} with the structure of a discrete op-fibration.
4.2.1 Examples
Although in some sense there’s nothing special about giving fibrational examples of models in the absence of modalities or other interesting structure because they’re precisely virtual double functors into \mathbb{S}\mathsf{et}, it’s nevertheless an important warmup for the modal examples we’re interested in later.
4.2.1.1 Graphs
The theory of graphs, \mathbb{T}_{\textsf{graph}}, is the free virtual double category on the walking parallel pair of morphisms. There’s not an awful lot to this example, but we highlight because it’s the exact analogue of usual story in the world of 1-categories.
4.2.1.2 Categories
The theory of categories, \mathbb{T}_{\textsf{cat}}, is the free virtual double category on a monoid. Explicitly, \operatorname{Ob}\mathbb{T}_{\textsf{cat}}=\left\{\bullet\right\}, there are no non-trivial vertical morphisms, there is a single pro-arrow h\colon \bullet \nrightarrow \bullet, and there are two non-trivial cells given below, satisfying the classical unitality and associativity axioms.
A model for this theory therefore comprises at first a set of “objects” we’ll suggestively write as \operatorname{Ob}\mathsf{C} fibred over \bullet. To every pro-arrow fibred over h we have a specified a domain and codomain object, so at first we have a span we’ll suggestively write as \operatorname{Ob}\mathsf{C}\leftarrow\mathop{\mathrm{Mor}}\mathsf{C}\to \operatorname{Ob}\mathsf{C}. By the discrete op-fibration structure, we know that for every x\in\operatorname{Ob}\mathsf{C} there is a unique cell \text{unit}_x filling a triangle whose every object is x so that in particular there must be a chosen 1_x\in\mathop{\mathrm{Mor}}\mathsf{C}. Similarly for every pair of composable f,g\in\mathop{\mathrm{Mor}}\mathsf{C} we may appeal to the discrete op-fibration structure to extract a unique cell \text{comp}_{f,g} determining the composite f\circ g\in\mathop{\mathrm{Mor}}\mathsf{C}. Finally the laws in the base lift to laws concerning 1 and \circ, so that models are exactly categories.
4.3 Modal models of modal theories
For the definition of monad on a virtual double category we defer to (Shulman and Cruttwell 2010). With that in mind, given a theory \mathbb{T} equipped with a monad M, a modal model (C,\mathbb{C}, S) of a theory (\mathbb{T}, M) is the data of a monad S on a virtual double category \mathbb{C} and a virtual double functor C\colon \mathbb{C}\to \mathbb{T} which has the structure of a discrete op-fibration and is additionally a strict morphism of monads S\to T.
4.3.1 Examples, or the two flavours
4.3.2 Multi-categories
The theory of multicategories, \mathbb{T}_{\textsf{multicat}}, is the virtual double category whose only non-trivial data is generated by:
- an object \bullet, a pro-arrow h\colon L\bullet\nrightarrow \bullet where L is the “list modality”
- cells governing composition and unitality as below, where \mu, \eta are the multiplication and unit of L
- equations between \text{comp} and \text{unit} asserting associativity and unitality, necessarily these involve the action of L.
Now let us turn our attention to a modal model C\colon(\mathbb{C},S)\to (\mathbb{T}_{\textsf{multicat}}, L). First, there is a class of models arising as essentially \mathop{\mathrm{\mathbb{E}l}}F for some modal virtual double functor F\colon(\mathbb{T}_{\textsf{multicat}}, L)\to (\mathbb{S}\mathsf{et},\operatorname{List}). For these, the fibre over \bullet contains a set of “objects”, and moreover the fibre over L\bullet contains genuine lists of these “objects”, and so on. In a similar way to our example of \mathbb{T}_{\textsf{cat}} in the theory of categories above the fibre over h therefore contains “multi-morphisms”, and the rest of the elaboration follows through mutatis mutandis.
However, not all modal models are of this form. In particular of course there is the identity modal modal, where as in our obstruction the fibres over L^n\bullet are all of cardinality one. More broadly, one might imagine various modal models which respect the necessary condition $|C||C| but otherwise do not supply “many” lists. These are various flavours of multi-categories which are degenerate in a variety of ways. TODO!
4.3.3 Schemas with nullable attributes
The theory of “schemas with nullable attributes” is the virtual double category whose only non-trivial data is generated by:
- two objects E, A,
- two pro-arrows E\nrightarrow E, E\nrightarrow A, and
- two more pro-arrows E\nrightarrow M(E), E\nrightarrow M(A) where M is the “maybe modality”.
A modal model for this theory is therefore:
- a set of entities fibred over E,
- a set of attribute types fibred over A,
- a collection of pro-arrows relating entities to other entities, and assigning named attributes to entities, and
- “nullable” versions of these, that is relations and attributes whose codomain is “Maybe(x)” for x some entity or attribute type
Note that because our only non-trivial in the theory is at the level of objects and pro-arrows, models may be empty or trivial in a variety of ways without contradicting the discrete op-fibration structure—this is a good thing.
Finally, this example is precisely of the form that our obstruction reveals is not in the image of the (modal) virtual double of elements construction. That is, we are entitled to ascribe an attribute of type “Maybe(x)” for x some attribute type instead of “Some(x)” or “None”.
4.4 A note on opcartesian cells, or why this section is not called “Unital models of unital theories”
Recall the definition of opcartesian of (Shulman and Cruttwell 2010). Observe that the structure and conditions are philosophically of the form “cells mapping ‘out’ of a top boundary”, and therefore suggest a high compatibility with the notion of discrete op-fibration. Indeed we invite the reader to verify the following.
Lemma: Suppose that F\colon \mathbb{D}\to \mathbb{C} is a discrete op-fibration of virtual double categories, and that moreover some string c_0\ldots\nrightarrow c_n of pro-arrows of \mathbb{C} has an opcartesian cell. In this case, every choice of strings d_0\ldots\nrightarrow d_n in the fibres of these pro-arrows has a uniquely determined opcartesian cell in \mathbb{D} fibred over the opcartesian cell in \mathbb{C}.
In this way, “unital models of unital theories” are simply those ordinary models for theories which happen to supply opcartesian cells.