Category Theory
Zulip Server
Archive

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

Stream: community: general

Topic: wiki: Color Logic

Christian Williams (Nov 08 2023 at 16:11):

I'm starting a wiki: color-logic.io

Jean-Baptiste Vienney (Nov 08 2023 at 16:12):

Cool! :tada:

Christian Williams (Nov 08 2023 at 16:16):

Thanks! Right now it has Metalogic; I just transcribed my thesis, but now it's more interlinked and easy to navigate.

Christian Williams (Nov 08 2023 at 16:22):

• Logic is a way to learn the language of categories in three parts, starting at any age: Binary Logic, Matrix Logic, Active Logic. (Matrix & Active Logic are Sections 14 and 15 of Framed Bicategories)

• Metalogic is the 3D language of bifibrant double categories, a.k.a. proarrow equipments / framed bicategories.

• Research is for laying out a plan to systematize (much of) category theory in this 3D language.

• Development is for growing Color Logic as an education and research program.

Christian Williams (Nov 08 2023 at 16:24):

It's a big program, so I am looking forward to collaborating. If you're interested, let me know.

Christian Williams (Nov 08 2023 at 16:28):

There should be a research seminar; but first there needs to be a draft of Logic, because that's what to show people when developing the project (like rich tech people in the Bay Area who want to understand CT, for example).

Christian Williams (Nov 08 2023 at 16:30):

The wiki was just made over the last week, so please let me know of things to be fixed or improved.

David Egolf (Nov 08 2023 at 17:22):

This looks really cool! I know only a few things about logic (and I wish I knew more), and so I'm especially intrigued by your section "Logic", which you mention as potentially being accessible to those of "any age".

It took me a long time to notice the "Binary logic", "Matrix logic" and "Active logic" links on the "Logic" page, by the way. And I think I would have failed to notice them entirely if I wasn't looking for those headings because of your post here on zulip!

I'm not sure how those could be made more obvious to the reader. I guess I didn't expect having to click to a different page to get to the most basic things, once I landed on the "Logic" page. Instead, I started scrolling down after landing on the "Logic" page and immediately encountered "bifibrant double categories", which didn't feel as introductory as I had hoped for!

Christian Williams (Nov 08 2023 at 17:26):

Thanks! Yes, I haven't made Logic yet, but I just finished a first draft of Metalogic and so I'm starting Logic today. I know that's what most people will care about.

David Egolf (Nov 08 2023 at 17:43):

I look forward to seeing how this develops!

I skimmed what's already there in the "Logic" section, and I found it quite interesting. I've recently been reflecting a bit on the idea that in a lot of categories morphisms are like a way of moving from one object to another (through some kind of geometric space, or in terms of logical reasoning), or a process that adjusts one object into another, or a process that transforms one part of a source object into a part of the target object.

So when you say things like "A world is a category of types of things, and processes between types.", it sounds interesting and exciting to me!

Christian Williams (Nov 08 2023 at 18:13):

(To navigate, use the top left bar: "Color Logic / Metalogic / Span categories / ...". If you press "back page", it asks you to log in to Notion.) (and if you've never used Notion, highly recommend. It's been amazingly easy to start building this wiki.)

Ralph Sarkis (Nov 09 2023 at 10:23):

Excited to see this wiki grow!

Ralph Sarkis (Nov 09 2023 at 10:23):

Technical problem: On both my phone and laptop, when I try to go back to the home page with my browser's back button, it loads a page that asks me to sign up. I think when I click on your link above, it loads this link instead and then changes window.location for it to simply be "color-logic.io", but when I use the back button with my browser, it probably does not remember that longer link and tries to load "color-logic.io" which apparently needs me to sign up.

Matteo Capucci (he/him) (Nov 10 2023 at 11:12):

Excited to see this, Christian!

Currently I have a hard time reading through you wrote because I don't intuitively see the correspondence between the usual syntax and the graphical syntax. Perhaps it's already in the plan of the work, but I suggest you have a page to explain that. Also it helps to have symbols and names that anchors what you say in the text to what I see in the diagram.

Christian Williams (Nov 10 2023 at 16:25):

Thanks! What part are you reading? Span Categories walks through the correspondence.

Christian Williams (Nov 12 2023 at 20:07):

Horizontal morphisms of a double category form a span of categories.
Squares of a double category form a span of profunctors.

So, we can visualize a span of categories $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ as a "string",
and a span of profunctors $f\Leftarrow i\Rightarrow g$ as a "bead".
1.png
span-prof.png

