Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: community: our work

Topic: Exponentiable virtual double categories and presheaves

Nathanael Arkor (Aug 18 2025 at 07:43):

I have a new preprint on arXiv: Exponentiable virtual double categories and presheaves for double categories. Here's the abstract:

Given a pair of pseudo double categories $\mathbb A$ and $\mathbb B$ , the lax functors from $\mathbb A$ to $\mathbb B$ , along with their transformations, modules, and multimodulations, assemble into a virtual double category $\mathbf{\mathbb Lax}(\mathbb A, \mathbb B)$. We exhibit a universal property of this construction by observing that it arises naturally from the consideration of exponentiability for virtual double categories. In particular, we show that every pseudo double category is exponentiable as a virtual double category, whereby the virtual double category $\mathbf{\mathbb Lax}(\mathbb A, \mathbb B)$ of lax functors arises as the virtual double category $\mathbf{\mathbb Mod}(\mathbb B^{\mathbb A})$ of monads and modules in the exponential $\mathbb B^{\mathbb A}$. We explore some consequences of this characterisation, demonstrating that it facilitates simple proofs of statements that heretofore required unwieldy computations. For instance, we deduce that the 2-category of pseudo double categories and lax functors is enriched in the 2-category of normal virtual double categories, and demonstrate that several aspects of the Yoneda theory of pseudo double categories – such as the correspondence between presheaves and discrete fibrations – are substantially simplified by this perspective.

The motivation for this paper is to understand the nature of the presheaf construction and the Yoneda lemma in double category theory. These were originally studied by Bob Paré in Yoneda theory for double categories. However, some surprises arise when one studies presheaves in this context: for instance, while presheaves on a category form a category, presheaves on a double category form not a double category but a [[virtual double category]]. This paper arose out of my trying to understand why this is.

In the paper, I explain that Paré's virtual double category of presheaves arises from two natural constructions on virtual double categories: taking exponentials, and the construction of monads and bimodules in a virtual double category (the so-called $\mathbf{\mathbb Mod}$ construction). This perspective is inspired by work of @Claudio Pisani on exponentiable multicategories. As a result, calculations involving presheaves on double categories are substantially simplified: for instance, I use it to give a new proof of the correspondence between presheaves on double categories and discrete fibrations of double categories. Along the way, I develop some (virtual) double category theory that I believe is of independent interest, so I'd encourage anyone interested in these topics to take a look, even if you're not specifically interested in the theory of presheaves.

As always, I'd be very happy to answer any questions anyone has!

John Onstead (Aug 18 2025 at 19:58):

I really enjoyed reading through this paper, since the matter of defining virtual double categories of lax functors between virtual double categories was something I have thought about a lot. I found it quite surprising that not every VDC was an exponentiable object in the 2-category of VDCs, since there is a usual category of lax functors between VDCs (giving us vertical arrows) and generally there's no restrictions on what the horizontal arrows can be (since they don't need to compose).
Maybe the issue is that there's "too much" freedom in how one could choose the horizontal arrows in a functor VDC (IE, the "existence" property is always satisfied, but not the "uniqueness" to make it a full exponential object). But I might be mistaken about this. Will certainly have more questions on this though, I just have to formulate them properly!

John Onstead (Aug 18 2025 at 20:02):

I mainly found it ironic that in an article centered on the "thing" the functors between double categories form- a virtual double category- the very same article brings up the possibility that there is no "thing" the functors between virtual double categories form (other than, obviously, plain 1-categories).

Mike Shulman (Aug 18 2025 at 21:08):

I thought a bit about exponentials of VDCs a while ago, and I think my conclusion was that it's mainly the absence of units that makes them fail to exist. That would be consistent with Nathanael's observation that pseudo double categories are exponentiable as a VDC. What about VDCs with units but not composites -- are they exponentiable?

James Deikun (Aug 18 2025 at 21:35):

No. The obstruction to exponentiability that comes up for functors of VDCs is essentially the same as the obstruction to the exponentiability of functors -- the fact that factorizations of cells don't always lift. The difference from ordinary functors is that even a terminal functor can have factorizations of cells that don't lift, because the terminal VDC is a lot less trivial than the terminal category.

