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.
Hello! I realized I took something for granted in my first read-through of CS09, but I'm having trouble constructing it.
In a Virtual Double Category with units, given a vertical How does one induce ? (see image) Capture.PNG
Thanks!
There is indeed no explicit definition of in the paper (or so it seems after a superficial ctrl-F)! Strange. Isn't it likely that one gets with a factorization along a cartesian cell, instead than just from units?
I guess that's possible, but it seems like several of the propositions in chapter 5/6 rely on it's construction, but only assume opcartesian cells (and sometimes only units). e.g. T5.2, P5.14, and P6.1
I assume it's not included because it's so glaringly obvious.
There is, however, an analog I tried to follow:
The monoidal identity in the former case comes from the null list in the free monoid, where-as the analog in virtual double categories would be the empty path in the free category... but I don't yet know how to parse this info into a
I don't have an answer; my suggestion was motivated by the fact that must have a universal property of some sort. Since (e.g. in the proarrow equipment of profunctors of small categories) is the cell that represents the action of a functor on morphisms, and this is a Kan extension on its own right...
I don't remember if this is legitimate (I always confused vdcs and augmented vdcs...) but perhaps it works?
I used opcartesianity of the unit of , and a "whiskering" with .
is induced by the universal property of applied to the composite of the defining universal cell of with . Possibly we neglected to define it explicitly.
Thanks! So this is what fosco said... this is also what I "took for granted" in my first reading. However, f is not a cell it is just a vertical morphism...
how do we "whisker" vertical cells with vertical morphisms in a VDC?
(I assumed this whiskering required apriori)
ah, from the direct axioms of a VDC it is not so clear that one can compose with "null length cells" or just vertical morphisms. But this is actually clear from the fc-multicategory perspective.
Sorry for the dumb Q, but thanks for the help!
It's not dumb; I agree we weren't as clear about these points as we could have been.
The paper is very insightful, IMO you've written something that deserves a lot attention.
@Noah Chrein , I would be interested in knowing why you're studying vdcs :-) I was a fan before it was cool (...is it cool now?), and I still hope I can share my passion with more people :grinning:
@fosco yes I assume it became cool this past semester, or at least that's when I learned it from the JHU Cat seminar.
I have a toy model for ontology that requires a formal notion of composition that behaves a lot like Prof / Span. VDCs provide notational convenience in this setting, but I'm also using them to try to understand which ontologies behave like categories via the existence of a yoneda-esq structure (and I call these "yoneda ontologies").
Actually it was your yosegi box paper that originally let me to Shulman/Cruttwell :)
Oh, yes, now I remember, we've had a conversation about that! What is an ontology again?
Broadly speaking its just an "expressive collection of data". It's like when you work with a new class of objects and you don't know it's structure, so you originally call it a "set" and then find it's morphisms or whatever, so you start calling it a "category" and then you realize it has a topology, higher coherance data, bells and whistles, etc. so you call it progressively more complicated names.
"Ontology" is just a word you can use to mean "I don't exactly know what structure this collection has, but I will keep upgrading it as I learn". Instead of claiming immediately that some collection is, ie, a category, you can call it an ontology to signal that it likely has more layers of expressive data.
The main point of the theory (of categories or other "categorical" forms of ontologies) seems to be how one determines objects from the ambient ontological data. One example is the yoneda embedding for categories, so I'm trying to understand this intuition through yoneda-ish formal reasoning. Seems like VDCs are (almost) expressive enough of a setting to formalize all this.