Christian Williams (Nov 12 2023 at 20:11):

Then, a span of transformations can be understood as a mapping of squares.
This can be drawn as a "cube", which we can read as:
an inner square of $i_0$ becomes an outer square of $i_1$.

span-trans-dia.png
span-trans.png

Christian Williams (Nov 12 2023 at 20:12):

So, a cube just means: an inner square becomes an outer square.

Ralph Sarkis (Nov 12 2023 at 20:17):

Why are the first two levels "undirected", but third one is not ?

Christian Williams (Nov 12 2023 at 20:18):

Well, the first two levels are "relations" between double categories, because they are just the "containers" for horizontal morphisms and squares. Then the third dimension is transformations of these elements.

Christian Williams (Nov 12 2023 at 20:22):

The language is laid out in Span categories, and I'd really appreciate any feedback. I'm happy to answer any questions and discuss.

Todd Trimble (Nov 12 2023 at 20:39):

Christian Williams said:

Horizontal morphisms of a double category form a span of categories.
Squares of a double category form a span of profunctors.

So, we can visualize a span of categories $\mathbb{A}\leftarrow \mathcal{R}\to \mathbb{B}$ as a "string",
and a span of profunctors $f\Leftarrow i\Rightarrow g$ as a "bead".
1.png
span-prof.png

I'm confused; to me it sounds like you might have said that backwards. That is, I would expect to hear something like "Spans of categories form the horizontal arrows of a [certain] double category [we will be discussing]", whereas it reads "Horizontal morphisms of a[ny] double category form a span of categories", which I'm not quite following the sense of.

Christian Williams (Nov 12 2023 at 20:42):

A double category $\mathbb{C}$ is a span of categories $\mathsf{ob}\mathbb{C}\leftarrow \mathsf{hmor}\mathbb{C}\to \mathsf{ob}\mathbb{C}$.

Christian Williams (Nov 12 2023 at 20:53):

hello? Ralph or Todd, I'm happy to have a conversation. but if the questions are cleared up, then fine.

Todd Trimble (Nov 12 2023 at 20:58):

Oh, very sorry, duh.

Christian Williams (Nov 12 2023 at 20:59):

no, all good!

Ralph Sarkis (Nov 12 2023 at 21:06):