An example of a normal VDC that isn't exponentiable--either as a normal VDC or a plain one--is the one generated by a single 3-ary 2-cell in general position. The two factorizations of the 3-ary 2-cell as two 2-ary 2-cells (and an identity) in the terminal VDC don't lift in the case of the generating cell, which means products with this VDC don't preserve pushouts. (This example is a slight modification of one due to Kevin Carlson, who in turn was inspired by one of Pisani's examples for multicategories.)

Nathanael Arkor (Aug 18 2025 at 21:39):

John Onstead said:

the possibility that there is no "thing" the functors between virtual double categories form (other than, obviously, plain 1-categories).

(There is also a notion of modification between transformation of functors between VDCs, although this doesn't extend the structure beyond a single "axis".)

My current perspective is that, for VDCs, one typically needs to take a more global perspective than one can get away with for categories or even double categories, because the lack of composition makes it impossible to stitch things together in the ways we have come to expect for structures with composition. For instance, VDCs do assemble into a coherent three-dimensional structure, but isn't possible to take "slices" of this three-dimensional structure in the same way that one can, for instance, take the hom-categories of a 2-category.

Nathanael Arkor (Aug 18 2025 at 21:44):

The exponentiable VDCs ought to be those that correspond to double categories in the same way that promonoidal categories correspond to monoidal categories. So, while they do not have composites, they are in some sense "not so far off" from having them. This corresponds to a certain factorisation property of cells in a VDC, as James mentions.

James Deikun (Aug 18 2025 at 21:47):

And VDCs should turn out to be exponentiable if you view them as certain virtual triple categories, which means you can get a hom virtual triple category of two virtual double categories. It seems that makes ordinary categories special here is that you can always knock the dimension down from 2 to 1 again when you take homs--this is what is not possible in general for virtual higher categories.

John Onstead (Aug 19 2025 at 09:51):

Nathanael Arkor said:

For instance, VDCs do assemble into a coherent three-dimensional structure, but isn't possible to take "slices" of this three-dimensional structure in the same way that one can, for instance, take the hom-categories of a 2-category.

James Deikun said:

And VDCs should turn out to be exponentiable if you view them as certain virtual triple categories, which means you can get a hom virtual triple category of two virtual double categories. It seems that makes ordinary categories special here is that you can always knock the dimension down from 2 to 1 again when you take homs--this is what is not possible in general for virtual higher categories.

That's interesting- I guess this is a case of how a structure is best understood in the context of the structure "one level up". Though it seems this pattern most likely continues- not every virtual triple category will be exponentiable unless viewed in the context of virtual quadruple categories, and so on, in a non-terminating sequence. So the only structure in this chain of virtual n-fold structures that can be closed under homs are ordinary categories.

Nathanael Arkor (Aug 19 2025 at 10:09):

James Deikun said:

And VDCs should turn out to be exponentiable if you view them as certain virtual triple categories, which means you can get a hom virtual triple category of two virtual double categories.

I'm not quite sure what you mean here: are you just restricting the VTC of VDCs to the two-object VTC where you only take the functors in one direction (e.g. from $\mathbb A$ to $\mathbb B$)?

John Onstead (Aug 19 2025 at 10:17):

Nathanael Arkor said:

I'm not quite sure what you mean here: are you just restricting the VTC of VDCs to the two-object VTC where you only take the functors in one direction (e.g. from $\mathbb A$ to $\mathbb B$)?

I don't know if this helps but here's how I interpreted this. Just as double categories are the "representable" VDCs and so are exponentiable with respect to VDCs, VDCs are "representable" VTCs and hence we might expect them to be exponentiable with respect to VTCs. (Nevermind, triple categories are the representable VTCs, oops. But I think there's a similar connection between VTCs and VDCs as between VDCs and ordinary categories that might be useful)

James Deikun (Aug 19 2025 at 10:35):

Nathanael Arkor said:

I'm not quite sure what you mean here: are you just restricting the VTC of VDCs to the two-object VTC where you only take the functors in one direction (e.g. from $\mathbb A$ to $\mathbb B$)?

This uses the reflective embedding of VDCs as "tightly discrete" VTCs. The reflection takes objects to generating objects, loose arrows to generating tight arrows, slack arrows to generating loose arrows, loose 2-cells to generating 2-cells, and the rest to relations. The embedding does the reverse, starting with the standard presentation. Identities and composition come from closure properties of the standard presentation.

The image of the reflective embedding lies among the VTCs that are representable as fVDC-categories, and hence exponentiable. Basically I think what happens here is that the image isn't closed under pushouts, and the pushouts of VDCs that aren't preserved by the VDC-level product functors are the ones that are moved by the reflection.

James Deikun (Aug 19 2025 at 11:04):

I think what the hom VTC looks like in practice is everything but the 3-cells are what you would expect if there actually were a hom VDC and you were embedding it as a tightly discrete VTC, but rather than the 3-cells witnessing unique composites, the 3-cells you get for a pasting diagram $\mathbb{P}$ correspond to natural isomorphism classes of coherent coverings of all 2-cells in $\mathbb{A}$ shaped like the out-cell of $\mathbb{P}$ by images of $\mathbb{P}$ in $\mathbb{A}$.

Nathanael Arkor (Aug 19 2025 at 11:17):

James Deikun said:

This uses the reflective embedding of VDCs as "tightly discrete" VTCs.

Ah, I see.

John Onstead (Aug 19 2025 at 17:05):

As promised, I did have a more formal question about the article. One of the main reasons for my interest in higher dimensional category theory is in how it relates to formal category theory. From what I've seen, there's two ways of doing formal category theory- equipments (like virtual equipments) that add a notion of "profunctor", and structures (like Yoneda structures) that add a notion of "presheaf object". The above work seems to be in the latter domain (ironically while working with the structures we use in the former). A previous work shows how these relate in simple cases. For instance, a Yoneda structure is given as a relative lax idempotent 2-monad, and the corresponding proarrow equipment that gives the same formal category theory uses the Kleisli construction for this relative monad.

John Onstead (Aug 19 2025 at 17:05):

The above paper covers how the $(-)'$ functor from normal VDCs to VDCs constitutes a lax idempotent adjunction with $\mathrm{Mod}$. It doesn't mention if this extends to $P: \mathrm{DblCat} \to \mathrm{VDblCat}$. But this does raise an interesting question for me. If $P$ were relative lax idempotent 2-monad, then we ought to be able to construct a proarrow equipment of double categories as mentioned above. However, there is no proarrow equipment for double categories (only a virtual equipment). Does this mean $P$ is not in fact a relative lax idempotent 2-monad, or am I getting confused somewhere?

Kevin Carlson (Aug 19 2025 at 18:12):

By the way, Ea Thompson announced a characterization of all exponentiable VDCs in a Topos seminar concluded their RAship here this summer a couple of weeks ago. I’ll ask whether they want to get on this server and share their slides as the video hasn’t yet appeared.

Nathanael Arkor (Aug 19 2025 at 18:39):

@John Onstead: I can give a high-level intuition, and give more details afterwards if you'd like. In an ideal scenario, either the exponential $\mathbf{\mathbb Span}^{\mathbb A^{\text{op\,t}}}$ or Paré's $\mathbf{\mathbb Lax}(\mathbb A^{\text{op\,t}}, \mathbf{\mathbb Span})$ would be:

1. A presheaf construction on $\mathbb A$ (in a formal sense, e.g. §7.1 here).
2. A free cocompletion of $\mathbb A$ (with respect to some notion of colimit).

There is evidently a subtlety in the above, in that the exponential and Paré's construction are only relative, in that they take a double category and produce a virtual double category. However, it is the case that the exponential forms a presheaf object in the virtual double category of virtual double categories, since it represents tight distributors between double categories. (This essentially says that the 2-category of virtual double categories has a Yoneda structure, in which double categories are admissible objects.)

However, it does not seem that there is any reasonable sense in which it can be a free cocompletion. (In a formal context, free cocompletions are always presheaf objects, but the converse is not always true.) Indeed, if it were, it would form a lax-idempotent relative pseudomonad, which would give a composition of tight distributors, which we know is not possible (from Mike's counterexample). But I think there is certainly more to be understood here.

Nathanael Arkor (Aug 19 2025 at 18:42):

@Kevin Carlson: oh, cool! I'm glad I decided to limit my consideration of exponentiability to this special case, then. I would be very interested to see the slides (or, even better, a recording if there is one).

Nathanael Arkor (Aug 19 2025 at 18:44):

I know Soichiro Fujii and Steve Lack have also been thinking about related topics (although I think they're focusing more on exponentiable morphisms of VDCs), so these ideas seem in the air at the moment.

John Onstead (Aug 19 2025 at 22:13):

Nathanael Arkor said:

I can give a high-level intuition, and give more details afterwards if you'd like.

Thanks for the explanations! Formal category theory is certainly one of my favorite parts of category theory in general so it's always fun to learn more about!

John Onstead (Aug 19 2025 at 22:15):

Nathanael Arkor said:

However, it does not seem that there is any reasonable sense in which it can be a free cocompletion. (In a formal context, free cocompletions are always presheaf objects, but the converse is not always true.) Indeed, if it were, it would form a lax-idempotent relative pseudomonad, which would give a composition of tight distributors, which we know is not possibl

Ah, that's exactly what I was suspecting above- that if it were a relative lax idempotent 2-monad there'd be an associated proarrow equipment, but it can't be since there isn't a non-virtual proarrow equipment for double categories. But now this makes more sense in the context of the divergence between "free cocompletion" (which I guess is always given by a relative lax idempotent monad by definition) and "presheaf object". It was confusing me earlier since these converge in "good" cases, but it's interesting to know it's not always the case!

John Onstead (Aug 19 2025 at 22:17):

I guess my next follow up would be this: might it be possible to reconstruct the virtual equipment structure on $\mathrm{DblCat}$ from the functor $\mathbf{\mathbb Span}^{\mathbb A^{\text{op\,t}}}$ in the same way one can reconstruct a proarrow equipment from any relative lax idempotent 2-monad? Put another way, does $\mathbf{\mathbb Span}^{\mathbb A^{\text{op\,t}}}$ satisfy any properties as a functor that generalize the notion of a relative lax idempotent monad to fill in the analogy: Relative Lax Idempotent Monad is to Proarrow Equipment as Mystery Functor Type is to Virtual Equipment? (Maybe we could call these "virtual free cocompletions" to keep the analogy in line?)
(Also, I guess you could just define these functors to be "functors into a virtual equipment such that the image of the functor are presheaf objects", but I was hoping for something less tautological that might even work on the bicategory level, like lax idempotence)

Ea E T (they/them) (Aug 20 2025 at 01:12):

Nathanael Arkor said:

Kevin Carlson: oh, cool! I'm glad I decided to limit my consideration of exponentiability to this special case, then. I would be very interested to see the slides (or, even better, a recording if there is one).

Hi, here are my slides that Kevin is referring to (in powerpoint and pdf formats if one doesn't work):
Pro-representableVDCs.pptx
Pro-representableVDCs.pdf
Also, after reading your paper today, I was able to prove that this characterization agrees with the notion of malleable VDCs, though I haven't yet checked the other two characterizations you propose in conjecture 3.15.

Additionally, since you mentioned it in your next message, the current proof I have of this characterization of exponentiable VDCs goes through the characterization of exponentiable morphisms of VDCs, which admits a similar description.

Nathanael Arkor (Aug 20 2025 at 06:00):

John Onstead said:

"free cocompletion" (which I guess is always given by a relative lax idempotent monad by definition)

A free cocompletion actually has a stronger universal property than a lax-idempotent relative pseudomonad (one way to see this must be the case is that not every lax-idempotent pseudomonad on Cat corresponds to a free cocompletion, e.g. as discussed in Power–Cattani–Winskel's A representation result for free cocompletions). The universal property I think is appropriate is the one discussed by @Dylan McDermott in this talk last year. But certainly every free cocompletion induces a lax-idempotent relative pseudomonad.

Nathanael Arkor (Aug 20 2025 at 06:17):

John Onstead said:

I guess my next follow up would be this: might it be possible to reconstruct the virtual equipment structure on $\mathrm{DblCat}$ from the functor $\mathbf{\mathbb Span}^{\mathbb A^{\text{op\,t}}}$

You can certainly construct the underlying "unary virtual equipment", but I don't see a way to obtain the multiary cells.

Nathanael Arkor (Aug 20 2025 at 06:19):

John Onstead said:

(Maybe we could call these "virtual free cocompletions" to keep the analogy in line?)

I think any notion of "free cocompletion" ought to admit, essentially by definition, left extensions along the embedding of any functor into a free cocompletion, otherwise it is not "cocomplete" in a reasonable sense. So I think it is more helpful simply to distinguish between presheaf constructions and free cocompletions (even though there are many settings where they coincide).

Nathanael Arkor (Aug 20 2025 at 06:35):

Ea E T (they/them) said:

Hi, here are my slides that Kevin is referring to (in powerpoint and pdf formats if one doesn't work):

Thanks, this looks really nice and I'm excited to read about it!

A few comments:

• In case you aren't aware, Soichiro Fujii and Steve Lack have reported that they have a sufficient condition for exponentiability of morphisms of VDCs (and they indicated their paper would be ready reasonably soon). I mention this in case it affects the timeline for your paper at all (Soichiro and Steve's results hold in more general contexts than for VDCs, so I expect they might be less disappointed to have their preprint come out second).
• Kawase does not prove in [Kaw25] that D-Mat or D-Prof are free cocompletions. He only proves characterisation theorems for them (which is, however, inspired by the perspective that they ought to be free cocompletions). On the other hand, in my talk, I do report a proof that they are free cocompletions (although under a slightly different notion of colimit than Kawase). I am hoping to finish this paper relatively soon.
• The virtual double category of categories and distributors is not the sub-VDC of Cospan(Cat) spanned by the two-sided codiscrete cofibrations, so I am a little bit suspicious of the multiary cells in the VDC you call BimodVDC. (I am actually not convinced it makes sense to consider multiary cells involving loose distributors/bimodules and functors, because multiary natural transformations intuitively correspond to a notion of "composition of loose heteromorphisms", but one should not expect any kind of composition of loose heteromorphisms in general. This is connected with the virtual triple category of VDCs.)

John Onstead (Aug 20 2025 at 07:33):

Nathanael Arkor said:

But certainly every free cocompletion induces a lax-idempotent relative pseudomonad.

Ah ok. So there's a strict hierarchy that goes something like free cocompletion -> object in the image of relative lax idempotent 2-monad -> presheaf object.

Nathanael Arkor said:

I think any notion of "free cocompletion" ought to admit, essentially by definition, left extensions along the embedding of any functor into a free cocompletion, otherwise it is not "cocomplete" in a reasonable sense. So I think it is more helpful simply to distinguish between presheaf constructions and free cocompletions (even though there are many settings where they coincide).

I see. I always think it's interesting when things we take for granted in the usual case (the presheaf category is also the free cocompletion, for instance) become divergent in general. Before learning CT I always thought it was the other way around- that as you generalize, more and more things converge.

Nathanael Arkor (Aug 20 2025 at 07:50):

John Onstead said:

Ah ok. So there's a strict hierarchy that goes something like free cocompletion -> object in the image of relative lax idempotent 2-monad -> presheaf object.

One needs to be a little careful, because although a lax-idempotent relative pseudomonad does induce an equipment with presheaf objects, it is not true that if you take a lax-idempotent pseudomonad on the underlying 2-category of a virtual equipment, then it gives you presheaf objects for that virtual equipment.

Nathanael Arkor (Aug 20 2025 at 07:51):

In general, I don't think the notion of lax-idempotent relative pseudomonad is an appropriate concept in the context of formal category theory, because it has no interaction with the loose morphisms.

Nathanael Arkor (Aug 20 2025 at 07:52):

However, once you "fix" the definition of lax-idempotent relative pseudomonad so that it does interact appropriately with the loose morphisms, you get the notion of free cocompletion Dylan and I consider. In other words, the formal notion of free cocompletion is the replacement for lax-idempotent relative pseudomonads in formal category theory.

Nathanael Arkor (Aug 20 2025 at 07:54):

John Onstead said:

I see. I always think it's interesting when things we take for granted in the usual case (the presheaf category is also the free cocompletion, for instance) become divergent in general. Before learning CT I always thought it was the other way around- that as you generalize, more and more things converge.

It's often the case in mathematics that when you have equivalent characterisations of objects in some setting, when you look at the analogous conditions in more general settings, the equivalent characterisations no longer coincide in general. However, the different conditions each capture many more things, because the setting is more general. So it's a combination of both.

James Deikun (Aug 20 2025 at 09:18):

Nathanael Arkor said:

• In case you aren't aware, Soichiro Fujii and Steve Lack have reported that they have a sufficient condition for exponentiability of morphisms of VDCs (and they indicated their paper would be ready reasonably soon). I mention this in case it affects the timeline for your paper at all (Soichiro and Steve's results hold in more general contexts than for VDCs, so I expect they might be less disappointed to have their preprint come out second).

For $T$-categories in general, a characterization of exponentiable $T$-categories would lead to a characterization of exponentiable $T$-functors, since the slice of $T\text{-}\mathbf{Cat}$ over $\mathbb{X}$ is actually just $\mathbf{\mathbb X\text-Alg\text-Cat}$. And I think the obvious extension of your version of malleability actually should work in that generality.

Nathanael Arkor (Aug 20 2025 at 09:32):

Yes, this is the approach @Matt Earnshaw and I had been taking (though we decided to wait until Soichiro and Steve's paper is out before continuing, to avoid potential wasted effort).

John Onstead (Aug 20 2025 at 10:24):

Nathanael Arkor said:

it is not true that if you take a lax-idempotent pseudomonad on the underlying 2-category of a virtual equipment, then it gives you presheaf objects for that virtual equipment.

In general, I don't think the notion of lax-idempotent relative pseudomonad is an appropriate concept in the context of formal category theory, because it has no interaction with the loose morphisms.

I think I understand... I should think of relative lax idempotent monads as less being tools in formal category theory, and more a device on a bicategory that induces a structure of formal category theory onto that bicategory. So they are useful when you start with a bicategory- with no loose morphisms- and want to do formal category theory with it by choosing a (potentially non-unique) equipping of loose morphisms/proarrows. But once you have made the choice, then you can begin to work within that setting and not really care so much about the relative monad anymore.

Nathanael Arkor (Aug 20 2025 at 10:34):

It's true that one can do this, but in practice I think it's almost always more natural to just start with a virtual equipment. If you start with lax-idempotent relative pseudomonads, for instance, you can't recover the virtual double category of locally small categories and distributors, only the double category of small categories and distributors.

Nathanael Arkor (Aug 20 2025 at 10:35):

I think lax-idempotent pseudomonads can be a useful tool for working in 2-category theory in contexts outside of formal category theory, but for the purposes of formal category theory, they're usually not the best tool for the job.

Ea E T (they/them) (Aug 20 2025 at 18:12):

Nathanael Arkor said:

Ea E T (they/them) said:

Hi, here are my slides that Kevin is referring to (in powerpoint and pdf formats if one doesn't work):

Thanks, this looks really nice and I'm excited to read about it!

A few comments:

• In case you aren't aware, Soichiro Fujii and Steve Lack have reported that they have a sufficient condition for exponentiability of morphisms of VDCs (and they indicated their paper would be ready reasonably soon). I mention this in case it affects the timeline for your paper at all (Soichiro and Steve's results hold in more general contexts than for VDCs, so I expect they might be less disappointed to have their preprint come out second).
• Kawase does not prove in [Kaw25] that D-Mat or D-Prof are free cocompletions. He only proves characterisation theorems for them (which is, however, inspired by the perspective that they ought to be free cocompletions). On the other hand, in my talk, I do report a proof that they are free cocompletions (although under a slightly different notion of colimit than Kawase). I am hoping to finish this paper relatively soon.
• The virtual double category of categories and distributors is not the sub-VDC of Cospan(Cat) spanned by the two-sided codiscrete cofibrations, so I am a little bit suspicious of the multiary cells in the VDC you call BimodVDC. (I am actually not convinced it makes sense to consider multiary cells involving loose distributors/bimodules and functors, because multiary natural transformations intuitively correspond to a notion of "composition of loose heteromorphisms", but one should not expect any kind of composition of loose heteromorphisms in general. This is connected with the virtual triple category of VDCs.)

Thanks for the insight and advice!

John Onstead (Aug 20 2025 at 18:55):

This might be tangential to the discussion, but I was particularly interested in Remark 7.3 in your paper after you've defined presheaf objects in a virtual equipment. This is because it makes a direct comparison with Koudenburg's formal category theory in an augmented VDC (aVDC), and I had been wondering how that aligned with the usual formal category theory in a virtual equipment. The paper seems to partially answer this by stating that, up to a choice of convention, virtual equipment presheaf objects are a "strict analogue" of the aVDC presheaf objects.

John Onstead (Aug 20 2025 at 18:55):

But this raises a few important questions. First, is there a (essentially injective on objects) functor $F: \mathrm{VEquip} \to \mathrm{aVDC}$ that sends a virtual equipment to the aVDC with "the same" internal formal category theory, IE such that the presheaf objects in the virtual equipment sense become the presheaf objects in Koudenburg's aVDC sense? And if so, then what of the aVDCs that don't arise from a virtual equipment in this way? Can one still do formal category theory with them- and if so, wouldn't this imply that formal category theory in an aVDC is strictly more general than formal category theory in a virtual equipment?

John Onstead (Aug 20 2025 at 18:55):

(Koudenburg's original paper seems to suggest this by stating how "augmented virtual equipments" are more general than "unital virtual equipments", and seems to imply that these "unital virtual equipments" are precisely the aVDCs that arise from standard virtual equipments, but the paper has always been confusing to me so I could be completely getting the wrong message there.)

Nathanael Arkor (Aug 21 2025 at 07:59):

John Onstead said:

The paper seems to partially answer this by stating that, up to a choice of convention, virtual equipment presheaf objects are a "strict analogue" of the aVDC presheaf objects.

The choice of strictness is independent of augmentation. One could work strictly in either framework. We choose to work strictly because it is simpler and captures all the examples we have in mind, which we think suggests it is the most appropriate notion.

Nathanael Arkor (Aug 21 2025 at 08:03):

Formal category theory in a virtual equipment is a special case of formal category theory in an augmented virtual equipment. However, a framework is not automatically better just because it is more general. I think the most important thing is whether a framework captures the examples. I don't know of any examples of augmented virtual equipments that are not virtual equipments that I think are interesting examples. The only example Koudenburg gives is starting with a virtual equipment and then taking a sub-augmented virtual equipment of it (e.g. large categories and small distributors). While this is useful for making a formal connection to Yoneda structures (which is useful for historical context), I'm not convinced this is an interesting example; it seems artificial to limit the size of objects and loose morphisms differently.

Nathanael Arkor (Aug 21 2025 at 08:04):

In my opinion, working with VDCs is simpler than working with AVDCs, without losing any interesting examples.

John Onstead (Aug 21 2025 at 19:21):

Nathanael Arkor said:

Formal category theory in a virtual equipment is a special case of formal category theory in an augmented virtual equipment. However, a framework is not automatically better just because it is more general. I think the most important thing is whether a framework captures the examples. I don't know of any examples of augmented virtual equipments that are not virtual equipments that I think are interesting examples.

Ah, that makes sense. Thanks for all your help!