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: James Deikun

James Deikun (Dec 29 2022 at 03:31):

(In the context of my conjectures on generalized equipments)

I've pretty much worked out what the generalized $\mathrm{Mod}(-)$-construction in $T(\mathrm{Str\omega{}Cat})$ looks like. The result is basically, objects of $\mathrm{Mod}(X)$ are strict $\omega$-cats internal to $X$, arrows are strict $\omega$-functors internal to $X$, $n$-dimensional pro-globes are "modules" in a fairly intuitive way and $n+1$-dimensional cylinders are their strict maps. I'm also fairly convinced that the construction adds the right kind of "units" to make the "display" construction work--at any rate as convinced as I am for the virtual double category case! (I understand how to factor squares through the opcartesian morphism but not why the factorization is unique.)

James Deikun (Dec 29 2022 at 13:23):

There are really some interesting subtleties in the definition of "barrel" for higher shapes like squares. For barrels to be algebras closed under the operations, you need to allow, for example, a unary square whose source lives over a point, to live over a nullary square. So far I've been treating squares of different arity as basically independent of each other as they aren't, for example, facets or anything, but it's not like anything goes (you can't have arrows and proarrows living over each other in a nontrivial way) so this indicates there needs to be some relation between them derived somehow from the operations they represent, or front-loaded in the case of e.g. strict $\omega$-cats. It seems like this is the same data that is needed to specify what "units" are probably. I still haven't found a better way to express that information than just drawing all the terminal barrels and being like "it's a barrel if it maps into that and preserves the facet inclusions", nor a formal way to induce the terminal barrels for $T(O)$ from the barrels and operations for $O$.

It is, however, pretty intuitive and I feel like I understand the "monoids and modules" construction way better than before even in the plain virtual equipment setting.

James Deikun (Dec 29 2022 at 14:06):

The rules for what can "live over" what in a barrel are starting to make some sense. It's basically similar to a kind of higher-dimensional graph minors, where if you contract away facets from $\partial X$ in the mapping/minorization and get $\partial Y$ (or $Y$ itself in some cases) then $X$ can live over $Y$. Need to see how this looks in the $\mathrm{Str\omega Cat}$ and 3-equipment cases where the boundaries can get more "interesting".

James Deikun (Dec 29 2022 at 14:42):

It seems to work fine in all the cases, as long as the barrel is over something "locally simply connected"--you don't have the same item occurring as two different facets of the same shape. Then a barreling of an algebra $A$ over a graph $G$ is a map $b$ from the cells of $A$ to the cells of $G$ so that:

1. If $b(a)$ is the same "kind" of object as $a$ in "the intuitive sense" (i.e. arrows and proarrows are different, but all squares are the same regardless of arity), then $b(\partial a) = \partial b(a)$.
2. Otherwise, $b(\partial a) = b(a)$.

Remaining: maybe something more robust than set mapping to handle barrels over interesting graphs; definitely some way to carry and synthesize the "intuitive sense of kind".

James Deikun (Dec 29 2022 at 14:56):

It might be possible to supply both desiderata at once by having some sort of category structure (on shapes? graphs?) that specifies when one thing is a 'contraction' of another. Might be similar to degeneracies. Maybe we even want them around when making "unitary" algebras, at least in some "weak" way, to bring in the units and their opcartesian morphisms.

James Deikun (Dec 29 2022 at 15:08):

Yeah, okay, with a nice system of degeneracies on shapes barrels get really simple: a barreling of $A$ over $G$ is a presheaf map from $A$ to the closure of $G$ under degeneracies. This is still a little simpler than specifying all the terminal barrels, though a bit more complex than "same kind". I have more confidence in it though ...

James Deikun (Dec 29 2022 at 17:17):

Where do the degeneracies come from? For virtual double categories, the degeneracies among just squares look like the degeneracies of the simplex category, 1, 2, 3 as you go up one-by-one in arity, $C(n,k)$ as you skip $k$ many; however there are extra generators: from a point you get a degenerate looping arrow or proarrow, from an arrow a degenerate nullary square with the arrow on both sides and a degenerate target, from a proarrow a degenerate unary square the shape of an identity square for it.

For virtually-thickened strict $\omega$-cats, you get, in the cylinders, a copy of the sensible degeneracies for globular pasting diagrams, plus from any globe you get its "identity cylinder" shape, and its "reflexive globe" shape, plus you get degeneracies (of cylinders again) that correspond to using reflexivity on the target. I can see how the former matches up as special cases of this when you limit to 0- and 1-globes as shapes.

For the virtual thickening of the trinary-operation planar operad ("odd multicategories"), the shapes are objects plus corollas with an odd number of in-leaves. For degeneracies it seems like you get: the identity shape from objects, tripling an in-leaf, plus three ways of tripling the output and bending two copies back. This is a nice example since the original operad has no (room for) nontrivial degeneracies among shapes so these must all arise from operations, compositions and/or dependencies somehow.

James Deikun (Dec 29 2022 at 17:53):

Speculation on how to get degeneracies somewhat systematically: an $\mathrm{Obj}$-barrel must simply be an algebra, so $\mathrm{Obj}$ must be initial/terminal in the category of degeneracies. This gives you enough information to build the terminal $\mathrm{Obj}$-barrel. Then, building up the degeneracies and terminal barrels for each shape inductively, you must have enough degeneracies to include all the compositions of the seed shape with stuff already in the boundary of its terminal barrel.

One thing I can't see that approach getting you, though, is the 2-cells in the terminal barrel for arrows, in virtual double categories. It would seem to be "totally fair" to have no 2-cells at all in there, as nothing guarantees such cells to exist in a virtual double category. "Arrow-barrel" would just be a much more restrictive concept, but it wouldn't be impossible to produce examples. Maybe this has to do somehow with inheriting degeneracies from the original operad-with-shapes. The operad with shapes for categories does have an existing degeneracy from object to looping arrow (inherited as proarrow) and that degeneracy is directly useful for inheritance since proarrows no longer have composition; but I don't see a connection between this and the generator from arrows to squares.

James Deikun (Dec 29 2022 at 18:00):

Oh, wait: the generator from arrows to squares is a picture of the generator from objects to (pro)arrows. That must (?) be significant: when you inherit a generator, you must get some kind of pictures of it too. But what is the process to generate them from the thing they're picturing? (Another example of this is the reflexivize-targets-of-cylinders generator, coming from the inherited reflexivize-(pro)globes generator.)

Christian Williams (Dec 29 2022 at 20:38):

I'm constructing the fibrant triple category of fibrant double categories (the 3-equipment of equipments), if you ever want to talk.

James Deikun (Dec 29 2022 at 20:41):

Certainly.

James Deikun (Dec 29 2022 at 21:33):

Continuing from before, probably $T(\mathrm{Str\omega Cat})$ is the best example to look at since it has so many more occurrences of the pattern than VDCs. In $\mathrm{Str\omega Cat}$ we can always view an $n$-dimensional pasting diagram as an $(n+1)$-dimensional pasting diagram that is "nullary", and pasting that way is equivalent to pasting the $n$-dimensional way and then taking the identity on the result. I guess what I'm getting from this is that when two operations have the same input and their result is related by a degeneracy, then the new shapes from those operations are also related by a degeneracy?

James Deikun (Dec 29 2022 at 21:52):

Or maybe that's only a condition for it; maybe "degeneracies of operations" need to be tracked as such and nullary compositions are born with them.

James Deikun (Dec 29 2022 at 22:55):

Not sure if this is the best way to express the compatibility of degeneracies with composition, but the closure under degeneracies of a representable $O$-graph should have a unique $O$-algebra structure.

John Baez (Dec 30 2022 at 11:55):

Christian Williams said:

I'm constructing the fibrant triple category of fibrant double categories (the 3-equipment of equipments), if you ever want to talk.

It's probably better to call it a '2-equipment', since it's one step up the categorical ladder from equipments, not 2.

James Deikun (Dec 30 2022 at 13:59):

To me the default equipment is a 2-equipment, a set is a 0-equipment, and a category is a 1-equipment ... do we really want a ladder where a set is a (-1)-equipment? Where a category is a 0-equipment?

James Deikun (Dec 30 2022 at 14:35):

I was missing something obvious about the degeneracies of the arrow and so on; you can paste a nullary square in the tip of the distinguished arrow to the distinguished arrow to get the nullary square over the distinguished arrow that starts it all out. This seems to work for the other cases as well, so there seems to be no need after all to track degeneracies on operations or distinguish "nullary" operations from operations in general just to get barrels/degeneracies right.

Christian Williams (Dec 30 2022 at 18:32):

For me the word "equipment" is completely unhelpful, and I think it should be replaced asap, because the concept is too important: in this structure the language of category theory is unified.

"Fibrant double category" tells you exactly what matters: we use both functions and relations, and we can substitute the former into the latter. (and generalizes to fibrant n-tuple category)

But since it's long, I really want to find a good abbreviation of the phrase. If anyone has ideas please let me know.

James Deikun (Dec 30 2022 at 18:35):

If anything the word should be "category", but that ship has already sailed two or three times.

Christian Williams (Dec 30 2022 at 18:39):

Yeah, maybe. This may be controversial in academia, but I think conventions are only "set in stone" when they are publically understood, not just by a subcommunity.

Christian Williams (Dec 30 2022 at 18:42):

Why do you want to call them categories? And then what would you call categories?

Christian Williams (Dec 30 2022 at 18:50):

Or to put it more simply/personally - I reserve the right to replace a term if I think it's helpful, and accept that its fate will be determined by community response.

Christian Williams (Dec 30 2022 at 18:50):

Sorry for the tangent; I do want to catch up on what you're doing here.

James Deikun (Dec 30 2022 at 18:52):

I would call (1-)categories "categories", and the existing higher categories something like "narrow n-categories".

James Deikun (Dec 30 2022 at 18:54):