Sorry, it will take me some more time to read (it's late here)

Christian Williams (Nov 12 2023 at 21:08):

sure, no problem.

Evan Washington (Nov 12 2023 at 22:50):

re: "matrix logic," these sorts of logics seem very familiar to me: e.g. $\mathsf{Set}$-valued logics look like the logic of possible world semantics (where we replace whether a proposition is true with a subset of ways it can be true), $\mathbb{V}$-valued logics (say, for a quantale) look like some flavors of many-valued logic. it would be really neat if this were the case! is this the kind of idea you're indicating / do you have ideas on sketching it out in more detail?

Christian Williams (Nov 13 2023 at 00:57):

Absolutely, I think that's the key idea: relations can be valued in any logic.

Christian Williams (Nov 13 2023 at 01:28):

As far as "sketching it out in more detail", there is so much to do, and I've barely started. I've been working on Metalogic the past two years, and now the bridge needed is the story of Logic - but this project is much harder because it's meant for a general audience, so it needs to be filled with examples and intuition and perspectives. This really is not a task for one person, so... this month I'm sketching an overview, so people can see the project as a whole. But I think the sooner this is collaborative, the better it will be in the long run. So I'll be working to lay it out, but this project is open to anyone.

Jason Erbele (Nov 13 2023 at 06:48):

I'm trying to parse the non-color diagram, span-trans-dia.png, and I can't work out what the middle column of arrows is doing. I'm pretty sure my guess that the arrow from $i_0$ to $i_1$ is a 3-arrow and not a 2-arrow is on the mark, but I'm not even sure of how many 1-arrows there are in that column – I cannot tell whether there are 1-arrows from $\mathcal{Q}_0$ to $\mathcal{Q}_1$ and from $\mathcal{R}_0$ to $\mathcal{R}_1$; I don't think there would be a 1-arrow from $i_0$ to $\mathcal{Q}_1$, but apparently there is one from $i_1$ to $\mathcal{R}_0$ that I was not expecting, so I'm not so sure.

I think it would be a clearer diagram if a bit of a horizontal offset is given between the 0-layer and the 1-layer (in that column, at least), much like the vertical offset you already have for the 2-arrows.

Christian Williams (Nov 13 2023 at 15:46):

Sure, we're drawing a span of categories as a "string", and a span of profunctors as a "bead":
span-prof.png
span-prof-string.png

Christian Williams (Nov 13 2023 at 15:49):

I think the main thing to get used to is viewing the transformations from $i$ to $f$ and $g$ as the connections of the bead to the left and right strings. But it's analogous to viewing the span of categories as a string.

Christian Williams (Nov 13 2023 at 15:50):

Then a span transformation is drawn as a "bead within a bead". In the conventional diagram, I put the two span profunctors on top of each other, so that the two images are exactly dual.
span-trans-dia.png
span-trans.png

Christian Williams (Nov 13 2023 at 15:52):

So the back face of the cube is the source span profunctor $i_0$, and the front face is $i_1$ ("hollowed out" so we can see through it).

Christian Williams (Nov 13 2023 at 15:53):

The top and bottom black beads are spans of functors, and the left and right black beads are transformations. Those are the two kind of 2-morphisms besides spans of profunctors.

Christian Williams (Nov 13 2023 at 15:54):

Then yes, you're right - that middle $i_0\Rightarrow i_1$ is the span of transformations, which is the 3-morphism that "fills the cube".

Christian Williams (Nov 13 2023 at 16:38):

And as said above, because a span of profunctors can be understood as containing squares of a double category, the cube (span of transformations) can be understood as "an inner square becomes an outer square".

If the string diagrams make sense, or at least the 2D one, can you put a thumbs-up?
It'd just help to know; thanks. (And if not, we can talk about it.)

Evan Washington (Nov 13 2023 at 21:07):

a question on the Logic page. I'm having trouble parsing the diagrams for the coend/existential and end/universal. maybe that's because I don't quite understand the meaning of the annotations, $(r \cdot b, s) = (r, b \cdot s)$ and $[\![\mathrm{x}\cdot p\cdot \mathrm{y}]\!] = \mathrm{x}\cdot [\![p]\!]\cdot \mathrm{y}$.(Should that last $p$ be a $q$? What do the comma $(-,-)$ and double brackets mean?)

Christian Williams (Nov 13 2023 at 21:13):

Yeah, they aren't really explained yet.

A composite profunctor $R\circ S$ consists of pairs $(r,s)$, quotiented by the "associativity relation" that for every morphism $b$ of the middle category $(r\cdot \mathrm{b}, s) = (r, \mathrm{b}\cdot s)$.

That's drawn as "swinging the action of B from R to S".
bilin-l.png
bilin-r.png

Christian Williams (Nov 13 2023 at 21:15):

The double brackets is a transformation $[\![-]\!]: P\Rightarrow Q$. (I know some people won't like that notation; it's just what I've used in Metalogic to reduce the number of symbols.)

Then a transformation satisfies the "naturality" equation that for every pair of morphisms in $\mathrm{X}$ and $\mathrm{Y}$, $[\![\mathrm{x}\cdot p\cdot \mathrm{y}]\!] = \mathrm{x}\cdot [\![p]\!]\cdot \mathrm{y}$, i.e. the mapping commutes with the actions.

That's drawn as "sliding the actions of X and Y through the mapping".
nat-s.png
nat-t.png

Christian Williams (Nov 13 2023 at 21:53):

(Unfortunately the current images do not look right in "dark mode" on zulip and elsewhere; but they're fine in "light mode".)

Jason Erbele (Nov 14 2023 at 05:09):

Honestly, I have not understood what's going on with your string diagrams except in the vaguest sense. I suspect that's because I'm not entirely sure what a profunctor is, so building things from them is going to be an uphill battle. I would like to understand what's going on, but I'm already stretched pretty thin and won't have time to spend on it for at least a month. So for now, all I can do is call out blatant ambiguities.

Jason Erbele (Nov 14 2023 at 05:10):

On that note, after looking at the 2D arrow diagram and thinking about it for a while, I was finally able to figure out what was going on in the 3D arrow diagram. That said, I still maintain that if you are going to present that 3D arrow diagram, the front and back of the middle column should have some horizontal separation to make it read less ambiguously. As is, several arrows share stems, which is bad for clarity.

Barton Rhodes (Dec 10 2023 at 22:25):

AF596606-E88B-4358-90A4-69E3861507ED.jpg can color logic help implement / illustrate these operations more intuitively?

Christian Williams (Dec 10 2023 at 23:55):

Hi! Well, do you know how the operations could be defined categorically?