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.
Christian Williams (May 09 2022 at 17:28):Hello, I'm Christian. I'm writing my thesis with John Baez at UC Riverside. It's called "Logic in Color", and it's both a language and a story of category theory. The material is still being developed, but I'd like to begin sharing the idea here.
Christian Williams (May 09 2022 at 17:29):Here's a proposal I submitted to give a talk at ACT 2022: Logic-in-Color-Williams-ACT2022.pdf.
Christian Williams (May 09 2022 at 17:35):Last summer, I was staying at the Topos Institute. It was a great time with great people. But I was between projects, and I was not sure what I wanted to do for my thesis. I liked the applications that I had explored in grad school, but I wanted to focus on a passion and a path forward beyond the PhD.
Christian Williams (May 09 2022 at 17:35):One night David Jaz Myers was showing me string diagrams for equipments, showing some examples of how powerful they are, how they can make ideas simple and clear. I became very interested, and I realized that what I really care about is education.
Christian Williams (May 09 2022 at 17:39):So, I started thinking about how one might use string diagrams to teach category theory. But the question was: if I want to show students the full language of colors, strings, and beads, where can we begin? How can they understand a 2-category if they don't already know categories?
Christian Williams (May 09 2022 at 17:40):The answer, I found, is Rel: sets and relations and implications.
Christian Williams (May 09 2022 at 17:42):Colors are sets, strings are relations, and beads are implications. bead.png
Christian Williams (May 09 2022 at 17:45):The more I thought about it, I realized this was a very natural setting to begin learning category theory. What I was most excited about is the aspect of beginning in two dimensions, rather than having to climb up some big ladder of abstraction.
Christian Williams (May 09 2022 at 17:49):But soon I also realized that Rel was great for another reason: it is logic. Just plain old logic. What's category theory? Who knows. You can tell anyone (with no math background at all) "hey, here's a visual language for logic, check it out." From quite a few experiences now, everyday people enjoy it and understand it.
Christian Williams (May 09 2022 at 17:52):So then it began to sink in that there is a story here, using string diagrams to teach category theory as logic. That's what I'm doing.
Christian Williams (May 09 2022 at 17:53):The proposal above gives a brief outline of a three-part curriculum.
Christian Williams (May 09 2022 at 17:56):I am happy to discuss anything. I'm not yet a very productive writer, so the thesis is coming along slowly. But I gave a seminar last term for grad students, so I have some (rough) notes from that. (I'm also teaching logic to undergrads this summer, so I'm excited to try out some of these ideas.)
Christian Williams (May 09 2022 at 17:57):Several people in our community have reached out expressing interest in this stuff, and that's really encouraging.
Christian Williams (May 09 2022 at 17:58):So even though I don't yet have much polished material to show, I think it's time to start talking about it any way.
Christian Williams (May 09 2022 at 18:08):Please feel free to share any thoughts or questions, any time; I'll try to be responsive. Thanks!
John Baez (May 09 2022 at 19:00):Please ask Christian questions!
John Baez (May 09 2022 at 19:00):I do it every week. I think his ideas are really exciting.
Franklin Pezzuti Dyer (May 09 2022 at 19:06):This is really neat! So will your thesis culminate in a lesson plan/curriculum? Or will you have a chance to actually test it out on some (young) students?
Robin Piedeleu (May 09 2022 at 19:16):This looks cool! I struggled with the general form of inferences in your ACT submission a bit. Would you mind explaining a bit more how I should read there?
Christian Williams (May 09 2022 at 19:34):Thanks! The thesis will be primarily theoretical research, but the first half will develop "category theory as logic" using string diagrams.
In general, it's about interpreting fibrant double categories (equipments) as logical systems. The main goal is to formalize the (higher) coend calculus of FDC, the triple category of fibrant double categories.
But I hope to find time this year to develop lessons, especially because I get to teach logic this summer at UCR. And once I graduate, developing this education program will be my life.
Christian Williams (May 09 2022 at 19:38):Yes, sorry I was very terse in order to fit into two pages. That inference could be an implication ; more generally it is a transformation of (enriched) profunctors, so is a (generalized) element of and is a component of the transformation applied to .
Tom Hirschowitz (May 09 2022 at 20:11):Christian Williams said:
But soon I also realized that Rel was great for another reason: it is logic. Just plain old logic. What's category theory? Who knows. You can tell anyone (with no math background at all) "hey, here's a visual language for logic, check it out." From quite a few experiences now, everyday people enjoy it and understand it.
Indeed, Rel is one of the best known models of linear logic, although a famously inconsistent one, where and and or, true and false, etc, agree. Is this the sense in which you're saying that Rel "is" logic, or do you have something else in mind?
Christian Williams (May 09 2022 at 20:58):Oh, I meant "plain old logic" as in the classical predicate logic of sets. I don't yet know enough about linear logic; what would you recommend reading about Rel as a model?
Christian Williams (May 09 2022 at 21:06):When you say that "and / or agree", it sounds like you are talking about a different view of Rel... are you only using one of the monoidal structures? I'm talking about Rel as a double category with two monoidal structures, sum and product of sets. In the relation direction, they are biproducts and compact closed, respectively; in the function direction, they are cocartesian and cartesian closed.
Valeria de Paiva (May 09 2022 at 21:48):hi @Christian Williams , like @Tom Hirschowitz I thought you meant the traditional category Rel, which has biproducts, so conjunction and disjunction are modelled by the same structure(which is the same as the internal hom, as the category is compact closed). I would like to know the references for modelling type theory with double categories, as I haven't seen it, yet. thanks!
John Baez (May 09 2022 at 21:49):I hope this reference will be Christian's thesis. :upside_down:
Christian Williams (May 09 2022 at 21:58):Okay, yes well above you can find that I am talking about double categories as logical systems. I do not know of any reference; I've been surprised to see that this has not yet been explored, though it is simple:
types objects
terms arrows ("tight" or vertical morphisms)
judgements proarrows ("loose" or horizontal morphisms)
inferences squares (2-morphisms)
Christian Williams (May 09 2022 at 21:59):A square can be drawn both syntactically and pictorially. Here they are overlaid: Inference.png
Christian Williams (May 09 2022 at 21:59):In Rel, this is the implication .
Christian Williams (May 09 2022 at 22:07):I've become convinced that logic is naturally modelled in two dimensions. It reflects the way we think about the world: we determine things by type (dimension 0), we connect types by judgement (dimension 1), and we transform judgements by inference (dimension 2).
Mike Shulman (May 10 2022 at 03:32):One extant type theory for proarrow equipments (which are equivalent to a kind of double category), albeit only in the posetal case, was used by Dan Licata and Max New to represent gradual typing.
Nicolas Blanco (May 10 2022 at 06:54):This work looks exciting! If I find time between two sessions of thesis writing I will try to think of questions.
Tom Hirschowitz (May 10 2022 at 07:37):Christian Williams said:
Oh, I meant "plain old logic" as in the classical predicate logic of sets. I don't yet know enough about linear logic; what would you recommend reading about Rel as a model?
There are some elements on the linear logic wiki, and an "enriched" description in weighted relational models of typed lambda-calculi. Maybe @Damiano Mazza or @Flavien Breuvart would know of easier material.
So, @Christian Williams, could you maybe explain how the usual, syntactic account of logic forms a double category? Or perhaps sketch how the double category structure is related to the usual rules of logic?
Peter Arndt (May 10 2022 at 09:20):Yes, I would also be interested in seeing "plain old logic" here - I didn't quite get it yet.
Jon Sterling (May 10 2022 at 10:26):Christian Williams said:
Okay, yes well above you can find that I am talking about double categories as logical systems. I do not know of any reference; I've been surprised to see that this has not yet been explored, though it is simple:
types objects
terms arrows ("tight" or vertical morphisms)
judgements proarrows ("loose" or horizontal morphisms)
inferences squares (2-morphisms)
This was a helpful rosetta stone, thanks!
Eduardo Ochs (May 11 2022 at 01:03):Hi @Christian Williams (and @Ralph Sarkis),
Do you have a collection of examples of translations between your diagrammatic language and other notations? Do you have a list of the conventions that you follow in your diagrammatic language?...
I am asking about examples of translations and conventions because this was what worked for me when I had to formalize the diagrammatic language that I had been using for years - shameless plug: link - but I am sure that many other approaches are possible...
Simon Burton (May 11 2022 at 11:06):It looks like these are string/sheet diagrams for 2-categories, in this case the bicategory of sets and relations (and implications).. This is a reasonably standard diagrammatic language, up to direction of time/composition..
Christian Williams (May 11 2022 at 16:09):Tom Hirschowitz said:
So, Christian Williams, could you maybe explain how the usual, syntactic account of logic forms a double category? Or perhaps sketch how the double category structure is related to the usual rules of logic?
Well, I don't yet know how to answer this in general. I just know that Rel models higher-order predicate logic, and I'm using this to motivate a logical interpretation of (nice) fibrant double categories, which includes many kinds of category theory.
Christian Williams (May 11 2022 at 16:17):Let be a double category. The category of objects and tight arrows is the category of types and terms. The category of proarrows and squares is the category of judgements and inferences.
Here is a square as an inference. inference.png
Christian Williams (May 11 2022 at 16:23):are types. and are terms. and are judgements. and is the inference.
In , these are sets, functions, relations, and an implication. Note that this interpretation supposes that this logic is made from a "base logic" ; for , this is , the very simple double category with one type, one term, two judgements "false" and "true", and one nonidentity inference from false to true.
Christian Williams (May 11 2022 at 16:28):By using all of the rich structure of , we can interpret each aspect of predicate logic. For example, universal quantification is given by right extensions and lifts. Extension.png
Christian Williams (May 11 2022 at 16:31):Like I said, I do not yet have much polished material. Perhaps one way we could discuss is to pick certain aspects of predicate logic to express in this way.
Reid Barton (May 11 2022 at 16:35):Christian Williams said:
Okay, yes well above you can find that I am talking about double categories as logical systems. I do not know of any reference; I've been surprised to see that this has not yet been explored, though it is simple:
types objects
terms arrows ("tight" or vertical morphisms)
judgements proarrows ("loose" or horizontal morphisms)
inferences squares (2-morphisms)
Should I think of this as like a version of [[hyperdoctrines]] but for binary relations rather than unary ones?
Christian Williams (May 11 2022 at 16:36):I think the main difference of this interpretation is taking inference as an explicit part of the structure, rather than as a "meta-structure" for forming and computing things inside the structure. So here, behind the scenes, there are "meta-inferences", the simplest of which is composition of inferences. (This is why I'm developing FDC as a triple category.)
Christian Williams (May 11 2022 at 16:37):Reid Barton said:
Should I think of this as like a version of [[hyperdoctrines]] but for binary relations rather than unary ones?
Yes, that's right. The main way to get nice double categories, if you don't already have one, is with monoidal fibrations.
Christian Williams (May 11 2022 at 16:40):Given a monoidal fibration (possibly a nice one, such as a hyperdoctrine), pulling back along the tensor of the base gives a fibrant double category. It just "spreads out" the fibration in a nice way, and reveals an extra dimension which was implicit in the monoidal structure. is obtained in this way from the subobject fibration over .
Christian Williams (May 11 2022 at 16:44):So in this way, the interpretation is not new. People have long interpreted a fibration over a base as a logic over a type system (Jacobs' Categorical Logic and Type Theory).
Christian Williams (May 11 2022 at 16:48):What is new is extending the logic to other double categories, particularly categories enriched in monoidal fibrations. This logic contains enriched categories, internal categories, and more.
James Deikun (May 11 2022 at 17:06):Does the fibrant double category of polynomials get a logic or is it not nice enough?
Christian Williams (May 11 2022 at 17:07):Oh, I'm sure it has a very nice logic. I'd be interested to explore that question.
Christian Williams (May 11 2022 at 17:12):I think you get the richest logic when you completely understand/formalize some base logic, and then do some canonical construction to form your double category of interest. (I've been focusing on the construction of monads and modules, in order to construct a logic of categories.) What is a canonical way to construct Poly?
Christian Williams (May 11 2022 at 17:18):I think the answer is likely in Polynomials, Fibrations, and Distributive Laws (von Glehn).
Matteo Capucci (he/him) (May 11 2022 at 20:26):Christian Williams said:
By using all of the rich structure of , we can interpret each aspect of predicate logic. For example, universal quantification is given by right extensions and lifts. Extension.png
Is this in your paper or should I ask here to elaborate on this point? It seems very cool!
John Baez (May 11 2022 at 20:37):Christian's paper is called his "thesis" and it'll be done by June 2023. :upside_down:
John Baez (May 11 2022 at 20:38):Maybe he'll finish and release some preliminary pieces before that....
Christian Williams (May 11 2022 at 20:54):I can elaborate here. Is there any aspect in particular you wonder how it might be interpreted?
Christian Williams (May 11 2022 at 21:02):Rel embodies predicate logic, for the same reason that the fibration of Pred over Set does (Jacobs Ch5); I just think of Rel as fundamental, because I think on a basic level we understand the world through relations.
Tom Hirschowitz (May 12 2022 at 07:05):Oh, maybe I'm sort of getting it now. Do you mean that a certain kind of fibrant double categories may be viewed as an alternative to whatever kind of fibration is considered as the standard notion of categorical model of predicate logic (hyperdoctrines?)?
Tom Hirschowitz (May 12 2022 at 07:06):Would you mind explaining universal quantification in a bit more detail, please?
Nathaniel Virgo (May 12 2022 at 07:15):I hope you don't mind a really dumb question, but what does it mean to say that a function is a "term" or that a relation is a "judgment"? I'm familiar with those words in a fairly informal way, but would have expected a term to be an element of a type, rather than a function between two types. (I'm not really sure what I would have expected a judgment to correspond to formally.)
John Baez (May 12 2022 at 07:21):I guess the simplest kind of term of type is a morphism where is terminal, i.e. an 'element' of . But it pays to work a bit more generally with 'generalized elements', which are just morphisms , being some other type.
John Baez (May 12 2022 at 07:22):It's pretty well-known that elements are not always enough to fully probe an object .
John Baez (May 12 2022 at 07:23):So I would not be shocked if someone called a morphism a 'generalized' term of type .
John Baez (May 12 2022 at 07:23):Or if you like, an '-parametrized family of terms of type ', or something like that.
John Baez (May 12 2022 at 07:24):Mind you, I don't do type theory so I don't talk like a well-educated type theorist.
John Baez (May 12 2022 at 07:25):I'm just saying some category theory while trying to make it sound like type theory.
Todd Trimble (May 12 2022 at 10:45):Tom Hirschowitz said:
Would you mind explaining universal quantification in a bit more detail, please?
For example, suppose and are relations. The right Kan extension of along is a relation such that 2-cells are in natural bijection with 2-cells . In logical notation, the latter take the form
and so when you calculate from here what must look like by playing with adjunctions of - and type, you get
which is how both and emerge naturally from right Kan extensions. Something similar happens with right Kan lifts. All of this can be seen in the light of end/coend calculus (hi @fosco ).
fosco (May 12 2022 at 11:15):Hi!
yes, on a similar vein I was yesterday years old when I discovered that the preorder on sets is just ( :smiling_devil: ) the codensity monad of the membership predicate
fosco (May 12 2022 at 11:17):this is because the right kan extension of applied to (x,y) is just the universal quantification
Todd Trimble (May 12 2022 at 13:06):Yep -- this fact is actually one of the axioms for the Freyd-Scedrov notion of power allegory. I think maybe C.S. Peirce knew it too.
Tom Hirschowitz (May 12 2022 at 14:24):Thanks, @Todd Trimble!
Christian Williams (May 12 2022 at 16:59):Nathaniel Virgo said:
I hope you don't mind a really dumb question, but what does it mean to say that a function is a "term" or that a relation is a "judgment"? I'm familiar with those words in a fairly informal way, but would have expected a term to be an element of a type, rather than a function between two types. (I'm not really sure what I would have expected a judgment to correspond to formally.)
I think of the words as follows. In a logical system, terms are the things we're thinking about, judgements are thoughts about them, and inferences are the flow of reasoning between thoughts.
Christian Williams (May 12 2022 at 17:00):So in predicate logic, one might say that we're reasoning about elements of sets; but one could argue that we are more generally reasoning about functions. I think this generalization is helpful.
Christian Williams (May 12 2022 at 17:03):For example, consider the inference "if person p hears song s, then heart(p) feels beat(s)". One could see this as an inference about people and songs, but I think it's more precisely about the pair of functions (heart, beat).
Christian Williams (May 12 2022 at 17:06):Similarly in category theory, I would propose that we are thinking about functors, while the "judgements" we make are profunctors.
Christian Williams (May 12 2022 at 17:07):This is a pretty loose explanation. I'm curious what other people think.
Christian Williams (May 12 2022 at 17:20):Tom Hirschowitz said:
Oh, maybe I'm sort of getting it now. Do you mean that a certain kind of fibrant double categories may be viewed as an alternative to whatever kind of fibration is considered as the standard notion of categorical model of predicate logic (hyperdoctrines?)?
Yes, the initial idea is to think of fibrations as the double categories they form. But this also motivates a more general perspective of double categories as logical systems - once we formalize the language of the double category Rel, then we can use this language to form the richer double category Mod(Rel), monads in Rel are preorders. This is a very rich language, and it cannot be constructed directly from any fibration.
Christian Williams (May 12 2022 at 17:37):But really, this is why double categories are essential. In the same way that we need both functions and relations in everyday math, we need both functors and profunctors in category theory.
Categories should be defined as monads, so that profunctors are just "relations with action". This perspective is not apparent in most books, because it requires two dimensions. That's what I hope to address with string diagrams.
Christian Williams (May 12 2022 at 17:40):People still make jokes online about the fact that "a category is a monad", meaning this must be an extremely abstract or esoteric fact. But I think this is actually the simplest way to explain categories to people, and this is how I plan to teach to young students. I don't know how it could get any more simple than this picture. Monad.png
Christian Williams (May 12 2022 at 17:42):The string diagram is the monad, which is precisely the shape of the inference of composition.
Nathaniel Virgo (May 13 2022 at 02:02):Thanks John Baez and Christian Williams for the explanations about terms and functions, that does make sense.
I'm still curious about the notion of judgment as a relation between types - could you say a bit more about that? I might be interpreting the term "judgment" wrongly - I've only come across that word as meaning a statement that a particular term has a particular type, but that seems like it should be something like a function from terms to types, rather than a relation between two types.
Christian Williams (May 13 2022 at 04:41):Yes, I am using the word judgement differently than normal. A relation is a matrix of propositions; in most type theories it is a two-variable type. But "judgement" seemed to be the only right choice of name, because I think inferences go between judgements.
Christian Williams (May 13 2022 at 04:42):But yes, here the "term judgement" you're referring to is the inference .
Morgan Rogers (he/him) (May 13 2022 at 08:10):Christian Williams said:
People still make jokes online about the fact that "a category is a monad", meaning this must be an extremely abstract or esoteric fact. But I think this is actually the simplest way to explain categories to people, and this is how I plan to teach to young students. I don't know how it could get any more simple than this picture. Monad.png
It could get simpler if you removed the blue background and bemusing lines?
I think the concept of a visual presentation of logic and categories is fantastic, and I support it being grounded in further category theory, but supposing that exposing the more advanced category theory that you're relying on makes things simpler is a very strange concept to me. How do you expect students to pick up double categories or bicategories, or even a specific case of such things, before seeing what a category is? It's fine for you to present the framework and pull the tablecloth out from under them later to reveal that they've been implicitly working with these structures all along, but it seems inevitable to me that you will have to hide some of the abstraction/formalization until they have developed some familiarity with the structures you're teaching them about.
Matteo Capucci (he/him) (May 13 2022 at 10:26):I believe Christian's idea is to never explain what a proarrow equipment is. You just introduce notation, and an intepretation thereof.
Matteo Capucci (he/him) (May 13 2022 at 10:27):This is similar to how ZX-calculus people work/popularize their stuff: it's just a notation, that happens to be backed by category theory
Christian Williams (May 13 2022 at 16:24):Children already know sets, relations, and implications. "If I eat food that has sugar, then I'll get energy." They already think in two dimensions; I think hiding that from them only complicates and obscures everything.
Christian Williams (May 13 2022 at 16:26):but yes, of course we have to hide some parts of the abstraction/formalization, especially at the beginning. The education program I'm imagining is long-term.
Christian Williams (May 13 2022 at 16:28):It could get simpler if you removed the blue background and bemusing lines?
It is two pictures overlaid, the syntax and the string diagrams. You set them side-by-side, then overlay them to show how they're equivalent.
Christian Williams (May 13 2022 at 16:30):sorry I have to go; I'm going to Valley of Fire state park in Nevada. thanks for your thoughts.
Morgan Rogers (he/him) (May 13 2022 at 17:43):Thanks for the thoughtful responses. I am confident that you are taking the time to ensure that everything is clear, and I hope I didn't seem down on the ideas. Good luck!
Mike Shulman (May 13 2022 at 17:55):Here's how I think of the word "judgment" arising here.
Suppose we have some collection of "function symbols" with arities. Then we can generate "terms" by applying these to variables. For instance, if has arity 2 and has arity 1, we have a term with two variables . (In general, the variables and functions might have types, but for simplicity let's consider the un(i)typed case. The kind of example you should think of is generating the types, terms, or propositions in some type theory or logic, where the "function symbols" are the formation operators. For instance, if the function symbols are of arity 2, we generate propositions in propositional logic.
Now suppose we have some collection of judgments that depend on some number of terms. You should think of term-membership or entailment judgments in a type theory or logic, for instance is a judgment depending on two terms and . So is an entailment with two assumptions, etc.
Finally, we complete the definition of a type theory or logic by giving primitive inference rules, each with some number of judgments as premises and one judgment as conclusion. Crucially, each such rule involves some number of variables, and all the terms appearing in it are built from those variables. For instance, the introduction rule for conjunction is
Here the variables are , and is a term built from those (as are the variables themselves appearing in the other judgments). Similarly, the elimination rule for implication is
and the "cut" rule is
From these primitive rules, we can construct derivation trees in the usual manner.
Now let's restrict to a special case such that:
Then each inference rule looks like
This contains the same data as a square in a double category, if we label the horizontal arrows by judgments and the vertical arrows by terms. Moreover, derivation trees correspond to vertical composition of these squares.
To get something like horizontal composition, we can add a couple of special inference rules exempt from requirement (2), namely a "cut"
an an "identity"
In fact from this perspective it's a bit more natural to think of a [[virtual double category]], which allows you to discard requirement (2) altogether, and add exactly as many cut and identity rules as you want, if any.
Christian Williams (May 16 2022 at 03:19):I agree that virtual double categories are more natural. You seem to phrase this as though you already know what structure models the general case. How might we relax the rest, 1 and 3 and 4? I can offer some thoughts.
Christian Williams (May 16 2022 at 03:28):
- Each judgment depends on exactly two terms, which we can call its "domain" and "codomain".
I should clarify that my thesis is not about arbitrary double categories, but "cosmoses" of categories. Their "logic" is much richer than the general case, and that is my focus.
So for point #1, VCat is (usually) compact closed monoidal: a judgement is multivariable. The distinction of domain and codomain is the distinction of "positive and negative" variables, meaning their variance.
Christian Williams (May 16 2022 at 03:36):
Each inference rule depends on exactly two variables, say xx and yy, and moreover these two variables are precisely the terms on which its premise depends.
The domain term of the conclusion of each inference rule depends only on the domain variable xx in the premise, and similarly the codomain term depends only on the codomain variable yy.
What are some examples of inferences that are not of this form? To me, they seem natural to assume without loss of generality.
Christian Williams (May 16 2022 at 03:39):I recognize that composition and identity of a double category, as you say, are two canonical examples; but to me these are inferences of metalogic.
Christian Williams (May 16 2022 at 03:41):well, there's more to say about that; but first I'm just curious what more general kinds of inferences you have in mind.
Mike Shulman (May 16 2022 at 06:50):Well, the usual semantic context used for first-order logic (which is basically what the general case is, only using the words "judgment" and "inference" rather than "proposition" and "entailment") is a hyperdoctrine, i.e. a monoidal fibration. I have trouble imagining a semantic structure other than this that would model logic with all of those conditions relaxed completely. I agree that a "compact closed double category", whatever that means (-:, is a natural structure for relaxing (1) to something like "the terms on which each judgment depends are partitioned into two groups called 'domain' and 'codomain'".
Mike Shulman (May 16 2022 at 06:59):The elimination rule for implication:
is an example of a rule that violates (3): one of the premise judgments involves a term that is not a variable.
I'm not saying that necessarily rules out modeling it in some double-categorical way. I haven't thought about that at all.
I think this distinction is analogous to that in dependent type theory between the "generalized algebraic theories" of Cartmell and the more restricted "dependently typed algebraic theories" of Leena Subramaniam: are arbitrary terms allowed to appear in the dependencies of the inputs of an operation?
Mike Shulman (May 16 2022 at 07:00):Another example, which has only one premise, is the elimination rule for conjunction:
Christian Williams (May 16 2022 at 16:57):Well, both of these example inferences exist in Rel as well, by representability: an extension along Q of R is equipped with an inference . So we have and concludes .
Because Prop is complete, Rel is higher-order; the judgement "" is a relation on the set of relations between two sets. I think that's why examples like these can be given within the language of Rel.
Christian Williams (May 16 2022 at 17:04):It seems like the example inferences one might cook up which "go beyond" the form of ordinary squares are precisely those which are given by the extra structure of the double categories of interest, e.g. being closed or complete.
Mike Shulman (May 16 2022 at 18:54):I think you're mixing levels from what I was talking about. I was talking about as a term constructor, not as an operation on judgments.
Christian Williams (May 16 2022 at 21:12):I'm saying that in a higher-order logic, such as Rel, for each pair of types and there is a type of judgements (set of relations) , equipped with an judgement of entailment . Hence the terms of are judgements, and a judgement constructor in the double category induces a term constructor on . Does that make sense?
Mike Shulman (May 17 2022 at 03:35):Yes, absolutely. It's just not what I'm talking about.
Christian Williams (May 19 2022 at 23:39):Here is a working title and contents. title.png contents.png
Christian Williams (May 19 2022 at 23:46):Soon I hope to have a webpage to share a developing draft. Even if it's messy, I want to communicate publicly during the process of writing, rather than after publishing, because anyone could have very helpful and valuable input.
Georgios Bakirtzis (May 20 2022 at 00:16):What is cosmic logic?
Christian Williams (May 20 2022 at 00:41):The higher coend calculus of FDC, the triple category of fibrant double categories (aka equipments), lax functors, (tight/vertical) term bimodules, and (loose/horizontal) judgement bimodules.
Christian Williams (May 20 2022 at 00:44):The terms of this logic are lax functors, which generalize enriched, internal, and fibered categories (and also sheaves and stacks).
Christian Williams (Sep 13 2022 at 16:01):Hello, I want to share what I've been developing for my thesis.
I'm defining the 3-dimensional monad construction: given a triple category T, it forms the triple category Mnd(T) of (pseudo)monads, functors, vertical & horizontal modules, V & H transformations, "double modules", and modifications.
The triple category MatCat is like Cat plus a new dimension consisting of 2-variable fibered categories, aka matrices. When the Mnd construction is applied, it forms the triple category of Fibrant Double Categories, which I am thinking of as Logics.
Here is a draft of the Mnd construction. Logos-MndMatCat.pdf It uses string diagrams, by slicing the cube like an MRI.
Christian Williams (Sep 13 2022 at 16:05):There are still details to be filled in, like the "internal view" and logical interpretation of several of the cells (as well as naming everything by a symbol, for easier reference.) Please let me know if something is unclear.
I think I'll take some excerpt images and talk about it here.
Mike Shulman (Sep 13 2022 at 16:06):How strict are your triple categories?
Christian Williams (Sep 13 2022 at 16:07):I believe they have strict pentagon & triangle identities for assoc and unit. (because fibrations are nice)
Christian Williams (Sep 13 2022 at 16:13):Also to clarify why I'm doing this:
The coend calculus is the language of monads - ends provide the "natural universal" for transformations of modules, and coends provide the "bilinear existential" for composing modules.
So, constructing FDC as Mnd(MatCat) defines a higher coend calculus, which should subsume and hopefully unify the coend calculi of FDCs in category theory.
Christian Williams (Sep 13 2022 at 16:18):String diagrams are truly powerful. Without them I certainly could not have really seen and grasped this construction - and now with them, it has become as easy as playing.
Christian Williams (Sep 13 2022 at 16:19):By taking slices, we can extend string diagrams for double categories into higher dimensions. Let me show an example of a cube.
Christian Williams (Sep 13 2022 at 16:24):
Christian Williams (Sep 13 2022 at 16:27):The key to the 3D monad construction is as follows:
In Cat, profunctors can be understood to give "heteromorphisms" between categories. Now here, double categories simply have two kinds of hetero-cells! Those are the "vertical & horizontal modules". So pictured above is the one for vertical heteromorphisms.
Christian Williams (Sep 13 2022 at 16:29):So to define a V-Module, we have a profunctor for the actual sets of v-heteros, but we also need a fibered profunctor to provide the inferences (hetero-squares) which introduce these terms.
Christian Williams (Sep 13 2022 at 16:30):Any way, one example of a non-globular cube in this construction is the horizontal composition of these hetero-terms. That's the bottom row in the picture. Blue is the front, purple is the middle, and red is the back of the cube.
Christian Williams (Sep 13 2022 at 16:34):The funny thing is that there are three ways of looking at a cube, and at first it can be very confusing. For a few weeks I was looking at that cube from the top rather than the side, and it took a while to rotate and recognize "oh! a vertical module (purple) is really 'a monad in the profunctor direction' ". That clarified a lot.
Christian Williams (Sep 13 2022 at 16:40):Any thoughts and questions are welcome. (I can also lay out the construction here step-by-step.)
Matteo Capucci (he/him) (Sep 13 2022 at 16:56):I see some of your 1-cells are fibered cats, fibered over what?
Matteo Capucci (he/him) (Sep 13 2022 at 16:57):Ah maybe you simply meant a fibration
Matteo Capucci (he/him) (Sep 13 2022 at 16:57):What's your def of fibered profunctor? A fiberwise profunctor?
Christian Williams (Sep 13 2022 at 17:11):Yes, a 2-variable fibration, so equivalently a pseudofunctor A°xB° to Cat.
Christian Williams (Sep 13 2022 at 17:15):A fibered profunctor is basically a fiberwise profunctor, yes. Over each hetero in the base, there is a profunctor of heteros lying over it between the fibers of its domain and codomain. For an arbitrary transformation this assignment is lax, and a fibered profunctor is one for which the assignment is pseudo.
Matteo Capucci (he/him) (Sep 13 2022 at 17:21):Cool
Matteo Capucci (he/him) (Sep 13 2022 at 17:21):By complete chance I was contemplating a construction today where (I think) these things popped up from the math
Matteo Capucci (he/him) (Sep 13 2022 at 17:25):I'm not completely sure though bc I got bored with the details. What I was trying to do is proving horizontal transformations between normal, lax double functors (where is a category turned into a vertically discrete dbl category, and is the proarrow equipments of cats, functors, spans of functors and 'morphisms of 2-spans') are the same thing as 'spans in ', i.e. commuting squares with in the right bottom corner
Matteo Capucci (he/him) (Sep 13 2022 at 17:26):I'm not completely sure about the part though... originally this theorem works for vertical transformations between normal, lax double functors , but I'm afraid profunctors might be too weak to exhaust
Matteo Capucci (he/him) (Sep 13 2022 at 17:27):If you could post the details of your 'fiberwise profunctors' they might be useful to me to understand what's going on here
Christian Williams (Sep 13 2022 at 17:27):oh cool, that sounds really similar. it's in another thread on here, let me find it
Christian Williams (Sep 13 2022 at 17:29): Mike Shulman (Sep 13 2022 at 17:31):Back to my question, sorry for being so nitty-gritty-minded: so a triple category has three directions of composition. Presumably some of them are strict, and you're saying at least one of them is weak at the bicategorical level? In particular, are your triple categories an instance of a structure in the literature like an [[intercategory]]?
Christian Williams (Sep 13 2022 at 17:36):no, it's a good question; I need to double-check this stuff for myself. so MatCat is strict in the functor direction, 1-weak in the profunctor direction, and 1-weak in the fibration direction (the pentagonator & triangulator are identities).
Christian Williams (Sep 13 2022 at 17:37):When forming the Mnd construction, I think the "weakest" thing that happens is the pseudocoequalizer needed to compose horizontal modules (which I'm calling "metajudgements").
Christian Williams (Sep 13 2022 at 17:39):The functor direction will be strict (because it's functors and fibered functors), and the vertical module direction will be 1-weak (because it's profunctors and fibered profunctors).
Christian Williams (Sep 13 2022 at 17:40):So I need to think about composing those modules. But I think it will be pretty well-contained.
Christian Williams (Sep 13 2022 at 17:48):the composite of and is a pseudocoequalizer of two fibered functors, the inner actions by . it's just like composing profunctors, except just a little bit weaker.
Christian Williams (Sep 13 2022 at 17:48):anyone know a good reference for pseudo-coequalizers? or pseudo-colimits in general
Mike Shulman (Sep 13 2022 at 17:54):The "pseudocoequalizer" you want here is sometimes called a [[codescent object]].
Mike Shulman (Sep 13 2022 at 17:56):A similar composition of bicategorical modules appears in section 6 of Enriched categories as a free cocompletion, among other places probably.
Mike Shulman (Sep 13 2022 at 17:58):So it sounds like your input is an intercategory, but your output is something weaker where the composition in one of the directions is tricategorical (maybe not as weak as a general tricategory, but weaker than a bicategory)?
Christian Williams (Sep 13 2022 at 18:00):thanks; Street's Fibrations in Bicategories and your paper will be sufficient.
Christian Williams (Sep 13 2022 at 18:02):yeah, that seems right... but it's just quotienting a pair of matrices of functors; so it doesn't seem like it should be too bad.
Ivan Di Liberti (Sep 13 2022 at 18:15):Hi Chris. I think this looks very cute and neat. I am looking forward to seeing the paper.
Christian Williams (Sep 13 2022 at 18:20):thanks. I know you've done formal CT - what do you think of the motivation, a coend calculus for FDCs?
Ivan Di Liberti (Sep 13 2022 at 18:33):When you look at the theory of coends from the perspective of Yoneda structures, or proarrow equipments, or KZ doctrines, what I think emerges quite clearly is that they are not a fundamental notion, they can be built out of Kan extensions (and their incarnation in these worlds). Thus, if by "coend calculus" you mean "a calculus of Kan extension" for FDCs, I think this is great and has potential applications to many things I think about daily.
I also find fascinating the naming you chose for a lot of these concepts. Most of them seem well chosen to me, I would suggest though to instantiate this framework in concrete examples, to check whether they meet their respective incarnation in each context.
PS. My answer is very vague, but your question is too ;). Also, I have a strong tendency to reject work in progress and judge stuff that is at least on the arXiv. There are several reasons for this choice, I do not want to discuss them here. Thus I think I should not go further with comments.
Christian Williams (Sep 13 2022 at 18:34):great! I understand; thanks for the comments.
Mike Shulman (Sep 13 2022 at 18:35):I could be wrong, but I don't think tricategorically-weak triple categories exist in the literature yet. So you may have some definitions to formulate before you can prove a theorem... (-:
Christian Williams (Sep 13 2022 at 18:36):yes, I would definitely like to discuss more the logical interpretation of double categories: objects are types, tight morphisms are terms, loose morphisms are judgements, and squares are inferences. for me, this interpretation has been very fruitful.
Christian Williams (Sep 13 2022 at 18:36):ah, okay. I guess I shouldn't be surprised, I have my work cut out for me.
Christian Williams (Sep 13 2022 at 18:46):can you say more about why you consider extensions to be more fundamental than co/ends? because the two are interdefinable, when they exist; do you mean how sometimes the extension exists but the end does not?
Ivan Di Liberti (Sep 13 2022 at 18:46):Christian Williams said:
yes, I would definitely like to discuss more the logical interpretation of double categories: objects are types, tight morphisms are terms, loose morphisms are judgements, and squares are inferences. for me, this interpretation has been very fruitful.
I think this is an intriguing and yet very dangerous point of view. Let me clarify this.
Let E be a Grothendieck topos. Then, if you see it an an object of the 2-category of elementary topoi and logical morphisms between them, this is an higher order theory. If we see it as an object in the 2-category of Grothendieck topoi, it is a geometric theory. If we look it as an object of the 2-category of doctrines (where it is represented as (E,Omega)) it is again a geometric theory, but we have a different take on it. Because the topos is an LCC it is also a model of very fancy lambda calculi.
This example is to say that the object of mathematics, especially at this level of generality can be almost everything, and more than the mere instantiation of an interpretation it is more telling (at least in my opinion) to relate and connect them to existing notions, because this taxonomy of mathematical language reveal their meaning much more than an isolated take on it.
Greta Coraglia and I recently have a paper where we show that one can use Cat to simulate deductive systems in a quite simple way, almost too simple in a sense. I do not think that work would be of any value if it would not recover completely the existing approaches à la Jacobs, or à la Taylor, or similia.
This is also why I suggested to clarify the relationship with existing frameworks having a similar or even a different purpose.
Christian Williams (Sep 13 2022 at 18:49):hm, I'm not sure what you mean. if we take a very general view of "logics", of course the notion of "type" in a logic can vary greatly. why could this be a problem?
(maybe I'm not quite understanding your point; by "dangerous" do you mean over-general?)
Mike Shulman (Sep 13 2022 at 18:50):Ivan Di Liberti said:
When you look at the theory of coends from the perspective of Yoneda structures, or proarrow equipments, or KZ doctrines, what I think emerges quite clearly is that they are not a fundamental notion, they can be built out of Kan extensions (and their incarnation in these worlds).
What emerges clearly to me is the exact opposite. The natural thing that is immediately definable from the structure of a proarrow equipment is a weighted (co)limit, which is of course almost the same as a (co)end. Pointwise Kan extensions are then just a particular case of a weighted (co)limit.
Ivan Di Liberti (Sep 13 2022 at 18:51):Mike Shulman said:
Ivan Di Liberti said:
When you look at the theory of coends from the perspective of Yoneda structures, or proarrow equipments, or KZ doctrines, what I think emerges quite clearly is that they are not a fundamental notion, they can be built out of Kan extensions (and their incarnation in these worlds).
What emerges clearly to me is the exact opposite. The natural thing that is immediately definable from the structure of a proarrow equipment is a weighted (co)limit, which is of course almost the same as a (co)end. Pointwise Kan extensions are then just a particular case of a weighted (co)limit.
A weigthed colimits is literally defined as a Kan extension.
Mike Shulman (Sep 13 2022 at 18:51):No, it's not.
Christian Williams (Sep 13 2022 at 18:54):well, so, in my mind "category theory" is basically "monad theory". so even though there are FDCs which are not of the form Mod(-), I think the most important ones are those of monads and modules. then I contend that the "internal logic" is that
ends are the "universal quantification with naturality" for transforming modules (reifying inference) and
coends are "existential quantification with bilinearity" for composing modules (composing judgement).
one can then derive weighted co/limits and extensions from these two basic constructors.
Christian Williams (Sep 13 2022 at 18:58):I recognize that this perspective may not be of maximum generality, but I think it is clarifying and fruitful.
Ivan Di Liberti (Sep 13 2022 at 19:02):Christian Williams said:
well, so, in my mind "category theory" is basically "monad theory". so even though there are FDCs which are not of the form Mod(-), I think the most important ones are those of monads and modules. then I contend that the "internal logic" is that
ends are the "universal quantification with naturality" for transforming modules (reifying inference) and
coends are "existential quantification with bilinearity" for composing modules (composing judgement).one can then derive weighted co/limits and extensions from these two basic constructors.
I will be very happy to read your paper on the topic.
Ivan Di Liberti (Sep 13 2022 at 19:03):Mike Shulman said:
No, it's not.
I cannot engage in this debate. Sorry. I have to finish an application in the next 3 hours. I will be tenured too one day, and I'll be back with my army. (It's not true, I won't be back. Forum-like conversations are just not my thing.)
Christian Williams (Sep 13 2022 at 19:13):to be more concrete, a right extension is the "currying" of the binary hom given by an end; and this currying is possible because composition by coend is bilinear.
Christian Williams (Sep 13 2022 at 19:13):oh okay, good luck!
Christian Williams (Sep 13 2022 at 19:44):also to address recent discussion of @Bruno Gavranovic and @Matteo Capucci (he/him) , the triple category of FDCs and lax functors is defined by taking the 3-cells as noninvertible, only "pushing the beads upward". see "System (Functor)" in Logos-MndMatCat.pdf, and
Christian Williams (Sep 13 2022 at 23:01):let and be horizontal modules of FDCs. hence and are matrices of categories, equipped with actions and .
hence there is a pair of fibered functors . the composite should be a suitable quotient of these two inner actions.
I think it isn't too mysterious. consists of pairs of "composable heteromorphisms" and pairs of horizontally-composable hetero-2-morphisms. when should two pairs be equal? if there exists such that and , i.e. if "whiskering" by the middle gives each equation of hetero-2-cells.
this seems like "the only reasonable answer", just following intuition.
Christian Williams (Sep 13 2022 at 23:06):if this is correct, then it seems to be as associative as ordinary profunctor composition. the associator is just "shifting parentheses"; ultimately it's just formal composition of hetero-2-cells. why or even how could there be a nontrivial pentagonator?
Christian Williams (Sep 13 2022 at 23:41):oops, I made it sound like B was acting only as a category. the matrix of hom-categories of B is what's acting on M and N; so it's not just "whiskering" by a middle morphism, but horizontally composing with any 2-cell in B.
Christian Williams (Sep 14 2022 at 00:13):One idea that's really helped in guiding my intuition is the fact that Mnd(-) is completion by collages. A profunctor really is a "hom between categories" (becoming an actual hom in the collage) - even when you think you're reasoning between categories, you're really inside a bigger one!
I think collage is the basic notion of "union type" in the "logic of categories", meaning that judgements are understood to connect objects of possibly different types. In some wavy way, I feel as though the completion theorem formalizes the idea that the logic of categories is completely "free-flowing".
Christian Williams (Sep 14 2022 at 00:18):This greatly helped in defining the 3-dimensional monad construction, because if I was ever unsure of how a module or a transformation should work, I could just imagine that the elements really were (vertical/horizontal) heteromorphisms. The 2D completion theorem (probably a huge task for 3D, probably won't do it for the thesis) gave confidence in the correctness of the construction, while also making the definitions more clear and simple.
Mike Shulman (Sep 14 2022 at 00:59):Christian Williams said:
if this is correct, then it seems to be as associative as ordinary profunctor composition. the associator is just "shifting parentheses"; ultimately it's just formal composition of hetero-2-cells. why or even how could there be a nontrivial pentagonator?
If I understand correctly, each is a category. So the "sensible" thing to do is never say that two pairs and of objects of these categories are equal, but only insert an isomorphism between them, coherently. That's what a codescent object does, and why you get a nontrivial associator.
Christian Williams (Sep 14 2022 at 02:54):ah, I meant to clarify that I was equating morphisms. but you're saying that we also need to insert these isomorphisms. is the latter the iso-coinserter and the former the coequifier?
Mike Shulman (Sep 14 2022 at 02:58):Yes, an iso-coinserter (or co-isoinserter) inserts isomorphisms and a coequifier equates morphisms.
Mike Shulman (Sep 14 2022 at 02:58):I generally prefer to think about it as a codescent object which inserts coherent isomorphisms all at once, rather than inserting them and then imposing their axioms.
Christian Williams (Sep 14 2022 at 03:37):wow, okay. guess it's time I really understand 2d colimits.
Christian Williams (Sep 14 2022 at 16:44):aha. Universal characterization of codescent objects understands codescent object as a kind of higher coend! I think this is extremely relevant to composing bimodules of FDCs.
Mike Shulman (Sep 14 2022 at 17:07):Exactly! Although the abstract is a bit misleading; a general codescent object is just a kind of 2-dimensional colimit, analogous to a coequalizer. A higher coend can be constructed as a codescent object, just as an ordinary coend can be constructed as a coequalizer, but not every codescent object is of this form.
Christian Williams (Sep 14 2022 at 17:41):Alright, so let's say we're composing with . This means we have pseudofunctors . We consider the following "coherence data": codescent.png
Christian Williams (Sep 14 2022 at 17:42):(replacing with )
Christian Williams (Sep 14 2022 at 17:45):and are domain and codomain, is identity, and are first and second projection of the source of each , and is the target of each . the relationships between these define 2-cells on the diagram.
Christian Williams (Sep 14 2022 at 17:48):so if and , then , , , , , and
Christian Williams (Sep 14 2022 at 17:55):need to check that I'm getting this right...
Christian Williams (Sep 14 2022 at 18:18):it's a bit more subtle than I thought. need to draw the right pictures
Christian Williams (Sep 14 2022 at 18:44):
Christian Williams (Sep 14 2022 at 19:23):this is very nice. it really is a two-dimensional tensor product, the "quotienting relations" of which are defined by certain 2-cells between actions.
Christian Williams (Sep 14 2022 at 19:38):
Christian Williams (Sep 14 2022 at 19:48):my and don't seem right; I don't want a 2-cell to equate with
Christian Williams (Sep 14 2022 at 19:59):hm, yeah I'm not seeing yet how this matches with what I imagined. I thought should be a category whose objects are composable pairs of hetero-1-cells, two of which are iso if there is a morphism in B that "cuts across" and equates them, and whose morphisms are composable pairs of hetero-2-cells, two of which are equal if there is a 2-morphism in B which "cuts across" and equates them. this looks different so far; but then again I don't really know the colimit yet.
Christian Williams (Sep 15 2022 at 05:04):
Christian Williams (Sep 15 2022 at 05:06):I'm learning the concept of codescent object from Codescent and coherence by Lack. It would be much harder without the guiding intuition of composing 2D relations.
Christian Williams (Sep 15 2022 at 05:20):the triangle is a hetero-inference. this "wave equation" says that (inferring in the left logic and transferring over) is equal to (transferring over and inferring in the right logic)
wave.JPG
Christian Williams (Sep 15 2022 at 05:22):yellow is 2d stuff, green is 1d, blue is 0d, and pink is the tensor which "collages" the actions together
Christian Williams (Sep 15 2022 at 05:26):(each string can be understood by what it does to the pink lines; and each bead by reading from left to right. sorry if the colors are too light.)
Christian Williams (Sep 15 2022 at 05:38):and I think the other is about coherently transferring identities bubble.JPG
Christian Williams (Sep 15 2022 at 05:39):so a "wave equation" for composites and a "bubble equation" for identities. that's nice
Christian Williams (Sep 15 2022 at 05:42):to form the codescent object - the pink, with the blue-to-pink string and the "star" bead - we first form the color and string as the coinserter of c and d. then to pose each equation, we form the coequifiers.
Christian Williams (Sep 15 2022 at 05:49):now just need the actual construction of coinserters and coequifiers in Cat.
Christian Williams (Sep 15 2022 at 06:03):a good reference is not immediately obvious, but it looks like Conformal Field Theory by T. Fiore constructs weighted colimits in Cat, chapter 4.
Christian Williams (Sep 15 2022 at 06:13):hm, okay it describes general (weak) unweighted colimits, which include pseudocoequalizers; then coproducts and tensors are clear, so by the theorem weighted-colim = cone-colim + tensors, we have all weighted colimits.
okay, but still need to determine coinserters and coequifiers explicitly. this is really interesting; I figured a 2-coend would just be a weak coequalizer, but it's a bit more complex and subtle.
Christian Williams (Sep 15 2022 at 06:22):okay, I was overthinking it. the objects of the (iso)coinserter are composable pairs, and the morphisms are composable pairs of 2-cells, plus new 2-isos for every .
Christian Williams (Sep 15 2022 at 06:24):that's like associativity for 1d hetero-hom-hetero composition.
then I think the coequifiers basically impose associativity for whiskering with a hetero-2-cell.
Christian Williams (Sep 15 2022 at 06:27):(I keep saying and drawing whiskering, but somehow there needs to be full parallel het-hom-het composition of 2-cells. any way, it's on the right track.)
Christian Williams (Sep 15 2022 at 17:25):In Fosco's Coend calculus 7.1.3, 2-profunctors are composed by forming a lax coend. It seems to be a bit different from the construction above.
Christian Williams (Sep 15 2022 at 17:25):There is no mention of coequifiers, but it may be implicit.
Christian Williams (Sep 15 2022 at 17:29):I'm pretty sure the equation drawing above with and is more complex than what falls out of a lax coend.
Christian Williams (Sep 16 2022 at 03:49):@Mike Shulman, how do you know that the composite is a codescent object? How does one determine the "right"/canonical way to compose double profunctors? Is there a good reference?
Mike Shulman (Sep 16 2022 at 04:06):Christian Williams said:
how do you know that the composite is a codescent object?
How do you know that the composite of ordinary profunctors is a coequalizer?
Christian Williams (Sep 16 2022 at 04:57):because it imposes associativity of hetero-hom-hetero composition.
Mike Shulman (Sep 16 2022 at 05:09):Okay, so a codescent object is what imposes that in this case, up to isomorphism.
Christian Williams (Sep 16 2022 at 05:14):okay... so is it also a lax coend? or is Fosco doing something different
Christian Williams (Sep 16 2022 at 05:31):I can also try to figure it out myself tomorrow.
if you know a good reference for composition by codescent, it would be appreciated.
Mike Shulman (Sep 16 2022 at 05:37):It's also a pseudo coend. Lax/pseudo coends can be constructed in terms of coproducts and lax/pseudo codescent objects, analogously to how ordinary coends can be constructed using coproducts and coequalizers.
Mike Shulman (Sep 16 2022 at 05:42):For one reference, I already mentioned section 6 of Enriched categories as a free cocompletion. It doesn't literally use coproducts + codescent objects, rather writing it as a single colimit, but you can make the functor in 6.6 into codescent data by taking coproducts, or more fancily by left Kan extension along a functor from the category to the domain category for codescent data.
Christian Williams (Sep 23 2022 at 01:32):to compose double profunctors, I think the sketches above are basically the whole idea. it looks like is constructed by (1) adjoin hetero-reassociating-isos and (2) identify 2-cells by associativity of hetero-horizontal composition. it doesn't seem like anything more is necessary.
Christian Williams (Sep 23 2022 at 01:35):the only other thing one could ask is "what equations do the new isos satisfy?" but I don't see any it could need. when we define the associator of a double category, we don't have to do any extra work to specify equations that its components satisfy. it seems like the same thing here; it's just inserting them in the hetero-hom-hetero composition.
Christian Williams (Sep 23 2022 at 01:43):sorry, of course the associator components have to satisfy the pentagon identity. so if there's any else to do in the construction, it would be for that.
Christian Williams (Sep 23 2022 at 01:58):I think this is the distinction between computing the colimits pointwise or not. is a single fiber of a fibered category, and the pentagon identity is an equation that spans across fibers.
Christian Williams (Sep 23 2022 at 02:42):anyway, somehow the pentagon identity will be imposed by a colimit.
I think I'm just realizing, composing higher profunctors shouldn't be advanced or scary, because they are really just bunches of hetero-morphisms. to define the composite, all you have to do is "cohere" horizontal composition of morphisms and heteromorphisms.
Mike Shulman (Sep 25 2022 at 00:20):I don't think there are any pentagons in this dimension. You're just constructing a category, so there's no room for things to be more than just associative inside that category. The associator for composition of double profunctors isn't something you insert in the construction of a particular composite.
Christian Williams (Oct 25 2022 at 19:02):Hello, this weekend I am giving a talk at Octoberfest 2022. I want to share the idea with the community before I spend the next six months writing it as my thesis. Hope you can join!
3d-talk.png
Christian Williams (Oct 25 2022 at 19:17):I propose:
(1) A "category theory" = a fibrant double category = a logic = a coend calculus.
(2) Category theories are unified in FDC = Mnd(MatCat), in the double coend calculus.
(3) We can grasp and work in this triple category, using 3D string diagrams.
Matteo Capucci (he/him) (Oct 25 2022 at 19:29):I'm very excited about this work, Christian! Do you think your talk will be recorded?
Christian Williams (Oct 25 2022 at 19:31):thanks! yes, I believe so.
Stelios Tsampas (Oct 26 2022 at 20:18):Christian Williams said:
I propose:
(1) A "category theory" = a fibrant double category = a logic = a coend calculus.
(2) Category theories are unified in FDC = Mnd(MatCat), in the double coend calculus.
(3) We can grasp and work in this triple category, using 3D string diagrams.
What is MatCat here?
Christian Williams (Oct 26 2022 at 20:27):Framed bicategories and monoidal fibrations: almost all FDCs (equipments) or "category theories" come from two constructions, the "framing" of a monoidal fibration, and the monad construction.
Given a monfib C1 over C0, pulling back along the tensor of C0 forms a fibrant double category. for example, forms , and forms .
Applying Mnd(-) forms categories internal to C and categories enriched in V, respectively.
Christian Williams (Oct 26 2022 at 20:29):In a great instance of the "cosm principle", can be formed in the same way! is a double fibration, and pulling back along forms what I call . two dimensions are , and the third is "matrices of categories", i.e. two-variable fibrations.
A fibrant double category is precisely a pseudomonad in MatCat. I define the 3-dimensional Mnd(-) construction, which (I believe) is far more simple and clear using 3D string diagrams.
Stelios Tsampas (Oct 26 2022 at 20:31):Christian Williams said:
framed bicategories and monoidal fibrations: most FDCs (equipments) come from two constructions, the "framing" of a monoidal fibration, and the monad construction.
given a monfib C1 over C0, pulling back along the tensor of C0 forms a fibrant double category. for example, forms , and forms .
then applying Mnd(-) forms categories internal to C and categories enriched in V, respectively.
OK, I didn't know that. Interesting pullback!
Christian Williams (Oct 26 2022 at 20:46):Yes. I think it's best understood as the construction of "generalized matrices". An object in the fiber over is an -matrix. For enriched categories, this is a literal set-indexed matrix; for internal categories, it is a matrix in the internal language.
Christian Williams (Oct 26 2022 at 20:51):But I want to point out, and are just two classic fibrations. The construction works for any monoidal fibration that "supports matrix composition", i.e. having fibered sums and Beck-Chevalley. There's a whole spectrum of the notion of "category" between enriched and internal that is largely unexplored.
Christian Williams (Oct 26 2022 at 21:05):Basically, I think the CT community has not yet collectively absorbed the unifying language of fibrant double categories, and I want to change that.
Christian Williams (Oct 26 2022 at 21:07):partly by giving them a much simpler name! my thesis will just call them "logics".
Christian Williams (Oct 26 2022 at 21:08):A logic is a category of types and terms, with a fibered category of judgements and inferences.
Christian Williams (Oct 31 2022 at 15:56):Hello, here is my talk: https://richardblute.files.wordpress.com/2022/10/williams-ofest-1.mp4
and the slides: Thinking-in-3D.pdf
I didn't present the whole 3d Mnd(-) construction, but I think I communicated the main point:
(1) A "category theory" = a coend calculus = a logic.
(2) Category theory is unified in the double coend calculus of FDC = Mnd(MatCat).
(3) We can grasp and work in this triple category, using 3D string diagrams.
Christian Williams (Nov 01 2022 at 17:47):It seems that most of us are so busy that we only have time and energy to engage with an idea when it's already completed and written up formally (with good exposition, too). I understand; but it's hard when you're doing a big project alone. (@John Baez and @Mike Shulman have helped a lot.)
Christian Williams (Nov 01 2022 at 18:07):I've just been a bit surprised with the quiet response, particularly people who study formal category theory. Like @fosco - haven't you been wanting this for a long time? A unified system of coend calculi.
Christian Williams (Nov 01 2022 at 18:08):(I don't mean to call anyone out; we can talk by direct message if you want.)
Christian Williams (Nov 01 2022 at 18:16):I'm sure many people on here are having the same difficulties, not having much community for collaboration. When I came to UC Riverside 5 years ago, we had a big and vibrant research group. By the time of the pandemic, everyone was gone.
Ralph Sarkis (Nov 01 2022 at 19:10):I am really sorry that I can only offer some validation for these feelings. :love:
Christian Williams (Nov 01 2022 at 19:20):Oh, that's alright. Thank you, I appreciate it.
I know other people are in similar situations, and so many people never even get the opportunity to research full-time. So I'm definitely fortunate.
Christian Williams (Nov 01 2022 at 19:27):A lot of it comes down to productivity and diligence... but not all. If I had been making nice blog posts over the past year, someone could have followed along and engaged... but the full view of the project wasn't clear until recently, after a year of solitary wandering. And now there isn't time for blog posts, because I need to write my thesis! So the timing just didn't work out.
Christian Williams (Nov 01 2022 at 19:40):Although - the part on the 3d Mnd(-) construction should be done pretty soon, so hopefully I'll put it on the arXiv in a month or so: mnd.pdf (draft that gets messier as it proceeds)
Morgan Rogers (he/him) (Nov 01 2022 at 20:08):Give it time to brew @Christian Williams. It's hard to judge the utility and flaws of a graphical system until you've really gotten your hands dirty with it, and it could take months to get to the point of really stress-testing it (even if one were to start right away). Have patience, and keep testing it yourself in the mean time
Christian Williams (Nov 01 2022 at 21:22):I understand. To clarify, the string diagrams are mainly to help people understand the Mnd(-) construction on triple categories, which is just to apply Mnd(MatCat)=FDC. "The project" is the language of FDC, the double coend calculus.
Christian Williams (Nov 01 2022 at 21:30):Experts have known for 40+ years that FDCs (equipments) unify the basic concepts of category theory (representation, extension, co/monad, etc). Yet nobody has defined the complete structure/language of all FDCs.
To be candid, in my view this means that Category Theory has not yet followed its own principle, to know the particular through the universal.
Fabrizio Genovese (Nov 02 2022 at 09:41):I am sympathetic with your feeling of quietness. I've been working on Petri nets for years and I've always had the impression they were a rather niche field of ACT. On the contrary there are other papers I've written of which I go way less proud that had a much bigger impact.
But this taught me something: Research is only a part of the work. The other part may be called 'marketing' and it's about writing blog posts, tweeting, giving as many presentations as you can.
I've always been bad at 'marketing', but this really is fundamental. Indeed, I noticed that while me, Fosco and Daniele didn't really push our work on Petri nets around too much, some of the coauthors in my other, more successful publications really did, and this paid off big time
Fabrizio Genovese (Nov 02 2022 at 09:42):Take home message is that, especially if you are aiming to an academic career, maybe slow down with research a little bit once you have something 'stable' and focus on going around and talking about it as much as you can. It will slowly get into people's heads that way.
Christian Williams (Nov 02 2022 at 15:10):Thanks Fabrizio, I understand.
Christian Williams (Nov 02 2022 at 15:13):I hope to make a book for a general audience, so marketing will be everything.
Christian Williams (Nov 02 2022 at 15:18):How do you find that it has paid off? More people who want to collaborate?
Fabrizio Genovese (Nov 02 2022 at 15:32):Christian Williams said:
How do you find that it has paid off? More people who want to collaborate?
Well, I found out that tweeting and blogging is boring AF, at least for me. But going around and meeting people is not. So I'm mainly doing that :grinning:
Fabrizio Genovese (Nov 02 2022 at 15:34):And yes, lots of interest especially from the crypto community atm. Another thing to keep in mind is that academia is weird. From the perspective of industry it is literally people fighting to the death for scraps (tenure track is like the sacred graal of academia and a tenured professor is often still paid less than the equivalent in industry). A consequence of this is that academia is incredibly competitive, especially when it comes to 'originality of research'. Way more than industry job market in my experience.
Fabrizio Genovese (Nov 02 2022 at 15:34):So it may be difficult to get other researchers' attention given that they are already very focused on their research and cannot really let go given how competitive it all is.
Fabrizio Genovese (Nov 02 2022 at 15:36):On the contrary industry is way more practical. If you have something, and that something may be useful, my personal experience is that people will listen to you and will give you credit. Also there are much more insanely skilled people in industry that the average academic would imagine, so it's not necessarily like talking to laymen. This is one of the reasons why I've been focusing more on the industry side than on the academic side in the last years. :smile:
Fabrizio Genovese (Nov 02 2022 at 15:37):(I'm not saying industry is perfect, it really is not. But paradoxically I find it way more relaxed than academia when it comes to 'thinking about my future' or stuff like that.)
Christian Williams (Nov 02 2022 at 15:42):Nice! Great to hear that it's working out for you.
Mike Shulman (Nov 02 2022 at 15:45):Fabrizio Genovese said:
And yes, lots of interest especially from the crypto community atm. Another thing to keep in mind is that academia is weird. From the perspective of industry it is literally people fighting to the death for scraps (tenure track is like the sacred graal of academia and a tenured professor is often still paid less than the equivalent in industry).
I'm glad you qualified that with "from the perspective of industry". In particular, I don't think most academics are in it for the money at all. I mean, obviously we need money to live on, and many of us wish our salaries were higher relatve to cost of living wherever our universities are located, and some of us may make decisions about jobs based on money. But if what we really cared about was money, we wouldn't be in academia at all, we'd be in industry; so from our perspective it's not "scraps".
Christian Williams (Nov 02 2022 at 15:45):I do not plan to go into academia. Though I want to develop new education materials, so I will probably need academic connections - especially for writing grants.
Fabrizio Genovese (Nov 02 2022 at 15:50):Mike Shulman said:
Fabrizio Genovese said:
And yes, lots of interest especially from the crypto community atm. Another thing to keep in mind is that academia is weird. From the perspective of industry it is literally people fighting to the death for scraps (tenure track is like the sacred graal of academia and a tenured professor is often still paid less than the equivalent in industry).
I'm glad you qualified that with "from the perspective of industry". In particular, I don't think most academics are in it for the money at all. I mean, obviously we need money to live on, and many of us wish our salaries were higher relatve to cost of living wherever our universities are located, and some of us may make decisions about jobs based on money. But if what we really cared about was money, we wouldn't be in academia at all, we'd be in industry; so from our perspective it's not "scraps".
I call it 'scraps' because many academic position literally don't pay enough to get a living, and that's shameful. In some countries postdoc salaries are below the poverty line. In other countries there are cases of university lecturers being homeless.
Mike Shulman (Nov 02 2022 at 15:50):I totally support people who choose a non-academic career path, and I'm glad those choices seem to be getting more attention these days than they used to. But we don't need to denigrate academia in order to give more respect to industry; both have advantages and flaws, they're just different.
Mike Shulman (Nov 02 2022 at 15:50):My point is that what academics are "fighting over", to the degree they're fighting over anything, is not the money at all.
Fabrizio Genovese (Nov 02 2022 at 15:51):I think we should denigrate ad nauseam any system in which paying many people so little that they barely make a living is normal. Especially given how much training and education one needs to get there.
Fabrizio Genovese (Nov 02 2022 at 15:51):And I'm not even going to talk about how graduate students are considered either students or workers depending on what's convenient to administration. :grinning:
Mike Shulman (Nov 02 2022 at 15:53):I think we have enough space in our brains to separate the shameful aspects of any "system" from its admirable ones.
Mike Shulman (Nov 02 2022 at 15:54):I agree that many academic salaries are shamefully low, and that competition for academic jobs is very hard. But at the level of personal interactions and research collaboration, my own experience has not been one of fierce competition, but more of cooperation, practicality, and openness.
Mike Shulman (Nov 02 2022 at 15:54):There are exceptions, but they are just that.
Mike Shulman (Nov 02 2022 at 15:56):Fabrizio Genovese said:
And I'm not even going to talk about...
... or adjuncts.
Fabrizio Genovese (Nov 02 2022 at 15:58):Mike Shulman said:
I agree that many academic salaries are shamefully low, and that competition for academic jobs is very hard. But at the level of personal interactions and research collaboration, my own experience has not been one of fierce competition, but more of cooperation, practicality, and openness.
Let me clarify. I do agree that many people in academia are nice and don't act competitively. What I'm saying tho is that getting into other people's research takes time. In a perfect world, I would have the time to do so. In the current world, I may be already spending _a lot_ of time trying to build my own career to be able to go deep into some other person research. This becomes truer and truer as that person research grows farther away from mine. Which is why sometimes we receive 'quieter than expected' replies and also why marketing can be important. :smile:
Steve Huntsman (Nov 02 2022 at 16:01):Fabrizio Genovese said:
I think we should denigrate ad nauseam any system in which paying many people so little that they barely make a living is normal. Especially given how much training and education one needs to get there.
I am sure that I'd be out of my league talking about economics with you but happy to be a heel. Is there a better system than a market at setting prices? And I mean "market" in a broad sense, including how publics allocate funding.
Mike Shulman (Nov 02 2022 at 16:02):Maybe let's not hijack Christian's thread any further to argue about economics? We have a stream for "off-topic"...
Mike Shulman (Nov 02 2022 at 16:07):To attempt to return to the original question: Fabrizio, I agree with your point that academics don't have enough time to get into someone else's research just for its own sake. Marketing helps, which in the case of academia usually means giving talks at conferences, as well as blogging and microblogging — and dare I mention writing nLab pages?
But what I think really helps is making your research useful to other people in the course of doing their research. That can mean a lot of things, such as doing lots of extended examples in your own work, or writing survey papers (or giving talks) aimed at different audiences.
Another aspect of this is just time. Even for the people who read your work, it takes time for them to understand it, time for it to percolate into their consciousness, time for them to realize that it's useful. Foundational work, especially, often takes a while to be appreciated. But if you hang out on places like Zulip and MathOverflow for a few years, occasionally you may see someone asking a question to which you can answer "well, I wrote this paper...". And then, maybe, over time more people will discover your work and find that it answers just the question they had. This has been my experience specifically with double-categories stuff: at first I didn't get much reaction to my framed bicategories and virtual equipments papers, but recently more and more people have been picking up the ideas.
Simonas Tutlys (Nov 02 2022 at 16:27):As a self-taught 'citizen scientist' trying to apply category theory to AI i feel the struggle of being heard. Like i'm reading papers from people in academia, comparing the ideas to mine and seeing that i might actually have something good is a bit screwy.i have some code that kind of works but is really not ready for public release yet,but seeing that people struggle with the same problem of community in academia makes my situation make more sense.
Christian Williams (Nov 02 2022 at 16:32):Academia has almost no incentive for good marketing and exposition, and I think this drastically limits progress. There are many ideas that could have reshaped the entire field decades ago, and currently it's a matter of just waiting for people to rediscover them and hopefully explicating them better. It's baffling, and I want to find a better way.
Simonas Tutlys (Nov 02 2022 at 16:43):Here's an idea for the more abstract sides of math: take a single subject and show that it can be applied to as many things that are popular as possible.categorical game theory for game mechanics etc. There's math youtubers like 3blue1brown who make videos like applying information theory to wordle,videos about the use of perlin noise to make the worlds in minecraft etc. But I don't know wether there are popular CT youtubers for example.Besides stuff like this:
https://m.youtube.com/watch?v=H0Ek86IH-3Y
Daniel Geisler (Nov 02 2022 at 17:19):The only successful outreach I've made has been through my website on my research. Even though I am unpublished, over time much of my work has been absorbed through osmosis. That is not how things are supposed to work, but it does work that way. One of the members here told me he became interested in mathematics after seeing my website. It would be nice to reach everyone, but it is sure sweet to strongly connect with individuals.
Simonas Tutlys (Nov 02 2022 at 17:25):'Supposed to work' sounds very rigid and prescribed,absorption of ideas through osmosis seems more natural and how things actually work :)
Ralph Sarkis (Nov 02 2022 at 18:02):Daniel Geisler said:
That is not how things are supposed to work, but it does work that way.
I've spent countless hours on academic websites following links and links to find out about people, their research and (sometimes) their personal life. I think putting stuff (not only research) out there is a great way to connect.
Georgios Bakirtzis (Nov 02 2022 at 18:33):Christian Williams said:
Academia has almost no incentive for good marketing and exposition, and I think this drastically limits progress. There are many ideas that could have reshaped the entire field decades ago, and currently it's a matter of just waiting for people to rediscover them and hopefully explicating them better. It's baffling, and I want to find a better way.
I understand the frustration of not feeling part of an engaged research community, especially after COVID many people are just severely burned out and have to somehow keep "producing". This is not the ideal environment for creative thinking atm. However, that's just not true, academia is as much about marketing (conferences, lab visits, colloquium talks, etc.) as much as it is about research. Progress just takes time, it's part of the game.
Mike Shulman (Nov 02 2022 at 18:40):One thing I think there is not enough incentive for in academia is good marketing and exposition of other people's ideas. So if someone has a good idea but they don't market it well despite whatever incentives they had (e.g. if they left academia), or if a good idea emerges as "folklore" without there being anyone whose career would benefit from marketing it, then it may struggle to get attention for longer than it deserves.
Eduardo Ochs (Nov 02 2022 at 19:09):I find your research extremely interesting, but there are many parts of it that I don't understand because I don't have the prerequisites, and I will only have time to study these prerequisites - for example, ends and coends - in my holidays...
Are you planning to do a series of blog posts and short notes? If yes, do you want suggestions on what to write about? If yes again, then here it goes... you mentioned coends and coYoneda very briefly in your Mnd.pdf. What about showing how you visualize them, and how to translate between the standard presentations and your diagrammatic language?
Christian Williams (Nov 02 2022 at 20:52):thanks! I understand. I made some notes last year for a seminar, which go to the coend calculus. the first two are messy, then they get a bit better; but overall, I will be making much better notes soon.
Logic-in-Color-2-Duality-Equipments.pdf
Logic-3-Matrices-Monads.pdf
Logic-in-Color-Monads-and-Modules.pdf
The-Language.pdf
Logic-7_-Higher-Order-Logic.pdf
Logic-in-Color_-Yoneda.pdf
Eduardo Ochs (Nov 02 2022 at 21:06):Thanks! =) =) =)
Christian Williams (Nov 02 2022 at 21:14):Georgios Bakirtzis said:
I understand the frustration of not feeling part of an engaged research community, especially after COVID many people are just severely burned out and have to somehow keep "producing". This is not the ideal environment for creative thinking atm. However, that's just not true, academia is as much about marketing (conferences, lab visits, colloquium talks, etc.) as much as it is about research. Progress just takes time, it's part of the game.
Yes, but this is not what I mean. Academia has enough marketing to sustain the academic job market, but not much more. If you impress the right people, it makes little difference whether your ideas are actually understood and utilized by the community.
What I mean is real metrics and incentives for community impact. Of course it's a difficult and complex topic, but right now there is almost nothing.
Matteo Capucci (he/him) (Nov 03 2022 at 10:15):Christian Williams said:
Academia has almost no incentive for good marketing and exposition, and I think this drastically limits progress. There are many ideas that could have reshaped the entire field decades ago, and currently it's a matter of just waiting for people to rediscover them and hopefully explicating them better. It's baffling, and I want to find a better way.
Well, maybe not directly but those things have a sizeable impact on your visibility as a researcher, and on the extent other people consider and build upon your research. So you might not get paid 'by the blog post' but in my experience networking you/your ideas pays off.
Matteo Capucci (he/him) (Nov 03 2022 at 10:17):Christian Williams said:
What I mean is real metrics and incentives for community impact.
No, please, no more metrics :cry:
Matteo Capucci (he/him) (Nov 03 2022 at 10:19):Christian Williams said:
I'm sure many people on here are having the same difficulties, not having much community for collaboration. When I came to UC Riverside 5 years ago, we had a big and vibrant research group. By the time of the pandemic, everyone was gone.
This sucks :/ my research and my life is so much better because of the group I'm in, even if sometimes our topics might feel distant. Mathematics (I'd dare to say: human life itself) is meant to be a social enterprise, not a solitary endeavour!
Matteo Capucci (he/him) (Nov 03 2022 at 10:19):That said I'm having a busy time but your talk is first on the pile :) triple categories rule! :party_ball:
Fabrizio Genovese (Nov 03 2022 at 11:17):Matteo Capucci (he/him) said:
Christian Williams said:
What I mean is real metrics and incentives for community impact.
No, please, no more metrics :cry:
I'm also strongly against metrics lol The problem is not the metrics, is too little funding and positions for too many people. This is what creates the metric craze as a way to 'decide' who's deserving and who's not. And it ends up being total BS, as always
Christian Williams (Nov 03 2022 at 15:56):I appreciate all the feedback. There's a lot to say, but mainly, I just care about bringing Category Theory to public consciousness. From what I've seen, all that academia provides toward this goal is connections to open-minded and capable people. Now that I've been making these connections, after graduating I just want to get enough money for rent and focus on writing a book.
Christian Williams (Nov 03 2022 at 16:08):If you're thinking "There's plenty of CT books, why do we need another?" - I'm happy to talk about it; but it's a lot to discuss, and easier face-to-face than online. It would be great to gather a list of people interested in developing the presentation of CT.
Christian Williams (Nov 03 2022 at 16:23):E.g. The concept of profunctor is the basic notion of relation between categories. It is fundamental to the entire subject. Yet because we usually don't draw the simple explicit picture of "a hom between two categories" (and still use the bizarre name), they are not regarded as basic. As far as I know, there isn't a CT book that gives the reader in its actual 2d form.
It doesn't have to be "advanced" at all. Just start with : of course we use both functions and relations to reason about the world. is exactly the same, just expanding 0/1 to sets of connections.
Simon Burton (Nov 03 2022 at 16:24):I don't think there's plenty of CT books. Especially if you are doing a graphical, string diagram treatment. Apparently Dan Marsden is also working on such a book...
Christian Williams (Nov 03 2022 at 16:27):Yeah, I understand. I feel like there's at least a few dozen... but certainly not plenty for people outside of math/CS. And that's great, I'd definitely like to hear about it.
Max New (Nov 03 2022 at 19:00):If you want more people to understand your work, I would suggest starting here: https://ncatlab.org/nlab/show/triple+category
Christian Williams (Nov 03 2022 at 19:32):Thanks. A lot of this discussion was based on a misunderstanding, so I need to clarify. Of course it takes time for an idea to be absorbed by the community, and I need to focus on making good content.
I was only expressing surprise and confusion that I've been openly making huge judgements about category theory, i.e. "CT has yet to be systematized as a science, and I think I've determined the language", and there was very little reaction - even skepticism; I thought surely somebody would say "what? I don't believe you, because ____".
But it seems like most people would just rather see it all written out before responding, so that's fine.
fosco (Nov 03 2022 at 20:59):But it seems like most people would just rather see it all written out before responding, so that's fine.
heh, in mathematics there are these strange contraptions called "proofs" of "theorems" used by people to avoid appearing high-sounding when claiming that they unveiled an ultimate truth about [thing X].
And sometimes not even a proof of a well-delimited statement is enough, because as they go into death, with their last breath they spit on your theorem.
Christian Williams (Nov 03 2022 at 21:07):Well this is mainly a definition, not a theorem, and it's summarized in this picture. cube-key.png
Christian Williams (Nov 03 2022 at 21:08):Yes, the hard work is proving that this forms a nice triple category; but there is no fundamental obstacle. It should be finished within a month or so.
fosco (Nov 03 2022 at 21:13):( I'm just messing with you in case you wonder, I mean no harm )
You asked for a reaction, and I want to give you an answer. I thought a lot about a similar problem, and I resolved to thinking that there are two ways to approach it (it = "a formal syntax for CT"): one is to think very long and very hard about an extremely broad and abstract issue that can be tackled from many angles, and tell this story as it deserves, XOR "waste" the problem, putting together some preliminary ideas explained as best as you can, and go on from there. No choice is right or wrong, and certainly the inability to walk the first path is due to my poor understanding of almost all the math that is contiguous to this problem. It's a bit too high for my abilities, and academia punishes people studying for years just for the sake of it.
So, I have been working on and off on this for the past few years (3 or 4, I'd say), and I have ideas I can share, but most of the time I work on this problem I don't even have an idea of statement, let alone a proof: I have a design in mind, and no infrastructure to implement it. So, following the idea that you should say few things, but let them ripe, I stay silent.
When you will make your work public, I will certainly judge it as someone who needs an answer to a Very Deep Question(TM) of theirs, and see if it provides the infrastructure I need; for the moment, I feel any comment on pictures that are not backed up by a precise statement risks being prejudicial -in the positive or negative direction.
fosco (Nov 03 2022 at 21:15):Christian Williams said:
Well this is mainly a definition, not a theorem, and it's summarized in this picture. cube-key.png
I can clearly see this cube unveils the language that will ultimately systematise category theory as a science ;-)
Christian Williams (Nov 03 2022 at 21:19):I just don't understand the need for such caution. Can't we just talk about it here? What is the "similar problem" you've been thinking about?
fosco (Nov 03 2022 at 21:24):(Again, don't get me wrong: I love to claim that this or that mathematical idea will ultimately be systematised in this or that way; but I believe that specific kind of philosophy of mathematics is best done sipping an extremely cold beer, and otherwise has little room in how we practice when sober.
For the third time: this is me and how I choose to work, and in no way a prescriptivist statement telling other people how to behave; you do you, and I think pure mathematics can profit from an attitude that is less rigid -with a grain of salt. I am young-ish, but I was educated in the old fashion, when theorems had to be proved and it wasn't enough to claim them on twitter ;-) )
fosco (Nov 03 2022 at 21:25):(I'm not talking about you, of course; I'm not talking about anyone specific.)
Christian Williams (Nov 03 2022 at 21:25):Yes, I understand.
fosco (Nov 03 2022 at 21:26):This said, the problem I'm referring to is this.
Christian Williams (Nov 03 2022 at 21:28):Yes, this is exactly what I'm doing for my thesis.
Christian Williams (Nov 03 2022 at 21:28):So I'm happy to talk about it now, or we can wait until it's all written up. I've just been doing all this alone and I would've really benefited from talking to people.
fosco (Nov 03 2022 at 21:29):I will gladly read your thesis then!
Mike Shulman (Nov 04 2022 at 01:04):Christian Williams said:
I was only expressing surprise and confusion that I've been openly making huge judgements about category theory, i.e. "CT has yet to be systematized as a science, and I think I've determined the language", and there was very little reaction - even skepticism; I thought surely somebody would say "what? I don't believe you, because ____".
Well, if you want to hear skepticism, I can oblige. As you know, I'm a big booster of double/triple categories in general, as well as of formal category theory and equipments / fibrant double categories, so I'm not going to criticize the overall premise. But I can take issue with bold claims like that this is a systematization of all of category theory.
Firstly, there are various things that your framework doesn't include yet, such as size distinctions and virtual structures (e.g. for enrichement and internalization in non-cocomplete categories). But it could presumably be enhanced to do so.
More importantly, a lot of interesting propositions and judgments (and functors) depend on more or fewer than two variables, and those that do depend on two variables may not have a clear way to distinguish one as the "domain" and one as the "codomain". So double or triple categories are a bit impoverished when it comes to systematizing logic and category theory. Which isn't to say they don't have important insights to contribute, but I'm not convinced that they are the way to systematize all of category theory.
Sociologically, I don't think making overly bold and imprecise claims is a good idea. It tends to get you branded as a crank, and the proper response to a crank is to ignore them. Better to be modest and undersell your work a little bit, and let others discover for themselves how powerful it is (assuming it is). I wasn't around for it myself, but I've been told that one reason category theory research languished for so long in the U.S. is that some of the originators of the subject had a tendency to make overly bold claims about its ability to systematize all of mathematics.
Christian Williams (Nov 04 2022 at 03:19):Thanks for the feedback; I'll respond soon. First, yes it does generalize to virtual structures and moreover the poly- version. And second, yes absolutely the compact closure is a vital aspect which can be incorporated.
Christian Williams (Nov 04 2022 at 04:11):Re: sociology, I really wish mathematicians felt more free to be loud and proud when they think they're doing something important. Yes it can be absurd and offensive when someone takes it too far, but I think the much larger reality is that everyone has a lot of self-doubt and ultimately we need to help each other believe in ourselves.
We critique and support each other as a community, and I think it works better when it can be in a spirit of friendship rather than anonymous "colleagues". You know me, of course; we've had many good meetings that I really appreciate. I think misunderstandings happen online when you don't know each other well, and I can see that some in this thread. Anyway, I really appreciate everyone's thoughts. I'll be focused on writing the preprint.
John Baez (Nov 04 2022 at 16:06):Re: sociology, I really wish mathematicians felt more free to be loud and proud when they think they're doing something important.
Personally I try to repeatedly explain what I'm doing, as clearly as I can, in many different ways in many different forums, from papers to blogs to talks to tweets. But I avoid talking about how important it is, because that just makes people resist it. There's a lot of hype in academia, and life in general, so most people have developed a kind of immune system to counter it.
I was only expressing surprise and confusion that I've been openly making huge judgements about category theory, i.e. "CT has yet to be systematized as a science, and I think I've determined the language", and there was very little reaction.
This could be an example of the immune system at work. I don't think this sort of claim invites engagement. I thought I heard a lot of eyebrows going up and eyeballs rolling.
John Baez (Nov 04 2022 at 16:08):I think if you just clearly explaining small pieces of what you're doing, people will get interested in it.
John Baez (Nov 04 2022 at 16:13):I'm quite confident that it's good stuff, btw. Probably for now you should just finish your thesis (about this stuff) and make it as nice as possible. Then you can get more serious about explaining it, and have your thesis as something to point to for people with questions. Eventually you might write a book... though books are extremely hard to write well.
Christian Williams (Nov 04 2022 at 16:38):Sorry, but I want to be done with this conversation. I was saying something completely precise and not overly bold:
If "a category theory" is a fibrant double category, then the double coend calculus of FDC is "the language of category theories".
It's not speculative or exaggerated or anything; people in this thread were making judgements before even understanding what I was saying, and it did not really feel good. I would like to move on.
Stelios Tsampas (Nov 04 2022 at 17:22):I don't know if this helps, but I've been following the resources you've shared with me and so far I've been finding this work captivating. It's a shame people found your claims bold, I didn't for once, and I haven't quite understood what's wrong with being bold anyway.
Christian Williams (Nov 04 2022 at 17:30):Thanks Stelios, I appreciate that.
John Baez (Nov 04 2022 at 17:45):I think it's incredibly important to be bold. I try to be as bold as I can be without completely falling flat on my face. And sometimes I fall flat on my face.
Christian Williams (Nov 11 2022 at 16:03):String diagrams and type theory combine to form a visual language I'm calling "color syntax". Here is the color syntax of a matrix.
mat.png mat-i.png mat-j.png mat-ij.png
Ralph Sarkis (Nov 11 2022 at 16:48):How should we understand composition of slices of matrices? I see that if we compose with we indeed get so that is nice, but what about with which looks like they should compose in your notation.
Christian Williams (Nov 11 2022 at 16:50):Let be an -matrix of data. We can reason about this matrix visually as a string connecting colors, here blue to green . Writing a specific in the blue region determines row , and writing a specific in the green region determines row . Writing both determines the entry .
Christian Williams (Nov 11 2022 at 16:50):Good question! Let me think.
Christian Williams (Nov 11 2022 at 16:53):so are and -matrices?
Ralph Sarkis (Nov 11 2022 at 16:54):It should be and .
Christian Williams (Nov 11 2022 at 16:56):okay cool (so I think you meant "compose with ").
Christian Williams (Nov 11 2022 at 16:56):yes, so you have two strings being composed, from blue to green and from green to red. composition along a particular is drawn by just writing that in the blue region.
Christian Williams (Nov 11 2022 at 16:57):I can draw both cases; should just take a minute.
Christian Williams (Nov 11 2022 at 17:03):
Christian Williams (Nov 11 2022 at 17:03):okay, let's see how to read these
Christian Williams (Nov 11 2022 at 17:05):you can read the type of the drawing by seeing what slots remain to be filled. so the first is a -vector, and the second is an -matrix.
Christian Williams (Nov 11 2022 at 17:06):maybe I should redraw it with etc. for the indices. (I was just trying to keep the initial drawings simple.)
Ralph Sarkis (Nov 11 2022 at 17:08):I am a bit confused because composition of matrices goes in the opposite direction to multiplication, and I remember from my linear algebra class that row column = scalar and column row = matrix. But the first picture is doing row;column (which is column row) and the result is a scalar (it is the opposite for the second picture).
Christian Williams (Nov 11 2022 at 17:10):oh, I am not thinking about the convention; sorry. I am just using visual intuition.
Christian Williams (Nov 11 2022 at 17:12):but you're right that so far, the picture doesn't represent composition yet, because that requires a sum over the middle variable. I think that's where the story gets interesting. so far this is just a representation of "slicing matrices".
Dylan Braithwaite (Nov 11 2022 at 17:14):You say that the the first picture, with the indices i and k depict a J-vector but I don't see how you could define a J-vector with this data. I would have assumed it to be a scalar
Christian Williams (Nov 11 2022 at 17:14):so the first picture, with filled in, is the vector whose coordinate is .
Christian Williams (Nov 11 2022 at 17:16):yes, we can choose to interpret this vector as its sum . I think that's the right way to go.
Christian Williams (Nov 11 2022 at 17:19):whereas the second picture, with just filled in, can be interpreted as "composition through "
Christian Williams (Nov 11 2022 at 17:27):So a string is a matrix , and to fill either region is to substitute into .
You are both right that the interesting aspect comes in with composition. Leaving the middle blank should be interpreted as a sum over the middle variable , while leaving the outer blank is just .
Christian Williams (Nov 11 2022 at 17:32):Does that make sense?
Dylan Braithwaite (Nov 11 2022 at 17:36):To me something seems off with putting an index in the middle. If you've already summed over an index you shouldn't be able to slice by it.
I guess this is because putting an index in a region is really composing with a conjoint/companion(?) of . So although it does work compositionally, it's doing so by factoring through the unit.
Christian Williams (Nov 11 2022 at 17:39):that's a good point. I just started making this yesterday, so we're figuring it out right now.
Christian Williams (Nov 11 2022 at 17:40):I can believe that juxtaposing two strings should always be interpreted as the composite .
Christian Williams (Nov 11 2022 at 17:41):but just to think, are there any times when you'd want to consider only a particular without the sum?
Christian Williams (Nov 11 2022 at 17:44):regardless, I think what you're saying is the right way to go. I hadn't yet made the connection to the general theory of equipments/FDCs, that substituting is composing with companions/conjoints. that's nice.
Dylan Braithwaite (Nov 11 2022 at 17:48):I stated that purely based on intuition so I'm not 100% sure that it's true. But I don't see how it could be anything else
Christian Williams (Nov 11 2022 at 17:50):yes, well I think you're right. thanks!
Christian Williams (Nov 11 2022 at 19:49):Just putting it together, for anyone interested, here is the idea as a page in the thesis-in-progress. mat.pdf
Christian Williams (Nov 11 2022 at 22:34):Thanks Dylan for the insight; now I'm seeing that it's already good to expand this "color syntax" to 3 dimensions.
The hom of a double category is a matrix of categories: for each pair we have a category of "loose morphisms" . In color syntax, we can determine such a category, and even an object therein.
Yet in the above drawing, we can only see an object of that category, not yet a morphism. How can we see the "beads", the 2-morphisms between loose morphisms? By going into dimension 3, as follows.
(ignore the insulation; I have a whiteboard in the garage)
Christian Williams (Nov 11 2022 at 22:37):The "beads" are revealed as a very simple cube in MatCat: the inner category is the terminal category , and the outward functors are picking out objects and . cube-key.png
then denotes the category whose objects are matrix functors framed by , and morphisms are matrix transformations.
Christian Williams (Nov 11 2022 at 22:58):I think we can in general interpret the white inside a bead as such a hom from 1.
Christian Williams (Nov 11 2022 at 23:58):Here is a more accurate picture.
The inner category is 1, just white. The outward functors pick out . The black square is the unit of the hom of 1, picking out the identity of , which is transformed into and .
Then the cube can be interpreted as the category in which: an object is a matrix functor (a black triangle), and a morphism is a matrix transformation (a cube of this form), i.e. we can interpret this general cube as the category of cubes of this form.
Christian Williams (Nov 12 2022 at 00:28):This is just --- but now we can see the beads: this 3d string diagram is now a formal template to specify hom-sets of the category . 1-hom-mat.png 1-hom-i.png
Christian Williams (Nov 12 2022 at 01:28):I think we can even interpret the above cube (1-hom-mat) as the fibered isomorphism .
This is a bead generator! On any matrix-category string (any horizontal profunctor of fdc's, including the identity hom above), this isomorphism generates beads.
A core aspect of each part of the Mnd(-) construction is naturality with respect to these beads, i.e. they can "flow freely".
Christian Williams (Nov 12 2022 at 01:43):But anyway, I'd just like to know what anyone thinks about using this string-matrix notation to represent hom-categories.
Morgan Rogers (he/him) (Nov 12 2022 at 08:47):What is in the last drawing?
And in your earlier drawings, what's the distinction between and ? If I understood correctly, is an object of the hom category; is something different? If so, how am I supposed to know?
Christian Williams (Nov 12 2022 at 17:48):is the whole matrix of categories (the over as a fibrant double category)
Christian Williams (Nov 12 2022 at 17:49):is a loose morphism
Christian Williams (Nov 12 2022 at 17:49):and is a 2-morphism
Christian Williams (Nov 12 2022 at 17:52):okay, I think you raise a good point. how to tell when the writing on the wire is a matrix entry vs an element of it
Christian Williams (Nov 12 2022 at 17:54):right now I've been just using font and color, the hom-category is black bold and the specific loose morphism is blue and whatever the font should be for profunctors.
Christian Williams (Nov 12 2022 at 18:29):I think a string is the simplest possible visual representation of a matrix. Category theory stores its data in matrices: is a matrix of hom-categories, and an object therein is a profunctor, which is a matrix of sets, etc.
So there's this visual "cosmic principle" where we can use the same simple string to "zoom in" all the way from a whole double category to an individual heteromorphism of a profunctor.
Christian Williams (Nov 12 2022 at 18:31):So you're right, there just needs to be clear distinction between the levels.
Christian Williams (Nov 12 2022 at 18:35):this is just a first sketch; I'm sure it can be improved. mat-zoom.png
Christian Williams (Nov 12 2022 at 19:21):okay, take two. I think it's more reasonable to just display all the information. mat-zoom2.png
Christian Williams (Nov 12 2022 at 19:24):(1) (2) (3) (4) (5) .
Christian Williams (Mar 02 2023 at 18:08):A two-sided fibration is (equivalent to) a "Cat-profunctor", a pseudofunctor . These have been considered as the morphisms of a tricategory, but is actually a triple category.
In a "category theory", a double category of categories, there are hom-sets of functors and hom-categories of profunctors. To generalize this to a language of all double categories, profunctors provide the "hom-sets" and two-sided fibrations provide the "hom-categories" between double categories.
But how do "set-profunctors" and "cat-profunctors" fit together? --- What is a "profunctor of two-sided fibrations"? The answer is ideal, by the following theorem.
Christian Williams (Mar 02 2023 at 18:09):Let and be two-sided fibrations, and let and be profunctors. Let be a profunctor with transformations to and , i.e. an arbitrary span of profunctors from to .
Then the induced span of discrete two-sided fibrations is a two-sided fibration.
Christian Williams (Mar 02 2023 at 18:09):
Christian Williams (Mar 02 2023 at 18:10):Let lie over . Consider a "precomposite" commutative square in , and a "postcomposite" commutative square in .
Christian Williams (Mar 02 2023 at 18:15):"pulling back" along cartesian morphisms and is functorial, giving a commutative square over that of ; and similarly, "pushing forward" by the opcartesian morphisms of and gives a commutative square over that of .
Christian Williams (Mar 02 2023 at 18:17):This characterizes as a discrete two-sided fibration .
Christian Williams (Mar 02 2023 at 18:19):This means that arbitrary profunctors of two-sided fibrations are as well-behaved as we could possibly want. So, the above can be understood as a "coherence theorem" for defining the triple category of functors, set-profunctors, and cat-profunctors.
Christian Williams (Mar 02 2023 at 20:46):One could argue that this means: is really a triple category! There are two monad constructions, a "small one" of ordinary bimodules (profunctors), and a "big one" of arrow-category bimodules (two-sided fibrations). The theorem says that they fit together.
Matteo Capucci (he/him) (Mar 02 2023 at 20:48):What do you mean by 'monad construction'?
Christian Williams (Mar 02 2023 at 20:50):forming monads and bimodules in a double category
Matteo Capucci (he/him) (Mar 02 2023 at 20:51):This is quite nice... I was writing a long blog post on how fibrations are much more similar to modules than one would expect, including having a tensor, hom, etc, and I was wondering whether people already studied the equipment (?) of two-sided fibrations and.. what? I didn't get that far because the blog post got lost
Christian Williams (Mar 02 2023 at 20:52):Street did some, but yeah I haven't seen much about TSFib. They really are just "boosted" bimodules.
Nathanael Arkor (Mar 02 2023 at 20:55):Christian Williams said:
One could argue that this means: is really a triple category! There are two monad constructions, a "small one" of ordinary bimodules (profunctors), and a "big one" of arrow-category bimodules (two-sided fibrations). The theorem says that they fit together.
There's also a triple category of double categories, if I remember correctly: does your triple category relate to this one somehow (e.g. by considering every category to be a trivial double category)?
Christian Williams (Mar 02 2023 at 20:57):the triple category of double categories is made from this one.
Christian Williams (Mar 02 2023 at 20:59):We take "half" of TSFib, say Opf, as a double fibration over Cat. Then pull back along the product of Cat, to form the triple category Mat(Opf) over Cat^2. Then form pseudomonads.
Christian Williams (Mar 02 2023 at 21:03):Matteo Capucci (he/him) said:
This is quite nice...
isn't that theorem amazing? so simple yet so powerful.
Christian Williams (Mar 02 2023 at 21:04):if I'd explored the question "what is a profunctor of fibrations" more systematically, I could've found this and saved myself many months of wandering in confusion; but so it goes.
Nathanael Arkor (Mar 02 2023 at 21:04):So you're saying that to form the triple category of double categories involves the process of taking a triple category of monads twice? (Once ordinary monads for Opfib, and once pseudomonads for DblCat.)
Christian Williams (Mar 02 2023 at 21:05):yes, first you need the language of op/fibrations, which is really that of two-sided fibrations, which are bimodules.
Nathanael Arkor (Mar 02 2023 at 21:06):What are pseudomonads in Mat(TSFib)?
Nathanael Arkor (Mar 02 2023 at 21:06):(If you've thought about that.)
Christian Williams (Mar 02 2023 at 21:06):here's a brief write-up theorem.pdf
Christian Williams (Mar 02 2023 at 21:06):you mean pseudomonads in TSFib?
Christian Williams (Mar 02 2023 at 21:07):pseudomonads in TSFib are double categories with companions.
Christian Williams (Mar 02 2023 at 21:07):(or conjoints, depending on your direction).
Christian Williams (Mar 02 2023 at 21:07):that's the only "limitation" of two-sided fibrations; they only "point one direction".
Nathanael Arkor (Mar 02 2023 at 21:08):Christian Williams said:
We take "half" of TSFib, say Opf, as a double fibration over Cat. Then pull back along the product of Cat, to form the triple category Mat(Opf) over Cat^2. Then form pseudomonads.
Here, you were taking pseudomonads in Mat(Opfib), right? And these were double categories. So I was wondering what happened if you didn't restrict to the opfibrations.
Christian Williams (Mar 02 2023 at 21:09):Mat(-) is a construction on fibrations; in this case Cat(Mat) is a construction on double fibrations. TSFib is a double fibration but it's already over a product Cat x Cat; I don't know what it would mean to apply Mat(-) but I expect it's redundant.
Christian Williams (Mar 02 2023 at 21:10):that's why you take just "half", Opf over Cat, then "matrize" it.
Christian Williams (Mar 02 2023 at 21:11):the main theorem going on here is Thm 4.1 of framed bicategories.
Nathanael Arkor (Mar 02 2023 at 21:12):Ah, right, I see, thanks.
Christian Williams (Mar 02 2023 at 21:13):A double category is a fibration iff it is an opfibration; these give all four of the "bends" of vertical morphisms into horizontal ones.
Nathanael Arkor (Mar 02 2023 at 21:13):Seems like a pretty construction! Looking forward to reading all the details when your thesis is ready :)
Christian Williams (Mar 02 2023 at 21:13):It's strictly stronger than saying is a two-sided fibration, because that just gives companions.
Christian Williams (Mar 02 2023 at 21:14):thanks! yeah, hopefully a draft by April.
Christian Williams (Mar 03 2023 at 05:38):here is the idea, with and without labels for the proof:
polthm-0-lbl.png polthm-1-lbl.png
polthm-diag.png
Christian Williams (Mar 03 2023 at 05:42):For any two-sided fibrations and , and profunctors and , we have that every span of profunctors has a natural action by and .
Christian Williams (Mar 10 2023 at 23:43):Correction: the above theorem is not true; thanks to Shulman for catching it. The "intuitive" composite squares and do not necessarily exist as elements of . For any span of profunctors between two-sided fibrations, a bimodule structure is essentially unique if one exists, but it need not (just like two-sided fibrations themselves).
Christian Williams (Mar 10 2023 at 23:46):I naively interpreted the string diagram as a construction, but "juxtaposition as composition" assumes that such a composition operation exists. You have to remember that when using the visual language.
Christian Williams (Mar 10 2023 at 23:48):Any way, the conjecture was far too strong, and it's not necessary. The basic idea is that the construction of two-sided fibrations extends from spans of functors to spans of profunctors, i.e. Span(Cat) as not just a double category but a triple category.
Christian Williams (Mar 10 2023 at 23:52):The point is that "Cat is really a triple category", where the third dimension is two-sided fibrations.
Matteo Capucci (he/him) (Mar 11 2023 at 08:33):So functors (transversal), profunctors aka 'discrete bimodules' (horizontal) and two-sided fibrations aka 'bimodules' (vertical)..?
Matteo Capucci (he/him) (Mar 11 2023 at 08:33):This is not Span(Cat) though, right? And is this chiral or not?
Christian Williams (Mar 11 2023 at 16:15):profunctors vertical, as they carry "sets of processes" between types, and two-sided fibrations horizontal, as they carry "categories of relations and inferences".
Christian Williams (Mar 11 2023 at 16:17):no, I meant that it is formed in/from Span(Cat)
Christian Williams (Mar 11 2023 at 16:17):what do you mean by chiral?
John Baez (Mar 11 2023 at 17:28):He means what you call "polarized". Jargon, jargon.... it just means you can't flip some kinds of arrows around, left is different from right.
Christian Williams (Mar 11 2023 at 19:48):Ah, yeah. TSFib is compact closed, but not self-dual compact closed, just like Cat.
Matteo Capucci (he/him) (Mar 11 2023 at 21:47):John Baez said:
He means what you call "polarized". Jargon, jargon.... it just means you can't flip some kinds of arrows around, left is different from right.
Mmh not sure it's the same meaning I use. Grandis and Parè call 'intercategories' also 'chiral triple categories' (a terminology I now favour). See here. Span(Cat) is a chiral triple category FYI.
Matteo Capucci (he/him) (Mar 11 2023 at 21:47):Christian Williams said:
no, I meant that it is formed in/from Span(Cat)
How? :thinking:
Christian Williams (Mar 11 2023 at 22:07):oh, no TSFib is definitely more strict that Span(Cat); I think the interchange is an iso, not lax.
Christian Williams (Mar 11 2023 at 22:09):Matteo Capucci (he/him) said:
Christian Williams said:
no, I meant that it is formed in/from Span(Cat)
How? :thinking:
TSFib is monads and modules in Span(Cat), but restricted to arrow categories.
Matteo Capucci (he/him) (Mar 11 2023 at 22:32):But a monad in Span(cat) would give a double category, not a category. I though the objects of TSFib were categories?
Christian Williams (Mar 12 2023 at 01:00):The objects of TSFib are arrow categories, which are canonically double categories.
John Baez (Mar 12 2023 at 01:46):Matteo Capucci (he/him) said:
John Baez said:
He means what you call "polarized". Jargon, jargon.... it just means you can't flip some kinds of arrows around, left is different from right.
Mmh not sure it's the same meaning I use. Grandis and Parè call 'intercategories' also 'chiral triple categories' (a terminology I now favour). See here. Span(Cat) is a chiral triple category FYI.
Oh, wow. Okay, so I have no idea why those are called 'chiral'. (I have also never understood intercategories, in part because I've never tried to.)
Matteo Capucci (he/him) (Mar 12 2023 at 17:11):What distinguishes a 'left-handed' triple category from a 'right-handed' one is the direction of the interchanger, which is now non-invertible. And there is a mirror-like symmetry going on since taking transversal opposites changes chirality, and the transversal opposite (I think) gives you the triple category which you see by holding up a mirror in front of the original one.
Matteo Capucci (he/him) (Mar 12 2023 at 17:14):Christian Williams said:
profunctors vertical, as they carry "sets of processes" between types, and two-sided fibrations horizontal, as they carry "categories of relations and inferences".
In double categories, vertical and horizontal have different roles, one direction is 'loose' and the other is 'tight'. In triple (and multiple) categories it seems to me the only distinguished direction is the transversal one, being tight, while the other ones are all equally loose.
So I'm curious, here you seem to hint at an attitude you see in being vertical or horizontal in a triple category. Is it just a convention of yours or is there a mathematical difference I didn't notice before?
Christian Williams (Mar 12 2023 at 22:57):[Conjecture, mostly checked]
The triple category Cat is TV- and TH-bifibrant: functors induce adjoint profunctors, and functors induce adjoint two-sided fibrations. But moreover, dimension VH is a two-sided fibration: a profunctor induces a companion two-sided fibration. (The conjoint just doesn't type-check.)
But we get both by completing Cat to form logics:
the triple category of bifibrant double categories is bifibrant T > V > H.
Christian Williams (Mar 13 2023 at 17:39):So Matteo, it sounds like you've been thinking about more "loose" triple categories, but Cat and BDC are very well-structured.
Seeing a bifibrant double category as a logic, a tight morphism is a "process" and a loose morphism is a "relation". The former induces a dual pair of the latter.
In the same way, a vertical profunctor of BDCs is a "metaprocess" and a horizontal profunctor is a "metarelation" --- and (I'm working on proving that) the former induces a dual pair of the latter.
Matteo Capucci (he/him) (Mar 13 2023 at 17:58):What is a BDC?
Christian Williams (Mar 13 2023 at 18:06):bifibrant double category. equipment, framed bicategory. the only thing I ever talk about :moon_face:
John Baez (Mar 13 2023 at 18:14):Acronyms are evil.
John Baez (Mar 13 2023 at 18:15):I bet Matteo would have understood "equipment".
Dylan Braithwaite (Mar 13 2023 at 18:19):If that's a bifibrant double category, what's a merely fibrant one?
Christian Williams (Mar 13 2023 at 18:21):is a fibration iff it's an opfibration; Thm 4.1 framed bicategories
Christian Williams (Mar 13 2023 at 18:23):The cartesian morphism over or is the "upward bend" of a companion or conjoint, and factorization of through it gives the "downward" opcartesian; dually for the converse.
Matteo Capucci (he/him) (Mar 13 2023 at 20:32):John Baez said:
I bet Matteo would have understood "equipment".
Or literally any other name for these things :laughing: there's no shortage. But this is the first time I hear bifibrant, where does that come from?
Matteo Capucci (he/him) (Mar 13 2023 at 20:32):Dylan Braithwaite said:
If that's a bifibrant double category, what's a merely fibrant one?
Which is probably what Dylan asked here.
Christian Williams (Mar 13 2023 at 21:25):I just said. A double category is fibrant if and only if it's opfibrant.
Nathanael Arkor (Mar 13 2023 at 21:52):I think perhaps a different way of phrasing the question is: why introduce new terminology "bifibrant double category" when the terminology "fibrant double category" is already in use, and is not ambiguous (as far as I'm aware)?
John Baez (Mar 13 2023 at 22:04):There aren't enough names for equipments yet.
Morgan Rogers (he/him) (Mar 13 2023 at 22:12):We aren't yet fully equipped
Christian Williams (Mar 13 2023 at 23:07):yes. I'm just that wild and crazy, adding two letters to remind people of an important duality theorem.
Mike Shulman (Mar 14 2023 at 05:43):For what it's worth, there are in principle many things that could be meant by "fibrant double category". After all, in general a "fibrant X" means an object of the category of Xs such that the map is a fibration, usually in some Quillen model structure, and there are many different Quillen model structures on the category of double categories. However, when not discussing any model structure, it does seem now to be fairly common for "fibrant double category" to mean this thing.
Matteo Capucci (he/him) (Mar 14 2023 at 09:04):Christian Williams said:
yes. I'm just that wild and crazy, adding two letters to remind people of an important duality theorem.
It's not crazy but don't act surprised when we don't know what you mean! Usually biX and X are different concepts in mathematics, category theory especially.
Matteo Capucci (he/him) (Mar 14 2023 at 09:05):Also equipments have so many names already it's very easy for us to roll our eyes at yet another name...
Christian Williams (Mar 23 2023 at 18:21):Here's an abstract I'm submitting: The triple category of categories
Christian Williams (Mar 23 2023 at 23:29):Being a fibration is a property-like structure, as in "you either got it or you don't, no two ways about it". Normally I've understood this idea abstractly, boiling down to a canonical isomorphism between any two cartesian lifts.
But I've been meditating on a "concrete", intuitive interpretation: the elements of a two-sided fibration really are the loose morphisms in the collage double-category-with-companions, and the actions really are composition of squares. It's "the canonical" representation of any two sided-fibration, given by the universality of collage. The "fundamental" cartesian action is precomposition, and opcartesian is postcomposition.
This gives a visual language where a string is a two-sided fibration, a matrix of categories.
fibprof-nat1.png
Bryce Clarke (Mar 26 2023 at 20:13):Christian Williams said:
Here's an abstract I'm submitting: The triple category of categories
I'm assuming you are submitting to CT2023?
Bryce Clarke (Mar 26 2023 at 20:15):All the best with your submission; I hope it gets accepted! The conference is a fantastic place to get feedback and interact with many amazing mathematicians, it would be great to see you there.
Matteo Capucci (he/him) (Mar 27 2023 at 14:34):Ditto! Along with (but separated from) all those amazing mathematicians, there'll be also me :)
John Baez (Mar 27 2023 at 23:38):Yes, he's submitting it to CT2023.
I hope Christian gets a chance to talk to many amazing mathematicians and also many amazed mathematicians.
Christian Williams (Oct 09 2023 at 16:53):Here is a summary of my thesis: The-Metalanguage-of-CT.pdf
Christian Williams (Oct 09 2023 at 16:54):The first two pages are the idea that category theory is logic, and can be presented via co/end calculus and string diagrams.
Christian Williams (Oct 09 2023 at 16:56):The fundamental concepts of category theory are systematized in the language of a bifibrant double category, also known as a "proarrow equipment" or "framed bicategory". I propose that such a language can be understood simply as a logic.
Christian Williams (Oct 09 2023 at 16:58):My dissertation is the metalanguage of logics, i.e. the "triple category" of bifibrant double categories, in the forms of both 3D string diagrams and the co/descent calculus.
Christian Williams (Oct 09 2023 at 17:02):Ultimately, I just want to find collaborators. So please let me know any thoughts, and we can discuss.
Christian Williams (Oct 09 2023 at 17:03):I also have the slides from my defense: Logic-in-color.pdf (and the video, though it is fairly rough, if anyone wants it).
Christian Williams (Oct 09 2023 at 17:05):(And of course, the actual dissertation. Because of various circumstances, the document is still very rough. But it has the essential definitions and theorems; so if you don't mind a rough draft then I can send it by private message.)
Christian Williams (Oct 09 2023 at 17:14):Any way, thanks for reading! I'm happy to provide more information. Looking forward to hearing your thoughts.
Christian Williams (Oct 09 2023 at 18:40):Ah, there's a typo. "Logics form a metalogic: morphisms are double functors, vertical profunctors, and horizontal profunctors;"
Because it's very concise, many parts could use some clarification. So we can just discuss here, or by message.
Christian Williams (Oct 09 2023 at 18:41):The main point is, my thesis proposes: Logic is 2D, and Metalogic is 3D.
2d.png
3d.png
Kevin Arlin (Oct 09 2023 at 20:35):I'm not sure if I missed it, but what exactly is the kind of triple category you're using for metalogics?
Christian Williams (Oct 09 2023 at 20:43):Yes, it's a kind of three-dimensional category that I'm calling a "metalogic". It is essentially a "bifibrant triple category without interchange".
Christian Williams (Oct 09 2023 at 20:43):There are two kinds of profunctors between bifibrant double categories, vertical and horizontal. A double profunctor (the VH face) is a bimodule of vertical profunctors, from one horizontal profunctor to another. As it turns out, horizontal composition of double profunctors does not preserve vertical composition, because each involves a colimit that the other cannot represent.
Christian Williams (Oct 09 2023 at 20:47):This is a general phenomenon for any instance of the 3D pseudomonad construction - with two dimensions of bimodules, there is an obstruction to interchange. So I gave it the name "metalogic", because this is just a fact, rather than some particular deficiency.
Christian Williams (Oct 09 2023 at 21:00):Just as the elements of a profunctor are morphisms of a category, via collage, the objects of a horizontal profunctor are the loose morphisms of a bifibrant double category. Similarly, the elements of a double profunctor are the squares of a double category. Hence the obstructions to interchange can be drawn as follows.
Because horizontal composition adjoins associator isomorphisms, there are composites with these in the vertical-of-horizontal composite matrix profunctor which cannot be represented in the horizontal-of-vertical composite. So it is not lax.
On the other hand, vertical composition is profunctor composition, which involves a quotient - so there are composites in the horizontal-of-vertical composite matrix profunctor which would require a choice of zig-zag witnessing that two pairs are equal up to associativity; yet each choice gives a different result, so it is not well-defined. So it is not colax.
Hence horizontal composition is neither lax nor colax with respect to vertical composition. I believe this is a basic limitation of metalogic.
Christian Williams (Oct 09 2023 at 21:27):Well, not exactly a "limitation". Perhaps more accurate to say this is a basic "complexity" of metalogic.
Christian Williams (Oct 17 2023 at 04:23):I'm preparing my thesis for arXiv, and I thought it would be good to share it in bite-size parts. So I just posted to LocalCharts, the forum that @Owen Lynch set up - the site is really well-designed, highly recommend.
Matrices of Categories, in 3D String Diagrams
This is a brief introduction to 3-dimensional string diagrams, as a language for dependent category theory. I'll be adding more tomorrow, and hanging around here for any discussion. Thanks!
Christian Williams (Oct 30 2023 at 16:08):This weekend at Octoberfest, I presented my thesis:
Here are the slides: Metalogic-in-3D.pdf
Here is the recording: https://richardblute.files.wordpress.com/2023/10/williams-oct23.mp4
Christian Williams (Oct 30 2023 at 16:23):And finally, the document is now complete enough to share:
https://sites.google.com/view/logic-in-color/