Much like the attempt to replace "weak n-category" with "n-category" and "n-category" with "strict n-category" which has been ... semi-successful.

Christian Williams (Dec 30 2022 at 18:56):

Oh, yeah but so what would you call equipments?

James Deikun (Dec 30 2022 at 18:57):

"Equipments" or "fibrant double categories" I would call "2-categories".

Christian Williams (Dec 30 2022 at 18:58):

ah, yes... this is very simple and I think I support it.

Christian Williams (Dec 30 2022 at 19:08):

but then what would you call a double category that's not fibrant / not an equipment? (though I do agree that being fibrant should be the default, because that is the concept of universality via representable profunctor).

James Deikun (Dec 30 2022 at 19:10):

Probably "double 1-category" or maybe some evocative red herring adjective like "stiff 2-category" ...

Christian Williams (Dec 30 2022 at 19:12):

yeah, it's stiff because it doesn't know how to "bend" tight morphisms into loose ones. that's good.

James Deikun (Dec 31 2022 at 14:31):

The shape category of an "operad with shapes" $O$ is a direct category $S(O)$ with finite fan-in. The operations can be viewed as a category $\mathrm{Op}(O)$ equipped with a discrete fibration $\mathrm{cod} : \mathrm{Op}(O) \to S(O)$ and a profunctor $\mathrm{dom} : \mathrm{Op}(O) ⇸ S(O)$ such that the collage of the whole diagram (and thus also $\mathrm{Op}(O)$) is direct with finite fan-in. The specifications exist as the arrows in $\mathrm{Op}(O)$ and the action of the profunctor $\mathrm{dom}$.

So far what has been specified is more like a "collection with shapes" than an "operad with shapes". Given two such collections $X, Y$ with the same shapes $S$, there is a monoidal product where the operations of $X \circ Y$ are operations $x$ of $X$ equipped with consistent labellings of $\mathrm{dom}(-,x)$ by operations of $Y$. "Consistent" means that: you have a $S$-set morphism from $\mathrm{dom}(-,x)$ to $\mathrm{Op}(Y)$ (viewed as a presheaf via $\mathrm{cod}_Y$). $\mathrm{cod}_{X \circ Y}$ is basically inherited from $X$ and $\mathrm{dom}_{X \circ Y}$ is obtained from $\mathrm{dom}_Y$ pointwise by gluing along the category of elements of $\mathrm{dom}(-,x)$. (A concern: does this actually exist in all cases? I think it does though since it looks pointwise like a colimit in a presheaf category...) Then an operad with shapes $S$ is a monoid in this monoidal category.

(It would be nice to have a form of this definition that didn't do so much equivocation between presheaves and discrete fibrations.)

James Deikun (Dec 31 2022 at 15:07):

A further conjecture related to this: A $T(O)$-algebra with one object is, when this is meaningful, the same thing as an operad with the shapes $S(O)$ over $O$, generalizing from Leinster in the case of globular operads.

James Deikun (Dec 31 2022 at 15:31):

You can turn a $S$-set into a collection with shapes $S$ by making $\mathrm{Op}$ the category of elements, $\mathrm{cod}$ the corresponding projector, and $\mathrm{dom}$ pointwise the empty $S$-set. Then this gives rise to an actegory structure and a (cartesian? probably/hopefully) monad $M(O)$ describing the $O$-algebras for each $O$ per the discussion in [[operad]] ("The monad attached to an operad"). I speculate hopefully that $M(T(O)) = M(O)'$ (prime a la Leinster).

James Deikun (Dec 31 2022 at 15:58):

A category on the same objects as $C$ with added morphisms can be given by a $\mathbb{P}\mathrm{rof}$-monoid on $C$, while a factorization system can be given as two $\mathbb{S}\mathrm{pan}(\mathrm{Set})$-monoids on the same object with a distributive law between them. Is there some way to combine these constructions so you can add the $E$ part of an $(E,M)$-factorization system in $\mathbb{P}\mathrm{rof}$?

Mike Shulman (Dec 31 2022 at 20:29):

Re: changing the meaning of the word "category": NO!

Mike Shulman (Dec 31 2022 at 20:30):

I can confidently predict that if you try to do that, the "community response" will be very negative, not only towards the attempted change of terminology, but towards the rest of your work by association.

James Deikun (Dec 31 2022 at 20:35):

Personally I'm happy to stick with "equipment" for about 10 or 20 more years until either that's no longer the case or "equipment" has legs of its own. I just want the default index of "equipment" to be 2 ...

James Deikun (Dec 31 2022 at 20:37):

What I don't want is to constantly rotate on the "next best thing" so that nobody outside can keep track of how things are developing.

Mike Shulman (Dec 31 2022 at 21:14):

My own opinion is that the really important structure where all of category theory is unified, including "multi-variable" notions, is a "compact closed equipment". This structure has yet to be precisely defined and studied (although Christian and I have had some ideas), and so I think rather than trying to rename ordinary equipments, it would be better to spend some time thinking of a new and snappy name for the compact closed ones. In some previous abortive work in that direction with Patrick Schultz, we used the word "kit" (Australian slang meaning something kind of like "equipment" or "outfit", I believe), but one can probably do better than that.

James Deikun (Dec 31 2022 at 21:20):

I can definitely see wanting duals, but it seems almost too on-the-nose to me in that a lot of nice generalizations of categories don't have $^{\mathrm{op}}$ ...

James Deikun (Dec 31 2022 at 21:31):

Treating degeneracies for now as a simple $\mathbb{P}\mathrm{rof}$-monoid on $S$, trying to come up with an $S$-collection [[actegory]] structure on profunctors. So far what I've come up with is making them into an $S$-collection themselves by taking the graph of the profunctor, using the fibrant projection as $\mathrm{cod}$, and making $\mathrm{dom}$ the profunctor represented by the opfibrant projection. This has the unfortunate effect of kind of hiding the coaction of the profunctor but it might work anyway. The idea is to put an algebra structure on degeneracies as a whole, in a way consistent with the category and factorization structure ...

Mike Shulman (Dec 31 2022 at 22:06):

I don't know too many generalizations of categories that lack duals but with which one can actually do a substantial amount of category theory. What do you have in mind?

James Deikun (Dec 31 2022 at 22:25):

Ordinary multicategories for one.

Mike Shulman (Dec 31 2022 at 23:29):

What sort of category theory can you do with multicategories that needs more than the 2-category of them? I've tried to make something useful come out of formal category theory in the obvious equipment of multicategories, but for the most part what drops out didn't seem correct or useful.

James Deikun (Dec 31 2022 at 23:40):

I don't know what else yet, but surely you need the equipment for correct definitions if you enrich them. What all kind of things have you tried? Also, I don't think the equipment on toposes has duals, and there are definitely at least a few interesting things you can do there, although limits/colimits have disappointed me so far.

James Deikun (Dec 31 2022 at 23:48):

It's starting to seem like the above lifting of $S$-endoprofunctors to $S$-collections preserves composition? Am I hallucinating? I certainly didn't expect this from such a heap of ad-hockery. If it's true it's definitely a reason to like it.

James Deikun (Jan 01 2023 at 01:36):

Well, it definitely doesn't preserve nullary composition.

James Deikun (Jan 01 2023 at 01:50):

The super-simple option -- take $\mathrm{cod}$ as $\mathrm{Id}$ and $\mathrm{dom}$ as the profunctor -- doesn't work here for other reasons. It means you would get one operation for each shape and the arity of the operation would be "all the facets of the shape and all their degeneracies pasted together along facets" -- it would be, generally, an infinitary operation, and it would not read out the information needed for closing things up.

Nathanael Arkor (Jan 01 2023 at 02:05):

Mike Shulman said:

I don't know too many generalizations of categories that lack duals but with which one can actually do a substantial amount of category theory. What do you have in mind?

V-enriched category theory for nonsymmetric V is one obvious candidate, no?

James Deikun (Jan 01 2023 at 02:21):

The more complicated option above, though: it has as operations the heteromorphisms with sources as codomains and (presheaf represented by the) targets as codomains. In the case at hand, this means an operation is a way of taking a facet of the (always representable/"unary") domain and degenerating it into the shape of the codomain. If you start with the identity profunctor, though, then an operation is a way of taking a codomain-shaped facet of the domain. I think this lifting lands in a subcategory of $S$-collections that all have these faceting operations, and they all laxly absorb the lifting of the identity, and composition is laxly preserved ... in all cases you miss out on quotienting away the action in the middle because the $S$-collection product doesn't do that or have a way to do it.

James Deikun (Jan 01 2023 at 02:50):

Maybe the solution to the laxness (and some other stuff) is to take the degeneracies as a collection in the first place! Degeneracies can be degeneracies alone, not mixed with faces. The facets of the degeneracies-as-operations can represent the composition table for degeneracies getting precomposed by faces, outputting degeneracies postcomposed by faces like you normally can get uniquely in a Reedy category. Then the endoprofunctor (and the monoid structure on it) can be recovered from the collection (and its monoid structure?).

James Deikun (Jan 01 2023 at 03:56):

Yes! The degeneracies for $O$ should be an $S(O)$-operad! This nicely gives the composition table for the degeneracies among themselves. This works beautifully except ... well it doesn't make a very good $O$-algebra! The problem is, the product $O \circ D$ still contains all these things with domains shaped like pasting diagrams, but $D$ only has operations with representable domains, so an action just isn't definable. This on the one hand defeats the entire original purpose of making $D$ a collection in the first place. On the other hand, this is a pretty nice presentation of the data needed to complete a direct category to a Reedy category, so I think I'll keep it anyway?

James Deikun (Jan 01 2023 at 04:18):

Maybe instead of an action of $O$ on $D$, I should be looking at a distributive law, a map from $O \circ D$ to $D \circ O$? Looks somewhat promising, but there's seemingly a lot of space for arbitrariness to crawl in when it comes to "identity shape on" operations versus actual degeneracies doing the lifting. Maybe there's a way to leave this as a choice, make it systematically, then squish it down later when making barrels? Ugh.

James Deikun (Jan 01 2023 at 05:02):

The distributive law idea doesn't really seem very good after all. Maybe I actually got too distracted by the idea of degeneracies in the first place; after all, the idea was originally to complete a simple shape to an algebra in a way suitable to mapping into., keeping in mind that anything could live over an object. Maybe there's a simpler way to do that.

James Deikun (Jan 01 2023 at 19:56):

For the new year I'm going to try something new: working with Cartesian monads directly! I'm starting out by trying to figure out when (small) $T$-multicategories are a special case of $V$-enriched $T$-multicategories; to keep from drowning in huge diagrams I am trying to axiomatize the $I$ (indiscrete) functor from Leinster. It seems that it is a reflective subcategory inclusion of $\mathcal{E}$ in $(\mathcal{E},T)$-categories and its underlying functor $I_0$ into $(\mathcal{E},T)$-graphs is also one. The left adjoints are maybe even fibrations? And the left adjoint of $I_0$ commutes with $T'$.

James Deikun (Jan 01 2023 at 22:44):

Okay, I think the desired situation for enriching a thing is: $\mathcal{E}$ is a category fibered over $\mathcal{O}$, with $I_0$ right adjoint to the fibration. $T$ is a cartesian monad on $\mathcal{E}$ fibered over $\mathcal{O}$. $I$ is $I_0$ pointwise equipped with the unique possible $T$-algebra structure.
Then you can define a "$T$-multicategory" to be a monoid in $\mathbb{S}\mathrm{pan}(\mathcal{E},T)$, $M(\alpha)$ to be the canonical $T$-multicategory on $TA \xleftarrow{\mathrm{id}} TA \xrightarrow{\alpha} A$ for $\alpha$ a $T$-algebra, plus the evident functor action, and finally:

An "$V$-enriched $T$-algebra" $C$, for $V$ a $T$-multicategory, is an object $C_0$ of $\mathcal{O}$, equipped with a $T$-multicategory map $C_1 : MI(C_0) \to V$.

Mike Shulman (Jan 01 2023 at 23:13):

James Deikun said:

I don't know what else yet, but surely you need the equipment for correct definitions if you enrich them. What all kind of things have you tried?

Well, internal notions in the 2-category of enriched multicategories don't suffice, but that doesn't mean that the equipment of them does suffice. My memory is that limits in the equipment of multicategories may be right, but colimits don't come out to be what one would want a colimit in a multicategory to be. Also one hopes maybe that universal arrows would be some kind of colimit in such an equipment, but they aren't.

Mike Shulman (Jan 01 2023 at 23:16):

Nathanael Arkor said:

V-enriched category theory for nonsymmetric V is one obvious candidate, no?

Yes, that's about the only example I know of where you don't have duals or tensor products, but you do get something meaningful from equipment-theoretic limits and colimits. (Well, and its generalization to W-enriched category theory for a bicategory W.) But nonsymmetric enrichment is pretty rare, compared to the vast amount of category theory for which you need duals and tensors.

Mike Shulman (Jan 01 2023 at 23:18):

Actually, although I paraphrased the comment about "all of category theory being unified", I think it's a mistake to even look for one structure in which all of category theory can be unified. It's certainly a mistake to focus too much on $n$-categories as the only face of higher category theory, but it's likewise a mistake to focus too much on double categories or equipments. Higher category theory is so much richer than that -- it's an immense zoo of fascinating structures that are related to each other in many ways.

James Deikun (Jan 01 2023 at 23:44):

In order to recover actual small $T$-algebras from an enrichment, it's necessary to pick an appropriate $V$.

$V$ looks like : $TV_0 \xleftarrow{dom} V_1 \xrightarrow{cod} V_0$ plus some monoid structure. The first requirement is for a map from $MI(C_0)$ to $V_0$ to be able to pick out any small object $A$ in the $\mathcal{E}$-fiber over $C_0$. An example of such an object, when $O$ is $\bold{Set}$, $\mathcal{E}$ is $\bold{Quiver}$, and $T$ is the free category monad, is the quiver with a universe worth of loops on a single point. I think the general thing one is looking for here is a "vertical morphism classifier" of some sort in $\mathcal{E}$.

James Deikun (Jan 02 2023 at 00:22):

Given a vertical morphism classifier (which I probably will return to later), the next thing that's required is to somehow be able to recover a map $\alpha : TA \to A$ -- with the right conditions on it to be a $T$-algebra -- from a map $f_1 : TI_0(C_0) \to V_1$ with certain commutation conditions.

Nathanael Arkor (Jan 02 2023 at 01:56):

Mike Shulman said:

Nathanael Arkor said:

V-enriched category theory for nonsymmetric V is one obvious candidate, no?

Yes, that's about the only example I know of where you don't have duals or tensor products, but you do get something meaningful from equipment-theoretic limits and colimits. (Well, and its generalization to W-enriched category theory for a bicategory W.) But nonsymmetric enrichment is pretty rare, compared to the vast amount of category theory for which you need duals and tensors.

I suspect categories internal to a nonsymmetric monoidal category with equalisers gives another example, but I never checked for want of examples.

James Deikun (Jan 02 2023 at 12:52):

If fibers of $\mathcal{E}$ are closed under (vertical) pullback, then any universe in $\mathcal{E}_1$ classifies vertical morphisms in $\mathcal{E}$. I think this condition is necessary anyway to have a monad that's both Cartesian and fibered? (If it isn't i think I'm willing to stipulate it as part of the setup ...)

James Deikun (Jan 02 2023 at 13:54):

Nathanael Arkor said:

I suspect categories internal to a nonsymmetric monoidal category with equalisers gives another example, but I never checked for want of examples.

Would the category of equaliser-preserving endofunctors on a category be an example?

James Deikun (Jan 02 2023 at 13:55):

(I mean of the thing you live in.)

James Deikun (Jan 02 2023 at 14:15):

According to the relations that hold around a functor of Burroni generalized multicategories, there must be two arrows into $V_1$, corresponding respectively to pulling back $T(\mathrm{el})$ along $\mathrm{dom}$ and $\mathrm{el}$ along $\mathrm{cod}$, and pulling them back along $f_1$ respectively give, in $\mathcal{E}_{C_0}$, the arrow $T!$ from $TA$ to $T1$ and the second projection of $A \times T1$. (This is probably some very painful plodding to someone more comfortable with the semantics of universes in type theory.)

James Deikun (Jan 02 2023 at 14:28):

This is reminding me of how you construct exponentials in an elementary topos as graphs of functional relations. Wonder how much of the apparatus you recover going the other way.

James Deikun (Jan 02 2023 at 16:41):

It seems like the essential ingredient for both this construction and the "$T$-multicategory of $U$-small $T$-algebras" construction is building a weak classifier/universe of $T$-algebras from a universe closed over $T$ and some other reasonable list of things to be closed over. Does anyone know a construction like this, either off-hand or in the literature?

James Deikun (Jan 02 2023 at 20:35):

(Particularly, it seems what's needed is where an arrow from $T1$ to the universe classifies an algebra, carrier included.)

James Deikun (Jan 02 2023 at 20:48):

(It's not the same as a universe in $\mathcal{E}^T$ -- in the case I'm looking for, if the arrow is of the form $Tf$ I think the algebra will turn out to be free on its carrier, assuming the universe is even of the form $TX$ making that possible.)

James Deikun (Jan 02 2023 at 23:14):

Actually in more detail: it's not a completely arbitrary arrow; it's a there's a morphism $f_0$ to a plain old universe that classifies the carrier, then $f_1$ is a chosen factorization of $Tf_0$ through the universe-of-algebras through the adjunct of a morphism from the free $T$-algebra on the universe-of-algebras to the free $T$-algebra on the plain old universe. So basically you can recover the carrier from $f_1$ but not every possible $f_1$ is sensible.

James Deikun (Jan 03 2023 at 14:32):

I've gotta say, all this thinking about universes really makes me appreciate the notion of fibered category and the externalization of an internal category! This makes me think: if the monad $T$ is [[parametric right adjoint]] instead of merely Cartesian, and $\mathcal{E}$ has an essentially small dense generating full subcategory $\mathcal{A}$, $T$ is automatically a [[monad with arities]] and its algebras can be externalized! In particular $\mathcal{A}_T$ is the essentially small full subcategory of $\mathcal{E}$ on objects whose $T$-image is under an object of $\mathcal{A}$ via a $T$-generic morphism. Then let $\Theta{}_T$ be the full subcategory of free $T$-algebras on objects of $\mathcal{A}_T$, and $j_T : \mathcal{A}_T \to \Theta{}_T$ the restriction of the free algebra functor. If I'm getting all this right, then an external $T$-algebra is a presheaf $\alpha$ on $\Theta{}_T$ such that $\alpha j_T^{\mathrm{op}}$ is naturally isomorphic to $\mathcal{E}(i_{\mathcal{A}_T} -, \mathrm{colim}_{\alpha j_T^{\mathrm{op}}} i_{\mathcal{A}_T})$. (This is not as super nice as I was hoping, but maybe it will still be nicer than messing with universes?)

James Deikun (Jan 03 2023 at 15:38):

Anyway what I would really like to externalize would be $T$-multicategories, not $T$-algebras. I think there's a lot less prior art on this!

James Deikun (Jan 03 2023 at 15:45):

Basically what I can think of is Hermida on (op)fibrations of multicategories, but that's done in such a way that to be properly "external" we already need an elementary description of the kind of multicategory in question.

James Deikun (Jan 03 2023 at 16:12):

I'm looking at the definition of local smallness of a fibration since that's the most interesting ingredient of recovering an internal category from a fibration. Basically it's talking about defining a fiberwise "hom" where the "hom" for two objects in a fiber doesn't have to actually live in the same fiber as them, and it's fiberwise because the hom between objects in different fibers can't be freely chosen but is dictated by the fiberwise homs and the structure of the base. TBH I'm not really understanding the role of the "evaluation map" in this definition since in the final construction it gets thrown away.

James Deikun (Jan 03 2023 at 20:02):

Maybe I should first try to construct "externalization" and then see what kind of properties it follows. I think probably the best way to do it is in PROP-style where both inputs and outputs are given as collections so arrows can be composed directly. Let $\bold{C} = TC_0 \xleftarrow{\mathrm{dom}_C} T_1 \xrightarrow{\mathrm{cod}_C} T_0$ be an internal $T$-multicategory in $\mathcal{B}$. For each object $I \in \mathcal{B}$ form a category $\bold{C}^I$ with

• objects: maps $X : I \to TC_0$ in $\mathcal{B}$.
• morphisms from $X$ to $Y$: maps $f : I \to TC_1$ with $\mu_T \circ \mathrm{dom}_C \circ f = X$ and $T(\mathrm{cod}_C) \circ f = Y$.
• identity morphisms given by composition with $T(\mathrm{ids}_C)$.
• composition given by getting an arrow into $TC_2$ via representability and preservation-by-$T$ of pullbacks and composing it with $T(\mathrm{comp}_C)$.

I would like to say this just involves turning $\bold{C}$ into an internal category in the Kleisli category $\mathcal{B}_T$, and doing normal externalization (via indexed categories) there. However, I'm not sure all the needed pullbacks actually exist in the Kleisli category or correspond to what they need to be. Perhaps it's best to try to understand it on its own terms.

James Deikun (Jan 03 2023 at 23:20):

I think via associativity of Kleisli composition it does turn out to be a split indexed/fibered category over $\mathcal{B}_T$, even if it doesn't get there in quite the usual way. It should have a bunch of other, not-particularly-smallness-related, properties though, coming from the fact that $\mathrm{cod}_C$, $\mathrm{ids}_C$, and $\mathrm{comp}_C$ enter in the form of free morphisms. What are these properties?

If you do this construction on a plain multicategory, you get:

• objects: indexed families of sequences of objects of the multicategory
• vertical morphisms: indexed families of sequences of morphisms of the multicategory that pick out their arguments in order
• cartesian morphisms: indexed families of sequences of indices; act by substitution on objects and morphisms.

Somehow the property seems like "all the morphisms are generated by the ones whose targets are free morphisms". But how to formalize that? Especially when you don't even "know" that objects are "really" families?

James Deikun (Jan 03 2023 at 23:31):

Probably somehow making use of the Cartesian morphisms which can still do reindexing without knowing something "is" a family in the first place ... there have to be relationships between $C_I$, $C_{TI}$ and $C_{TTI}$ ...

James Deikun (Jan 03 2023 at 23:36):

Then again, maybe there's an extra bit of structure, indicating where the "unary output" things lie, that shouldn't be forgotten, like with a [[category of operators]].

James Deikun (Jan 03 2023 at 23:54):

And actually the 1-output objects don't seem to carry all the information in a natural way; it seems like when externalizing a virtual double category you need the 0-input 0-output objects to get the arrows without having to attach them to any particular squares, which may not be forthcoming. So it seems like you need the outputs that are "shaped" by some kind of generator of $\mathcal{B}$, probably weaker than a dense generator though ... I find this so weird.

James Deikun (Jan 03 2023 at 23:55):

(Maybe this has more to do with which $I$ should get sampled, though.)

James Deikun (Jan 04 2023 at 00:00):

Yeah, I think it's still fine to only look at the things where the shape of the output is literally the quiver $I$, whatever quiver that is.

James Deikun (Jan 04 2023 at 00:49):

Let's look at strongly cartesian (p.r.a.) monads $T$ again just for fun ... there is a generic/free factorization system in $\mathcal{B}_T$ there and using it on arrows representing objects factors them into a generic cartesian arrow and a free arrow. Basically it's an "image factorization" where the generic cartesian arrow represents all the "reshaping" done and the free arrow is purely "labelling the generic shape". I think even without a strongly cartesian monad, you could indicate the class of objects that are "free" and they would be closed under following free cartesian arrows backward. Classes of objects are a bit odd, though, especially ones with such weak closure properties. And the free objects don't seem to do obvious things like form a [[coseparator]] in a fiber, or even the total category.

James Deikun (Jan 04 2023 at 01:18):

Is there any way a vertical arrow into a free object can be not a free vertical arrow (i.e. represented by a free arrow into $C_1$)? It's easy to see that a free vertical arrow must terminate at a free object (composition of two free arrows is free) but while intuitively "obvious" the converse would seem to imply a factorization property on free arrows that's not immediately evident (if $f \circ g$ and $f$ are free so is $g$). It's not true for the reader monad (where the functor is Cartesian but the unit isn't) but my go-to test Cartesian monads do have this property (but they might be strongly Cartesian and it might be only a property of strongly Cartesian monads).

James Deikun (Jan 04 2023 at 01:30):

As a side effect of all the looking into parametric right adjoints, I've discovered that my notion of an $S$-collection way up above is actually the same data as a p.r.a. endofunctor on $\mathrm{Psh}(S)$, and the composition seems to be the same too.

James Deikun (Jan 04 2023 at 01:32):

If the notion of map between $S$-collections is the same as a Cartesian natural transformation, then my $S$-operad is exactly a [[p.r.a. monad]] !

James Deikun (Jan 04 2023 at 02:28):

By using (1) the definition of a free algebra in the EM category (2) the definition of an algebra morphism (3) the identity of free morphisms in the EM category as ones of the form $Tf$ (4) the cartesianness of $\mu$'s naturality squares and (5) the two-pullback-square pasting lemma, I get something close to the factorization property I'm looking for, namely:

If $f \circ g$ and $f$ are free morphisms, $Tg$ is the pullback of $g$ along $\mu$ with other projection also $\mu$. Having some trouble getting from there to $g$ being actually free though.

James Deikun (Jan 04 2023 at 02:41):

By pasting naturality squares for $\eta$ instead I got it. Nice little puzzle. Actually looks like only $\eta$ has to be Cartesian to make this work!

James Deikun (Jan 04 2023 at 08:13):

Actually Definition 6.2.2 in Higher Operads, Higher Categories may hold a clue to a better way to define a "large $T$-multicategory". The slice over a universe object can be replaced with the Cartesian arrow category of $\mathcal{E}$, and the forgetful functor $U_E$ replaced with the restriction of the codomain fibration, resulting in a large discrete fibration instead of a small one, which is "almost representable" as only size issues prevent it. Similarly other discrete fibrations can be used. (It would be hilarious if the induced functor between Kleisli categories were that exact same fibration but I only give it about 50-50.)

James Deikun (Jan 04 2023 at 08:47):

Looks like it's not. I miss out on big lols but this functor looks nicer so I'll live.

James Deikun (Jan 04 2023 at 12:43):

I guess $\overrightarrow{\mathcal{E}}_{\mathrm{cart}}$ is only discrete as a Street fibration unless you weed out the projections from the non-designated pullbacks, and there may not be a consistent way to do that? Bother. I'm still going to guess it's good enough though.

James Deikun (Jan 04 2023 at 13:14):

So the first big production: $\mathcal{E}$ as a large $T$-multicategory!

• The fibration is $\overrightarrow{\mathcal{E}}_{\mathrm{cart}}$.
• The cartesian functor $S$: on objects, $T$ acting on the arrow, on arrows, $T$ acting on the whole square (preserves pullbacks), pullbacks are preserved because the projection creates them and $T$ preserves them.
• The unit $\eta_S$: naturality squares for $\eta_T$, Cartesian because the projection creates pullbacks and $\eta_T$ is Cartesian.
• The multiplication $\mu_S$: naturality squares for $\mu_T$, same remarks.
• $\phi$: $\mathrm{id}$, this is a strict monad morphism.

I think even if I actually did this one internally with a universe it would only need to be closed under pullbacks, composition, and $T$ itself. It would have been a lot harder to think of, though!

James Deikun (Jan 04 2023 at 13:16):

I thought that one would actually be hard, maybe impossible, because $\mathcal{E}$ didn't have any big conditions on it relating it to $T$, but then I realized: $T$ lives there, how could it be more related?

James Deikun (Jan 04 2023 at 13:29):

Now that I have this, I can start working on a version of the display conjecture, since normal $T$-multicategory maps into the $T$-multicategory of $T$-algebras should be the same as arbitrary $T$-multicategory maps into the $T$-multicategory of $\mathcal{E}$. I need a couple more ingredients, though: the $T$-multicategory of pointed $\mathcal{E}$-objects, its standard projection, and the externalizing version of Leinster's $M$.

James Deikun (Jan 04 2023 at 13:57):

First of all what even are pointed $\mathcal{E}$-objects? Well, plain $\mathcal{E}$-objects are represented as an arrow into the indexing object, I guess pointing such a thing is equipping it with a section? Cartesian arrows are still just Cartesian squares since everything else is determined. Same monad can be used except now $T$ also acts on the sections. Projection is forgetting the section -- I still don't know what properties the "sides" of large external $T$-multifunctors need but if you imagine doing this with a universe it's going to be $\mathrm{el}_!$ so it's probably fine. Again it's a strict monad morphism.

James Deikun (Jan 04 2023 at 14:41):

Just for fun let's try abusing the translation in Proposition 6.2.3 to create an internal version of the multicategory of $\mathcal{E}$-objects. Start with a universe $\bold{E} \xrightarrow{\mathrm{el}} \bold{U}$. Then:

• $E_0 = \bold{U}$
• $E_1 \xrightarrow{\mathrm{cod}} \bold{U}$ is the name of $T(\mathrm{el})$, which isn't obviously guaranteed to exist since it lives over $T\bold{U}$ which is a large object.
• $T\bold{U} \xrightarrow{\mathrm{dom}} T\bold{U} = \mathrm{id}$. This object is in the image of $M$, so it's secretly just a $T$-algebra ("vertically trivial"). Interesting.
• $\mathrm{comp}$ is $\mu_{T,\bold{U}}$.
• $\mathrm{ids}$ is $\eta_{T,\bold{U}}$.

The underlying $T$-algebra here is just $t(\mathrm{id})$, the name of $T(\mathrm{el})$, which if it exists is automatically a $T$-algebra by general considerations of pullbacks.

Jacques Carette (Jan 04 2023 at 14:50):

Words of encouragement: while I understand but a tiny fraction of what you're posting in this thread, I'm an interested lurker who thinks you're poking around somewhere interesting. Much of the background material on which you're building is very near the top of my to-read list. Some of it is even on my 'to formalize' list.

James Deikun (Jan 04 2023 at 14:52):

Thank you for the kind words! Believe it or not considering the volume, it's been hard for me to keep going on this work with so little engagement, wondering if I'm just wasting everybody's time.

Jacques Carette (Jan 04 2023 at 14:54):

My guess is that there are very few people, even here, with the necessary background to follow what you're doing (myself included). So engagement will be thin. Not enough of the authors of like material are on here.

Morgan Rogers (he/him) (Jan 04 2023 at 15:40):

@James Deikun it looks like you've been working at this full time this week, but not everyone reading will be checking very often. Be patient and you'll get some comments or pointers. It will also help to regularly summarise where your up to or make explicit what questions you're tackling, since those will improve your chances of getting responses :innocent:

Mike Shulman (Jan 04 2023 at 15:42):

As I said before, I don't have the time to follow what you're doing right now, and some people who are interested may feel overwhelmed by such a high volume of posts. It sounds to me like you're investigating something potentially interesting, but rather than using Zulip as your scratch paper I would suggest working on it for a while on your own and then coming back to summarize and/or ask specific questions.

James Deikun (Jan 04 2023 at 16:17):

Fine, I'll slow down after the one I've been working on.

For the multicategory of pointed objects:

• $\dot{E}_0 = \bold{E}$. (You can extract an arrow with a section from an arrow into $\bold{E}$.)
• $\dot{E}_1 \xrightarrow{\mathrm{cod}} \bold{E}$: to evaluate this take $\mathrm{id}_{\bold{E}}$, figure out its sectioned arrow, apply $T$, and turn back into a name. The sectioned arrow is one of the projections of the pullback of $\mathrm{el}$ along itself, which "forgets one point"; the section is the "diagonal" that chooses both "points" to match. The $T$-image of this sectioned arrow seems to have a name whenever $T(\mathrm{el})$ does: pull back the name of $T(\mathrm{el})$ along $\mathrm{el}$.
• $T\bold{E} \xrightarrow{\mathrm{dom}} T\bold{E}$: this seems to be $\mathrm{id}$ again: once more it's actually an algebra?

Everything being an algebra surprises me because $\mathbb{S}\mathrm{pan}(\mathrm{Set})$ seems like an actually vertically nontrivial virtual double category and it seems like that's what the "virtual double category of quivers" should be. Am I doing something wrong here and if so what?

James Deikun (Jan 05 2023 at 18:27):

At this point I consider that I've established the display conjecture . There are a few holes to fill in that involve eye-watering diagram chases or manipulating the internal logic of an LCCC but they don't really seem in doubt. The way this works is:

• You're in an LCCC $\mathcal{E}$ with a predicative universe $\mathrm{el}_0 : \dot{U}_0 \to U_0$, and you have a Cartesian monad $T$. I don't think the universe absolutely has to be closed under $T$ but it might have to, and it's nice if it is. You might be able to get away with a mere Cartesian category as long as $T(\mathrm{el}_0)$ is exponentiable.
• Call $T$-graph or $T$-multicategory morphisms where the square involving $dom$ is a pullback Cartesian. Cartesian morphisms are closed under composition and have a factorization property thanks to the pasting lemma.
• The image of Leinster's $M$, the $T$-algebras included as vertically trivial $T$-multicategories, are precisely those which are over the terminal $T$-multicategory by a Cartesian morphism. Thanks to the above factorization property, all the morphisms among them are Cartesian, and thereby originate from $T$-algebra morphisms, making this a full subcategory.
• Cartesian $T$-multicategory morphisms are closed under strict pullback along arbitrary morphisms, which is done by pulling back the maps of objects and arrows, drawing in the T-image of the morphism-of-objects pullback, which is still a pullback, drawing in $\mathrm{dom}$ and $\mathrm{cod}$ for the corner category using the universal property of pullbacks, and noticing that thanks to pasting one of the new morphisms is Cartesian.
• You can extend your predicative universe to a Cartesian $T$-multicategory morphism $\mathrm{el} : \dot{U} \to U$ that classifies Cartesian morphisms. The morphism of objects is just the universe $\mathrm{el}_0$ you started with. $U_1$ with its projections is, in internal logic, $\mathrm{dom}: TU_0, \mathrm{cod}: U_0 \vdash T\mathrm{el}_0(\mathrm{dom}) \to \mathrm{el}_0(\mathrm{cod})$. $\dot{U}_1$ and its domain projection are obtained by pullback; its codomain projection is application.
• For each $T$-multicategory $X$ there is an equivalence of categories $T\text{-Multicat}_{U_0\text{-small}}/X_{\mathrm{cart}} \approx T\text{-Multicat}(X,U)$. I suspect, but have not yet established, that this will somehow extend to an equivalence of $T$-multicategories.
• In particular, for each $T$-algebra $A$, there is an equivalence of categories ${\mathcal{E}^T}_{U_0\text{-small}}/A \approx T\text{-Multicat}(MA,U)$ nicely generalizing the original displayed categories equivalence, which appears in the case of the free category monad on the category of quivers.
• $U$ generally has a nice claim to be a $T$-multicategorical "universe of $\mathcal{E}$-objects"; for example, in the above case it is identical to $\mathbb{S}\mathrm{pan}(\mathrm{Set})$.

(And yes, I did have the wrong monad before. The right one doesn't even externalize because the monad part of the externalization would have large algebras.)

James Deikun (Jan 07 2023 at 01:32):

Update for the day:

• Maybe I should have called Cartesian morphisms discrete opfibrations, that's what they are in $\mathrm{Cat}$.
• If the total category of your fibered category is an LCCC with a predicative universe, then ordinary $T$-multicategories are a special case of enriched ones. First you build a mini universe in the fiber $\mathcal{E}_1$ (surprisingly tricky but doable) and then you do the immediately-above "universe of $\mathcal{E}$-objects" construction in there. That gives you the right enriching category, and yes it is delooped $\mathrm{Set}$ in the case you're thinking of.
• In preparation for extending the above equivalences of categories to equivalences of $T$-multicategories I created a virtual double category of functors between any two virtual double categories $C$ and $D$. As one would expect, the objects are functors and the vertical arrows are vertical transformations but there are also proarrows and squares. In the case that $C$ is $1$ it reduces to $\mathbb{M}\mathrm{od}(D)$.

Nathanael Arkor (Jan 07 2023 at 04:02):

As one would expect, the objects are functors and the vertical arrows are vertical transformations but there are also proarrows and squares.

I'm interested to hear what the proarrows are. I thought about it a little while ago, and the definition didn't seem obvious without having composites of proarrows.

James Deikun (Jan 07 2023 at 15:10):

Well, first off, correction: it seems the construction might not work for all $C$. The problem is with composition of squares, which I clearly took for granted too much. It does still work for all vertically trivial $C$, though, which is enough for the classic display equivalence; and maybe some more cases.

Let me see how far I can explain the construction within the limitations of Zulip.

A proarrow of functors $P : F \to G$ consists of:

• for each proarrow $p : c \to c'$ in $C$, a proarrow $Pp : FX \to GX$.
• for each square $\theta : \overline{p_{(1...n)}} \xrightarrow[f]{g} p$ with a marked edge $k$, a square $P_k\theta : \overline{Fp_{(1...k-1)}}, Pp_k, \overline{Gp_{(k+1...m)}} \xrightarrow[Ff]{Gg} Pp$.
• Identity squares must be preserved by $P_1$.
• Composites of squares must be preserved in the following manner: mark any edge in the top row and every edge below it in the composition. Marked edges and squares having them are mapped through $P$, everything to the left of them (including their left edges/ends) is mapped through $F$, everything to the right of them (ditto) is mapped through $G$. These composites must be equal to what you get by mapping the composite with its marked edge through $P$.

A square $\alpha : \overline{P_{(1...n)}} \xrightarrow[\omega]{\omega'} P$ consists of, for each $\theta : \overline{p_{(1...m)}} \xrightarrow[f]{g} p$ in $C$ with $n$ strictly ordered marked edges $\overline{i_{(1..n)}}$, a cell

$$\alpha\theta : \overline{F_0p_{(1..i_1-1)}}, P_1p_{i_1}, ..., P_np_{i_n}, \overline{F_np_{(i_n+1...m)}} \xrightarrow[\omega{}f]{\omega'g} Pp$$

(break because this comment was making Zulip give up on previewing)

James Deikun (Jan 07 2023 at 15:11):

with composites being preserved thusly:

• pick any pasting diagram of squares in $C$
• mark any square in the diagram with "$\alpha$"
• mark any $n$ edges in the top of that square with "$P_1$" through "$P_n$", in left-to-right order
• for each of these marked edges, mark any edge in the top row above it with the same mark
• if at any point so far you have failed to find something to mark, ignore and try again from the top
• mark all the horizontal edges and squares between the two existing "$P_1$" marks with the same mark
• repeat for each $P_k$
• mark the bottom edge of the "$\alpha$" square, and all squares and horizontal edges below it, with "$P$"
• mark the left edge of the "$\alpha$" square and every unmarked square and vertical edge to the direct left of it with "$\omega$"
• mark the right edge of the "$\alpha$" square and every unmarked square and vertical edge to the direct right of it with "$\omega'$"
• mark every cell horizontally between a "$P_k$" and a "$P_{k+1}$" mark with "$F_k$"
• mark every cell to the left of a "$P_1$" mark and/or above an "$\omega$" mark with "$F_0$"
• mark every cell to the right of a "$P_n$" mark and/or above an "$\omega'$" mark with "$F_n$"
• mark every cell to the left of a "$P$" mark and/or below an "$\omega$" mark with "$F$"
• mark every cell to the right of a "$P$" mark and/or below an "$\omega'$" mark with "$G$"
• at this point every cell should have exactly one mark
• map each cell and its boundary marks through the corresponding functor, vertical transformation, proarrow of functors, or square of functors corresponding to its body mark to obtain a pasting diagram in $D$
• map the composite of the pasting diagram in $C$ through $\alpha$ using the marks on the boundary of the pasting diagram as the extra data, to get a cell in $D$
• this cell should be equal to the composite of the pasting diagram in $D$

It's all very straightforward locally, there's just globally a lot of stuff involved.

Composing squares (this will be much less detailed):

• start with a pasting diagram $X$ in $T\text{-Multicat}(C,D)$.
• for each marked cell in $C$, find a marked pasting diagram in $C$ where the diagram and marks are consistent jointly with the cell marking and the diagram $X$. This is the hard part, which doesn't seem to work in arbitrary $C$ but that I can do at least if $C$ is vertically trivial.
• translate the marked diagrams to plain diagrams in $D$.
• compose them to get the data of the composite square in $T\text{-Multicat}(C,D)$.

Nathanael Arkor (Jan 07 2023 at 17:15):

Thanks for explaining! So, if I understand correctly, for each cell $\theta$ (left), you have a family of 2-cells (right), of the following form (quiver)?

image.png

Nathanael Arkor (Jan 07 2023 at 17:17):

I'd like to think about it a little more, but it seems reasonable on first glance.

James Deikun (Jan 07 2023 at 17:49):

That looks right.

James Deikun (Jan 07 2023 at 18:01):

In the case of $1$:

• the two squares in the definition of bimodule fall out of the single binary square in $1$, with left/right marking.
• the identity laws come from preservation of identities and the fact that there's no square in $1$ parallel to the identity.
• the left/right multiplication laws come from the fact there's only one trinary square in $1$ to have a marked left/right.
• the exchange law comes from the fact that there's only one trinary square in $1$ to have a marked middle.

James Deikun (Jan 09 2023 at 02:40):

Update:

• I made a vertical slice virtual double category over an object with unit, or alternately, over a monoid. Unlike the functor category, this needs a unit/monoid, but unlike the functor category, it doesn't have any weird problems with square composition when it's not over some special kind of object. Looks like the equivalence holds at the full VDC level for the classic displayed category construction, but the equivalence and/or $\mathrm{VirtDblCat}$ itself as a VDC must break down outside the vertically trivial world.
• I've tried making a $T$-multicategory of $T$-functors internally, but it ends up with the wrong cell structure. This really is a fundamental problem of using internal logic in $\mathcal{E}$ and of the setting as such; I want $T$-functors to be dots, but $\mathcal{E}$-logic has no idea what a "dot" is, only a "point"--in quivers, that's a dot with a loop on it, so I get dots in the object of $T$-functors being ordinary functors on the dots and vertical arrows, with no information about proarrows and squares. I'm trying to augment the setting and logic with a flat modality but I'm not sure if that will help.
• That notwithstanding, mad props to Mike Shulman for encouraging me to work in this (Burroni/Leinster) setting as it's been very productive and clarifying as to exactly what structure I actually need for things, compared to working with presheaves.

James Deikun (Jan 09 2023 at 16:42):

I'm trying to decide if an exotic definition of functors between virtual double categories is equivalent to the normal one. It's giving me headaches and I would greatly appreciate any help anybody can give. [I got over the headaches and this definition, but it was very helpful thinking about it.]

The conventional definition: A functor F between C and D consists of:

• For each object X of C, an object FX of D.
• For each arrow f : X -> X' of C, an arrow Ff : FX -> FY of D.
• For each proarrow P : X +> X' of C, a proarrow P : FX +> FX' of D.
• For each square $\theta : \overline{P_{(1...n)}} \xrightarrow[f]{f'} P$ of C, a square $F\theta : \overline{FP_{(1...n)}} \xrightarrow[Ff]{Ff'} FP$ of D.
• Identities and composites of arrows and squares must be preserved by F.

The exotic definition: Let $\mathrm{Pro}(C)$ be the quiver of objects and proarrows of C and $\mathrm{Sq}(C)$ the quiver of arrows and squares of C. A functor F between C and D consists of:

• For each quiver Q and image q of Q in $\mathrm{Pro}(C)$, an image Fq of Q in $\mathrm{Pro}(D)$.
• For each quiver Q and pure-degeneracy map $\phi$ of a quiver Q' into Q, equipped with a "section" $\sigma : Q \to \mathrm{Paths}(Q')$:
  • For each image q of Q in $\mathrm{Sq}(C)$ equipped with an image q' of Q' in $\mathrm{Pro}(C)$ such that $\mathrm{dom}_C \circ q = \mathrm{Paths}(q') \circ \sigma$
  • an image $F_{\phi,\sigma}q$ of q in $\mathrm{Sq}(D)$
  • such that $\mathrm{dom}_D \circ Fq = \mathrm{Paths}(Fq') \circ \sigma$
  • and $\mathrm{cod}_D \circ q = F(\mathrm{cod}_C \circ q)$.
• Such that for all q, $F_{\mathrm{id},\eta_{\mathrm{Paths}}}(\mathrm{ids}_C \circ q) = \mathrm{ids}_D \circ q$
• and for all [all the variables], $F_{\phi \circ \phi',\mu_{\mathrm{Paths}} \circ \mathrm{Paths}(\sigma') \circ \sigma}(\mathrm{comp}_C(q,q')) = \mathrm{comp}_D(F_{\phi,\sigma}q, F_{\phi',\sigma'}q')$.

I'm mostly concerned that there might be too much freedom regarding how quivers of different shapes get mapped relative to each other and there might need to be an extra law or two to restrain that.

James Deikun (Jan 10 2023 at 20:49):

•, Δ, and the standard multicategories

In order to talk about the objects of a T-multicategory, you need tools a little more sensitive than the global point $1$. The first of these tools is the dot, $\bullet$. This is a subterminal object of $\mathcal{E}$ which induces an idempotent modality $\flat$ via Cartesian product. This "flat" modality forgets everything but the "objects" or "dots" in an $\mathcal{E}$-object.

The second tool is the degeneracy monad, $\Delta$. This serves as a non-idempotent modality that builds up where "flat" tears down. Semantically, it serves to add "degenerate cells" that reflect lower-dimensional things, including objects, into the higher dimensions of $\mathcal{E}$. In good cases, at least, $\Delta$ is stable, strongly Cartesian, and left adjoint, but which of these nice attributes are essential remains to be determined. $\Delta$ must obey the law $\Delta\bullet = 1$.

The third tool is the virtual distributive law $\mathbb{S}$ (of $T$ over $\Delta$). It serves as compatibility data between $\Delta$ and $T$, by deciding when a T-term with some degenerate arguments is actually a degenerate version of another T-term. In the case when T is the free category monad, it decides when a "slow path" that can pause at dots traverses the same edges as a "fast path", or when it doesn't traverse any "real" edges at all.

$\mathbb{S}$ is a functor from $\mathcal{E}$ to itself, with two natural projections, $\mathrm{dom}_{\mathbb{S}}$ to $T\Delta$ and $\mathrm{cod}_{\mathbb{S}}$ to $\Delta{}T$. It has four structure morphisms corresponding to the four laws of a distributive law: $u : \Delta \to \mathbb{S}$ satisfies $\mathrm{dom} \circ u = \eta_T\Delta$ and $\mathrm{cod} \circ u = \Delta{}\eta_T$ while $m : T\mathbb{S} \times_{T\Delta{}T} \mathbb{S}T \to \mathbb{S}$ follows $\mathrm{dom} \circ m = \mu_T\Delta \circ \mathrm{dom}$ and $\mathrm{cod} \circ m = \Delta\mu_T \circ \mathrm{cod}$. $v$ and $n$ are symmetric compatibility laws with $\Delta$.

From $\mathbb{S}$ you can construct the standard multicategory functor 𝕂. It raises $\Delta$ to create T-multicategories, equipping the $\Delta$-image of each object with an object of morphisms and a compatible T-multicategory structure. Having a parameterized T-algebra structure on $\Delta$ turns out to be too much to ask, but a T-multicategory stuff is just right!

Now, 𝕂 may seem like a lot of data, but like $\Delta$ it usually folds out from a little data, because it is required to (1) be a left adjoint (its right adjoint might be called $\mathbb{M}\mathrm{od}_0$) and (2) take $\bullet$ to $1$. This means you really need to just specify it for your basic shapes other than dots in a consistent way and the full thing will unfold. In the case of $T$ being the free category monad, $\bullet$ is the one-dot quiver, $1$ is the dot-with-a-loop quiver, and $\Delta$ is the "put a loop on every dot" monad. 𝕂 is entirely determined by its value on the walking edge; this is a vertically trivial $T$-multicategory unfolded from the algebra that maps every path to the unique edge with the same source and target. The other 𝕂 values are "subtrivial"--there are never two squares for a given domain but there may be none. There is a square for a domain when the path involved only traversed at most one nondegenerate edge, and the codomain is either that edge or the degenerate edge it spun on. (Now if only I could figure out how to create all of $\mathbb{S}$ that easily!)

With the aid of these tools, it's possible to generalize the definitions of "functor" and "natural transformation" of $T$-multicategories to include not only the "objects" we usually think of them as denoting but a bunch of higher shapes, setting the stage for raising the display equivalence for $T$-algebras from an equivalence of categories to an equivalence of $T$-multicategories.

James Deikun (Jan 11 2023 at 19:07):

Update:

• I seem to have missed an important structural morphism of $\mathbb{S}$ that doesn't have an analogue for a pseudo-distributive law, but it is what determines the direction and itself kinda distributes on a micro level, so call it $d : \mathbb{S}(\mathrm{cod} X)\cdot{}T\Delta{}X \to \Delta{}TX\cdot\mathbb{S}(\mathrm{dom} X)$, where $\cdot$ is composition of plain spans and $X$ is a span.
• With this it is possible to lift $\Delta$ to a (pseudo?)monad on $T\text{-Multicat}$, given by $\mathbb{\Delta} = (\Delta - \circ \mathbb{S}(\mathrm{dom} -))$ with right (pseudo?)adjoint $\mathbb{M}\mathrm{od}$. In the Usual Setting, this adds new units to the virtual double category along with a bunch of new cells and equations to make them work. Unlike $\mathbb{M}\mathrm{od}$ I don't think it gets along nicely with existing restrictions.
• And with that I'm finally close to an answer to "what are units?": a $T$-multicategory with units is a $\mathbb{\Delta}$-algebra or equivalently a $\mathbb{M}\mathrm{od}$-coalgebra.
• I can't believe there's no blackboard bold delta; hopefully you can tell which is which.

James Deikun (Jan 13 2023 at 23:48):

Update:

• Talked with @Christian Williams about bending shapes in a fibrant triple category and got some good intuitions about "restrictions" outside the paradigm case. They seem to involve universal fillers for "cylinders" with one end open and identity-derived cells on the sides.
• Related to this, rather than ordinary categories not having a notion of units and restrictions, or having a trivial notion, they have a notion that is automatically fulfilled. Units are given by identities, and restrictions of an object along its nothing boundary are given by the object itself with identity as the Cartesian cell.
• To get a less algebraic notion of "having units", probably going to replace "being a $\Delta$-algebra" with "being a cofibrant object for a model structure right transferred from the EM category of Delta along the cofree functor".
• And the fibrant objects will "have restrictions", hopefully.
• Related to this, trying to figure out what a model structure on $\mathrm{Cat}$ generated by cofibrations the inclusions $0 \to 1, 1 \amalg 1 \to \mathbb{2}$ and acyclic cofibrations the inclusion $1 \to \mathbb{2}$ as the target of the morphism is like.

James Deikun (Jan 19 2023 at 01:06):

Haven't had as much time to work on this lately since I have a new job.

• Backed off from geometrizing units and restrictions for now as the tools for handling geometric structures with universal properties generically just don't seem to be there. Hoping to still come up with something eventually but it's no longer a priority.
• Figured out even though it's unreasonable for $T$ and the degeneracies monad to have a distributive law in the right direction, the degeneracies comonad is another story. Need to figure out if $\mathbb{S}$ can be recovered from this.
• Have a pretty good hypothesis as to what "restrictions" are like at least when there are no inherited ones. There should be a restrictions monad where the object of objects classifies partial maps into the object of morphisms of the underlying internal category such that the taking the codomain includes it into an associated total map into objects. Basically an object of this thing is a cell with a bunch of unary morphism-cells bristling out the back of it. If there's one that covers the whole cell then you get something isomorphic to the source of that, if the cell is completely bare then you just get the underlying cell, but in between you get a situation in between. Morphisms have an underlying morphism-cell, their own bristles on the "back" and in "front" you have "slots" that are made by factoring out unary morphisms from its facets. Morphisms with identity as an underlying morphism are Cartesian. I'm probably not explaining this well.
• Want to figure out what the restrictions monad above looks like formally and whether it preserves freeness, so I can find a place to slot in inherited restrictions.
• Slightly far out idea: restrictions are basically a categorification of being "normalized" a la Cruttwell and Shulman (Def. 8.2)

Morgan Rogers (he/him) (Jan 19 2023 at 18:47):

Congratulations on the new job!

James Deikun (Jan 25 2023 at 03:07):

• Figured out that "new" restrictions are basically "sub-unary pullbacks" in a T-multicategory and found a formulation of that which is not very nice what with all the nested quantifiers and stuff but seems to at least be correct. Still don't have a way to inherit the notion of restrictions from T-algebras, or even express that.
• Found a general approach to a prime construction for $\Delta$ and $\mathbb{S}$. $\Delta'X$ is $\Delta(X+\mathrm{Id}_{X_0}) \cdot \mathbb{S}X_0$, and $\mathbb{S}'$ comes from putting $T'\Delta'X$ and $\Delta'T'X$ in a common normal form of alternating layers of degenerate and "real" cells and pulling back the normalizations. There are still a lot of gaps like proving that $\Delta'$ is still a Cartesian monad (it seems to need some assumptions on some of the structural morphisms of $\mathbb{S}$ being Cartesian, and possibly $\mathbb{S}$ itself preserving some limits) or still has a right adjoint or that $\mathbb{S}'$ is still a virtual distributive law or still fulfills these new Cartesianness assumptions. The diagrams involved in those proofs are nothing short of terrifying so hoping another sort of general abstract nonsense will work.

Matteo Capucci (he/him) (Jan 25 2023 at 14:42):

@James Deikun may I suggest you move this thread to #practice: our work?

James Deikun (Jan 25 2023 at 16:18):

Maybe that would be a good idea. An even better idea might be to move it leaving the first few messages. I don't seem to have rights to do either one though.

Matteo Capucci (he/him) (Jan 25 2023 at 16:39):

If you tell me which message to cut off at I will do it

James Deikun (Jan 26 2023 at 00:04):

I was answering direct questions a bit longer than I thought, probably https://categorytheory.zulipchat.com/#narrow/stream/229136-theory.3A-category-theory/topic/Conjectures.20on.20generalized.20equipments/near/318354499 would be a good place to start putting it in #practice: our work since that is where I started doing updates.

James Deikun (Jan 09 2024 at 19:48):

The Equipment of Equipments Seems to be Vertically Cartesian Closed

In marked contrast to the virtual double category of virtual double categories, the virtual equipment of virtual equipments seems to have a unit-respecting right adjoint to the vertically-Cartesian product functor. This means that any shape $\mathbb{I}$ of diagram in a given equipment $\mathbb{X}$ forms another equipment, $[\mathbb{I},\mathbb{X}]$! Here's how it works:

James Deikun (Jan 09 2024 at 19:50):

The vertical Cartesian product of two equipments, $X$ and $Y$, is an equipment $X \times Y$ such that (normal, restriction-preserving) virtual functors into it represent a pair of virtual functors into $X$ and $Y$. It's about the simplest thing imaginable:

• Objects are an object of $X$ and an object of $Y$
• Arrows are an arrow of $X$ and an arrow of $Y$
• Proarrows are a proarrow of $X$ and a proarrow of $Y$
• Cells are a cell of $X$ and a cell of $Y$ of the same shape
• Composites and units and restrictions are componentwise; nothing new needs to be generated.

The unit $𝟙$ of the vertical Cartesian product is the vertical terminal object; it has exactly one thing of each shape and "all equations are true".

James Deikun (Jan 09 2024 at 20:03):

Everything so far is just inherited from virtual double categories; all the magic comes from the definition of an equipment itself. Let $S$ be some shape in an equipment (a dot, arrow, proarrow, or cell) and $\mathbb{S}$ be the equipment freely generated from a virtual double category containing a single $S$-shape. (In the case of a dot, you get $𝟙$; this may be considered a good sign.)

Now we can define $[\mathbb{I},\mathbb{X}]$. An $S$-shape in $[\mathbb{I},\mathbb{X}]$ is simply a (normal, restriction-preserving) virtual functor from $\mathbb{I} \times \mathbb{S}$ to $\mathbb{X}$. That's it! This definition "instantly" gives us virtual equipments of relative monads and many other things.

James Deikun (Jan 09 2024 at 20:11):

The "fun" part is unfolding what these Cartesian products look like in particular cases. For example, a proarrow of proarrows unfolds into a "butterfly" shape:

$$\begin{CD} A @>{P}>> B @>{G}>> D \\ @| @. @| \\ A @>{R}>> @>>> D \\ @| @. @| \\ A @>>{F}> B @>>{Q}> D \end{CD}$$

where the bottom cell points up.

James Deikun (Jan 09 2024 at 20:15):

An "arrow of proarrows" looks pretty involved at first because of all the restrictions, but it turns out to all be generated by a single square $\phi$:

$$\begin{CD} A @>{P}>> B \\ @V{f}VV @VV{g}V \\ C @>>{Q}> B \\ \end{CD}$$

James Deikun (Jan 09 2024 at 20:17):

Where this approach really proves its worth is in figuring out the more obscure situations, like a 2-cell of 3-cells, or an arrow of maps out of restrictions, which are too complicated to draw with AMSCD sadly (?).

James Deikun (Jan 09 2024 at 20:20):

I'm currently trying to determine exactly how the definition of equipment does this "magic", which is very similar to the "magic of degeneracies" in simplicial sets, so I can write up something a little more formal and maybe generalize it to generalized equipments (see above).

Nathanael Arkor (Jan 09 2024 at 21:17):

Do you require $\mathbb I$ to be an equipment, or is it enough to be a normal virtual double category (that is, admitting loose identities)?

Nathanael Arkor (Jan 09 2024 at 21:18):

(The normality assumption is necessary to define a diagonal functor, so this seems necessary.)

Nathanael Arkor (Jan 09 2024 at 21:29):

It would be nice to have this written out, because I think an appropriate definition of "$\mathbb X$ admits $\mathbb I$-indexed colimits" for a virtual equipment $\mathbb X$ is for the diagonal $\mathbb X \to [\mathbb I, \mathbb X]$ to have a normal left adjoint, and there are several motivating examples. For instance, taking $\mathbb I$ to be the "free-standing loose-monad", I believe that asking for $\mathbb X$ to admit $\mathbb I$-indexed colimits is close to asking for it to be exact in the sense of Schultz (with one caveat that can be addressed by asking for the unit of the adjunction to be cartesian).

Nathanael Arkor (Jan 09 2024 at 21:34):

(Of course, standard double categorical colimits like cotabulators/collages are also examples.)

James Deikun (Jan 09 2024 at 23:46):

AFAICT restrictions aren't doing any work until they're brought in explicitly, so probably all this works for normal VDCs as well. It's remarkable how well restrictions cooperate and stay out of the way, though.

James Deikun (Jan 10 2024 at 16:45):

Just a random note that, while investigating the concept of monadicity for equipments, I tried equipmentifying the explicit presentation of the EM category by hand, hoping for some insight, and ended up with exactly $\mathbb{M}\text{od}(\mathbb{H}\bold{\text{-Kl}}(\mathbb{X}^\mathrm{op},T^\mathrm{op})^\mathrm{op})$ ...

James Deikun (Jan 10 2024 at 17:45):

It actually was pretty insightful, since it seems like you can use the monad data to turn the modules around so that it doesn't seem to much matter which direction of arrows you picked ...

James Deikun (Jan 10 2024 at 17:53):

And it seems like an equipment of actual algebras and an equipment of nice presentations of algebras are inches apart in this environment instead of miles.

James Deikun (Jan 10 2024 at 20:35):

The Diagonal Fibration of a Virtual Equipment

If you have a virtual equipment $\mathbb{X}$ (and this time it really does have to be an equipment) you can get a lot more 1-categorical data out of it than merely its vertical category. Consider the following functor $d_\mathbb{X} : D(\mathbb{X}) \to V(\mathbb{X})$, considered as a "category over $V(\mathbb{X})$":

• Objects over $X : V(\mathbb{X})$ are proarrows in $\mathbb{X}(X,X)$,
• Arrows over $f : X \to Y$ are square cells framed by two copies of $f$,
• Cartesian squares of the right shape in $\mathbb{X}$, which always exist, become Cartesian arrows,
• Squares exhibiting double corestrictions along $f$, if they exist, become opCartesian arrows.

James Deikun (Jan 10 2024 at 21:02):

Now, this may seem rather plain, it's just a fibration after all. But wait! It's not just a plain fibration, it's a fibration in plain multicategories. How does this work? Each fiber $d_{\mathbb{X},X}$ has the structure of a plain multicategory, where the multi-arrows are all the cells in $\mathbb{X}$ framed by the vertical identity on $X$ and having target and all sources in $\mathbb{X}(X,X)$. The underlying categories are just the fibers as defined above. The pullback functors $f^*$ extend to transport this multicategory structure using composition and Cartesian factoring of cells.

So far all this works for any equipment, but if $\mathbb{X}$ is a pseudo equipment rather than virtual, and $V(\mathbb{X})$ is Cartesian monoidal, then Theorem 12.8 of Shulman's "Framed Bicategories and Monoidal Fibrations" should actually give a monoidal fibration out of this.

James Deikun (Jan 10 2024 at 21:17):

"But what is it good for?" you ask. Well, one important role is lowering monads on equipments back down to 1-category land without losing too much information. If you take the diagonal fibration of the horizontal Kleisli category of a monad on an equipment, you still have all the pieces you need to construct the vertical category of $\mathbb{K}\text{Mod}(\mathbb{X},T)$. This may seem like a bizarre thing to do, but it's really helpful for comparing Burroni-Leinster generalized multicategories to Cruttwell-Shulman ones and teasing out the hidden higher-dimensional features of the former. For example, the category of quivers fibered over their sets of dots is exactly the diagonal fibration of $\mathbb{S}\text{pan}(\bold{Set})$.

James Deikun (Jan 10 2024 at 21:35):

(In fact, in general the category of "$T$-graphs" is the total category of the diagonal fibration of the equipment of "$T$-spans", and the diagonal fibration itself gives the structure you need to reconstruct the "$T$-multicategory on a $T$-graph" monad.)

Nathanael Arkor (Jan 11 2024 at 08:19):

James Deikun said:

Just a random note that, while investigating the concept of monadicity for equipments, I tried equipmentifying the explicit presentation of the EM category by hand, hoping for some insight, and ended up with exactly $\mathbb{M}\text{od}(\mathbb{H}\bold{\text{-Kl}}(\mathbb{X}^\mathrm{op},T^\mathrm{op})^\mathrm{op})$ ...

It may be worth noting that @Roald Koudenburg has studied augmented virtual double categories of algebras in §6 of the preprint A double-dimensional approach to formal category theory. Is this the same kind of structure you were looking at?

Nathanael Arkor (Jan 11 2024 at 08:20):

But this identification seems very curious... I'd be interested to see the details.

Nathanael Arkor (Jan 11 2024 at 08:39):

James Deikun said:

If you have a virtual equipment $\mathbb{X}$ (and this time it really does have to be an equipment) you can get a lot more 1-categorical data out of it than merely its vertical category. Consider the following functor $d_\mathbb{X} : D(\mathbb{X}) \to V(\mathbb{X})$, considered as a "category over $V(\mathbb{X})$":

In the setting of pseudo double categories, this functor $d_\mathbb{X}$ looks related to the hom functor Paré describes in §2.1 of Yoneda theory for double categories, except that he considers a two-sided construction that captures arbitrary loose-cells $X \not\rightarrow Y$, rather than just the endomorphisms. The same kind of construction should work for virtual double categories. Perhaps this is a useful perspective also?

Nathanael Arkor (Jan 11 2024 at 08:42):

(I was thinking about this at some point because I wanted a Yoneda embedding for virtual double categories, but I ran into issues because there didn't seem to be a functor virtual double category construction. But perhaps if one restricts to (virtual) equipments it will work out after all.)

James Deikun (Jan 11 2024 at 10:22):

Nathanael Arkor said:

But this identification seems very curious... I'd be interested to see the details.

For objects: the base proarrow of the monoid, $X : TA \to A$ becomes the algebra arrow. The multiplication and unit of the monoid become constraints:

$$\begin{CD} @>{TX}>> @>X>> @. @= \\ @V{\mu}VV x_\mu @. @| \phantom{blah blah} @V{\eta}VV x_\eta @| \\ @>>X> @>>> @. @>>X> \end{CD}$$

matching the equations $Tx \circ x = \mu \circ x$ and $id = x \circ \eta$. The monoid laws become the necessary coherences.

James Deikun (Jan 11 2024 at 10:29):

For arrows: the arrow part becomes the algebra morphism $f$ itself, the square becomes a constraint:

$$\begin{CD} @>X>> \\ @V{Tf}VV f_T @VVfV \\ @>>Y> \end{CD}$$

matching the equation $x \circ f = Tf \circ y$, and the compatibilities become coherences.

James Deikun (Jan 11 2024 at 10:53):

For proarrows: here the guidance from the EM category was a bit less clear, but: the base proarrow of the bimodule becomes the algebra bimodule $p$ itself, the actions become a butterfly:

$$\begin{CD} @>{Tp}>> @>Y>> \\ @V{\mu}VV \Downarrow @. @| \\ @>p>> @>>> \\ @A{\mu}AA \Uparrow @. @| \\ @>>{TX}> @>>p> \end{CD}$$

These match the equations $Tp \circ b = \mu \circ p$ and $Ta \circ p = \mu \circ p$ that make the bimodule like an algebra, and the "meta equation" $Tp \circ b = Ta \circ p$ that makes it almost like a morphism. The coherences of the action become, well, coherences.

I'm not going to try to draw out what happens with cells.

James Deikun (Jan 11 2024 at 11:08):

The horizontal Kleisli category includes in as "free modules" where all the cell parts are made from cartesian and opcartesian cells. Here, as in the inclusion of the underlying equipment into the horizontal Kleisli category, we rely heavily on the existence of units and restrictions, this doesn't work at all with simply a virtual double category. The really interesting part is how proarrows include: the "free bimodule" on a horizontal Kleisli arrow $p : A \; ⇸ \; TB$ is $Tp(\mu,\eta) : TTA \; ⇸ \; TB$. This is how proarrows "turn around".

James Deikun (Jan 11 2024 at 11:16):

There's stuff that's still mysterious about this correspondence, like: why doesn't there seem to be normalization? I think probably there is normalization, and it's probably because the unit constraint for an algebra just happens to be cartesian in the diagram equipment where it originally lives, and this has to be preserved by maps of equipments. This would then complete an equivalence between $\mathbb{K}\text{Mod}(\mathbb{X},T)$ and this category; both categories have normal collapses for normalized monoids, so you could just turn around all the free stuff using the above free construction, and get the rest of the category by collapsing the standard presentations of the free stuff.

James Deikun (Jan 11 2024 at 11:27):

Nathanael Arkor said:

James Deikun said:

Just a random note that, while investigating the concept of monadicity for equipments, I tried equipmentifying the explicit presentation of the EM category by hand, hoping for some insight, and ended up with exactly $\mathbb{M}\text{od}(\mathbb{H}\bold{\text{-Kl}}(\mathbb{X}^\mathrm{op},T^\mathrm{op})^\mathrm{op})$ ...

It may be worth noting that Roald Koudenburg has studied augmented virtual double categories of algebras in §6 of the preprint A double-dimensional approach to formal category theory. Is this the same kind of structure you were looking at?