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: learning: questions

Topic: Peirce, logic and the categories


view this post on Zulip David Corfield (Jan 21 2025 at 13:03):

Just to record some observations, but I'd be grateful for any thoughts on these.

The American philosopher Charles Peirce has received some attention in the CT community for his string-diagrammatic approach to logic, e.g., see the recent

Now anyone who's read Peirce will know the importance he assigns to his categories of Firstness, Secondness, and Thirdness. These aren't easy to convey briefly, but see here. Suffice it to say here that the categories emerge in his theory of logic (as a part of his general theory of signs) in the form of a triad: term, proposition, argument.

Reading what he says of each, I could persuade myself that in type-theoretic language he might have written: type, term (or maybe judgment), argument. Translating this into CT form, one might think: object, morphism, operation on morphisms, which of course is how a category is standardly defined: objects, then morphisms, then identity morphisms and composition.

I've been interested to note then how people have recently been giving double categories a logical interpretation. We find that

are given slightly different logical readings as

There seems then to be a certain convergence to a layered understanding of logic. Any thoughts?

view this post on Zulip Morgan Rogers (he/him) (Jan 21 2025 at 17:40):

At the very least, the increasing use of double /n-fold categories in CT at large represents a progression towards including more ways of relating objects in a single categorical context, and that is consistent with your examples.

view this post on Zulip David Corfield (Jan 21 2025 at 19:15):

Peirce with his triadism would have us keep to 3 layers, arguing that any 4 or higher-way relation may be reduced to arrangements of 3-relations.

Hmm, that puts me in mind of something @Mike Shulman wrote:

In principle, the sort of “interaction between adjacent levels” that we’re interested in — using a 2-theories in a particular 3-theory to describe a deductive system for syntactic 1-theories in such 2-theories — could be generalized to any adjacent levels. For instance, we could imagine using 7-theories in a particular 8-theory to describe a deductive system for syntactic 6-theories in such 7-theories. However, in practice, when dimensions get beyond 2 or 3, human beings seem to do better with some sort of “encoding” of the higher-dimensional structure in terms of lower-dimensional structure.

But perhaps this is just about our convenience.

view this post on Zulip Morgan Rogers (he/him) (Jan 21 2025 at 21:03):

David Corfield said:

arguing that any 4 or higher-way relation may be reduced to arrangements of 3-relations

If all of the things being related were on the same level, that might be so, but that is no longer the case when there can be, for instance, relations between relations.

view this post on Zulip David Corfield (Jan 22 2025 at 07:37):

I think there's a way to see 4 interrelated levels in terms of interlocking 3-level devices. Let me try out a way of seeing higher categories in a Peircean fashion.

So, in terms of logic, it would seem natural to want to extend the sequence -- type, term/judgment, derivation, ... -- with some kind of fourth, such as derivation of derivations. Translating this into CT form, we would need to extend the notation to allow for derivations to be directly represented (say by 2-morphisms), then laws governing composition of 2-morphisms can capture derivations of derivations. Hence we arrive at 2-categories uniting our 4 elements.

But then Peirce suggests to us that we can view such things in terms of a relation between two 3-relations. So we try to reconfigure 2-categories so that they may be seen as a pair of interlocking categories. One good way to do this gives rise to the concept of a category internal to CatCat, or a double category, which then turns out to be more general than a 2-category.

view this post on Zulip Morgan Rogers (he/him) (Jan 22 2025 at 11:18):

I suppose you can do it by iteratively packaging data and relating the packages, but it seems artificial to do so without further motivation. For instance, I can express that a square in a category commutes by introducing ternary relations identifying the two available composites and then a further relation of equality between those composites, but that reduction doesn't inherently gain me anything. What is Peirce's argument for this decomposition of higher-order relations?

view this post on Zulip David Corfield (Jan 22 2025 at 11:37):

Morgan Rogers (he/him) said:

What is Peirce's argument for this decomposition of higher-order relations?

You can get a sense of it from a brief description here, written by Robert Burch who refers to a book in which he works out all the details.

The thing with Peirce is that his triadism runs through his vast system and takes on cosmic significance. Devoted Peirceans pour through 100,000 manuscript pages in the Harvard archive.

Even if one finds the whole account overblown, there's something to wonder about the intuitions which led him to his string-diagrammatic work in logic, picked up, as I mention in the opening message, by several people on this chat forum.

view this post on Zulip David Corfield (Jan 22 2025 at 11:41):

For those wanting a brief glimpse of what the three categories mean, here are three slides from an obvious fan:
image.png
image.png
image.png

view this post on Zulip Pawel Sobocinski (Jan 22 2025 at 11:58):

The way that I understand Peirce's triadism, at least in the context of relations, is that he had an intuition for what we now call Frobenius (bi)monoids. This algebraic structure is a crucial part of Carboni and Walters' cartesian bicategories of relations. Carboni and Walters knew that cartesian bicategories of relations are closely related to regular logic (the ∃, ∧ fragment of first order logic). In fact, later with Bonchi and Seeber we proved that the equational theory is sound and complete (in the sense of Gödel) for regular logic. The paper quoted by @David Corfield at the start of the thread shows how one can extend cartesian bicategories of relations to get full first order logic.

You can read Walters' account of the history of the Frobenius equation here https://rfcwalters.blogspot.com/2006/02/history-of-equation-1-tensor.html.

In terms of logic, one can think of the Frobenius laws serving as what we would now call "equational logic", i.e. the basic rules for handling equality e.g. in universal algebra.

There is evidence that Peirce had an intutive understanding for Frobenius bimonoids, even though the technology to express this formally didn't arrive for another 100 years. My collaborator Nathan Haydon found several snippets in the archives that convinced me of this -- you can find some of these in the footnotes of our paper "Compositional Diagrammatic First-Order Logic" https://www.ioc.ee/~pawel/papers/peirce.pdf (nb. the technical material in that paper is deprecated by the paper that @David Corfield quoted at the start of the thread)

view this post on Zulip Morgan Rogers (he/him) (Jan 22 2025 at 14:02):

David Corfield said:

You can get a sense of it from a brief description here, written by Robert Burch who refers to a book in which he works out all the details.

A quote from there is that,

The full philosophical import of his Reduction Thesis, and the philosophical importance of his triadism insofar as this triadism rests on his Reduction Thesis, cannot be ascertained without a prior understanding of his non-typical theory of identity and his special view of the fundamental nature of the relative product operation.

I conclude from this that I will not be able to ascertain "the full philosophical import of his Reduction Thesis" after all... but another claim there is that certain logical constructions are "more primitive" than others, while certain other constructions are not considered (a comparison is given with Quine's result that binary relations are sufficient for some other set of constructions). Can either of you shed any light on that?

view this post on Zulip Matt Earnshaw (Jan 22 2025 at 16:31):

The role of frobenius monoids suggests that the essence of the "reduction thesis" is already contained in n-ary identity relations. For example, we can define T(x,y,z):=x=yy=zT(x,y,z) := x=y \wedge y=z, which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of yy, that is, teridentity has already occurred. The conjunction of binary identities as string diagrams/existential graphs corresponds to the formula x=yw=zx=y \wedge w=z: to identify y and w, one uses the (co)monoid structure. The "spider theorem" more or less says that teridentity suffices to construct n-ary identities for all nn.

Although this understanding of lines of identity in terms of frobenius monoids is really nice, shoe-horning relations into categories does impose a directionality to relations that isn't there in Peirce. A simple ternary relation becomes two relations 212 \to 1 and 121 \to 2 etc. Something like entries-only star-polycategories might be a bit more faithful, as well as interesting to develop for its own sake.

view this post on Zulip John Baez (Jan 22 2025 at 16:36):

David Corfield said:

Devoted Peirceans pour through 100,000 manuscript pages in the Harvard archive.

"Pore", unless the archive has hot and cold running Peirceans.

That's an insanely large number of manuscript pages! It makes Grothendieck look like a guy with writer's block.

view this post on Zulip Kevin Carlson (Jan 22 2025 at 20:11):

Especially remarkable considering that Peirce mostly worked at the geological survey, and then I think was almost entirely unemployed for quite some time at the end of his life!

view this post on Zulip David Corfield (Jan 23 2025 at 09:44):

He was hounded by creditors in his later years. There's an amusing exchange he has with William James where James has managed to get him some paid lecturing for wealthy Bostonians, and tries unsuccessfully to get Peirce to tone down the crazily ambitious outline of his proposed syllabus on logic.

view this post on Zulip Morgan Rogers (he/him) (Jan 27 2025 at 08:42):

Matt Earnshaw said:

For example, we can define T(x,y,z):=x=yy=zT(x,y,z) := x=y \wedge y=z, which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of yy, that is, teridentity has already occurred. The conjunction of binary identities as string diagrams/existential graphs corresponds to the formula x=yw=zx=y \wedge w=z: to identify y and w, one uses the (co)monoid structure. The "spider theorem" more or less says that teridentity suffices to construct n-ary identities for all nn.

Wait so how do you do 4-ary identity?

view this post on Zulip David Corfield (Jan 27 2025 at 09:19):

Won't it just be Q(w,x,y,z):=w=xx=yy=zQ(w,x,y,z):= w= x \wedge x=y \wedge y=z, arising from the formula w=xu=yv=zw= x \wedge u=y \wedge v=z by identification of xx and uu, and of yy and vv?

view this post on Zulip Chad Nester (Jan 27 2025 at 09:24):

I think the easiest way to see what Peirce is talking about is by triangulating regular polygons.

In his diagrammatic notation, entities correspond to the end points of line segments. A line segment indicates that the two entities corresponding to its end points are equal. We can't connect two line segments to identify three entities, since the "middle" endpoint is lost when we connect them. Only two entities remain. If our line segments are allowed to branch, then the problem is solved. Connecting a "branched line segment" to some configuration results in an additional endpoint, allowing us to identify as many entities as we like.

To construct a diagram identifying nn separate entities, construct the regular polygon on nn vertices, triangulate it, and take the Poincaré dual of the resulting diagram. What you get is nn individual teridentity diagrams connected in a ring, with one "spoke" of each teridentity diagram connected to nothing, indicating a distinct entity.

If not sure how clear this is without any pictures, but I think that, at least from a certain narrow perspective, Peirce's thoughts on thirdness are about triangles, and about the way that you can build basically anything out of triangles.

view this post on Zulip David Corfield (Jan 27 2025 at 10:06):

That sounds right to me. I'm still left in awe and amazement though how he relates what appears to be a combinatorial fact about the number 3 to the grand metaphysical picture I referred to above with those three slides.

I think there may be something in that original thought I had about categories in our sense and in his sense. There's certainly a Peircean flavour to the passage which I re-glossed as: type, term/judgment, argument.

view this post on Zulip David Corfield (Jan 27 2025 at 10:11):

And this just concerns a fragment of his semiotics, the right-hand column of this table, from Chris Barnham's 'The Natural History of the Sign':

image.png

view this post on Zulip Chad Nester (Jan 27 2025 at 12:43):

There are certainly compelling echoes of the triadic idea of meaning in category theory. For example, if the basic unit is, to recklessly simplify, "something that means something to something", then it is very tempting to see the two lower somethings as objects of a category, and the "means something" that connects them as a morphism in that category.

However, it's quite frustrating to try to make things like this explicit, since the concepts involved are so very slippery.

view this post on Zulip David Corfield (Jan 27 2025 at 12:55):

Seeing the 'thirdness' of a category as composition (deduction) allows for the broadening of the notion of argument to other kinds of inference, such as Peirce's other two forms (induction and abduction). @Matteo Capucci (he/him) expands on this idea here.

Taken in the form of Kan extension/lift, it's all still about triangle completion.

view this post on Zulip Morgan Rogers (he/him) (Jan 27 2025 at 13:46):

Morgan Rogers (he/him) said:

Matt Earnshaw said:

For example, we can define T(x,y,z):=x=yy=zT(x,y,z) := x=y \wedge y=z, which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of yy, that is, teridentity has already occurred.

Wait so how do you do 4-ary identity?

My question here was really, if 4-ary identity is constructed from teridentity as the conjunction w=x=yx=y=zw=x=y \wedge x=y=z, why wouldn't the same argument about implicit identifications apply? How does this not degenerate into a spiral of identifications, in the spirit of Lewis Carroll's tortoise questioning modus ponens?

view this post on Zulip Matt Earnshaw (Jan 27 2025 at 16:44):

4-ary identity is obtained by composition of two teridentities, e.g. t,x=y=tt=z=w\exists t , x=y=t \wedge t=z=w, as a formula. In the combinatorial encoding of lines of identity by Frobenius bimonoids, the "Frobenius laws" give the necessary coherences.

image.png from https://www.gnusystems.ca/PeirceWelbyMarch1906.htm

view this post on Zulip Matteo Capucci (he/him) (Jan 27 2025 at 16:50):

Uhm but then why is x=yy=zx=y \land y=z not a good 3-ary identity?

view this post on Zulip Matt Earnshaw (Jan 27 2025 at 17:01):

There's nothing "wrong" with it of course, the point is just that, as a string diagram/existential graph it is not the conjunction (or composition) of binary identities, it is a three-way branching. This (I suppose) is the sense in which "both Quine and Peirce were right".

view this post on Zulip Morgan Rogers (he/him) (Jan 28 2025 at 16:25):

Matt Earnshaw said:

4-ary identity is obtained by composition of two teridentities, e.g. t,x=y=tt=z=w\exists t , x=y=t \wedge t=z=w, as a formula. In the combinatorial encoding of lines of identity by Frobenius bimonoids, the "Frobenius laws" give the necessary coherences.

Hmm. Reading the passage that you linked @Matt Earnshaw , it seems that the third entry in Peirce's ternary relation is supposed to be a witness, the "something" that is alluded to in the middle of the passage, whence it makes sense to use tt in that way. However, that only works under the presumption that one can find a witness; if there are no x,y,tx,y,t, then the absent object(s) denoted by those empty symbols are vacuously equal, but the 4-ary equality you constructed fails to capture this. There may be a different convention regarding existential quantification that fits into the Peirce framework. (He insists that every sign denotes some thing, so maybe he would argue that signs without forms are meaningless, but since he does allow for signs to represent unverified truths, there is still something to consider!)

A more serious critique I would give is that, on the face of it, his framework still precludes universal quantification. For example, "every man is an animal", a statement which one could take as definitionally true (and is close to a statement that Peirce models in that passage), does not meaningfully fit into this framework, since any instance of a something which is both man and animal will only witness the existential version of the statement.

view this post on Zulip Morgan Rogers (he/him) (Jan 28 2025 at 16:34):

It is a little tempting to ask for more clarification, more filling out of Peirce's framework etc, but I think my conclusion is already that the original question of @David Corfield about needing to arrange things in threes is a distraction (or a mere coincidence). The interactions between the components of a type theory will respectively be expressed as relations in one way or another, and if you want those relations to be presented Peirce-style with three components, that's fine. A component may be in "third position" for one relation, but in "second" or "first" position for another. I don't think there is solid grounds for proposing that there should only be three types of thing in logic/type theory.

view this post on Zulip David Corfield (Feb 02 2025 at 10:50):

I wasn't suggesting that we should think of Peirce as simply proposing three types of thing in logic/type theory. I was looking for some kind of resonance between his ideas and category theory and I think there's something to the thought that categories work as well as they do through the interdependent tripartite structure of object, morphism, composition.

And I find it at least suggestive that a way to proceed the next level up with 2-categories is to pass to double categories, which as categories internal to categories, could be construed in terms of the modification of 4-ary relations to 3-ary ones that @Matt Earnshaw showed us earlier.

Whether there's any value to all this can only be seen if it prompts a further thought in someone. E.g., I like what @Matteo Capucci (he/him) did with an earlier one of mine.

view this post on Zulip John Baez (Feb 02 2025 at 20:25):

Maybe someone already said it, but "object", "morphism" and "composition" are the 0-simplices, 1-simplices and 2-simplices in the nerve of a category. The 3-simplices are the associativity equations.

The 4-simplices are trivial for the nerve of a category, but when we take the nerve of a bicategory the 3-simplices are the associators and the 4-simplices are the pentagon equations:

pentagon identity as 4-simplex

view this post on Zulip David Corfield (Feb 03 2025 at 08:06):

Thanks!

John Baez said:

The 3-simplices are the associativity equations.

So in logic, rules about the equivalence of derivations.

Moving up a level, I wonder if there's something to note in the difference between the [[nerve of a bicategory]] and of a double category.

Is there any reason why at [[double nerve]] it's speaking only of the construction for 2-categories? Presumably we may speak of the nerve of a double category.

And this would be a [[bisimplicial set]]. So then the nerve of a double category is a certain kind of bisimplicial set, as it says here:
image.png

Is there a way to visualize bisimplices?

view this post on Zulip John Baez (Feb 03 2025 at 16:42):

They're products of two simplices, so the first exciting one is a triangular prism. When you get to a product of two equilateral triangles, you get an interesting 4-dimensional shape that's pretty hard to visualize. This is the sort of thing I spend time visualizing when I wake up in the middle of night, to take my mind off dark thoughts about American politics and global warming. But I haven't tried this one!

It'll have a bunch of triangular prisms as 3-dimensional faces. How many? Use the Leibniz law

(X×Y)=X×Y+X×Y \partial(X \times Y) = \partial X \times Y + X \times \partial Y

So these 3d faces come in two kinds: the boundary of the first triangle times the second triangle, and the first triangle times the boundary of the second triangle. So there 3+3 = 6 of them.

This is just a first step toward visualization. Thanks! My sleepless nights may be a bit less dark.

view this post on Zulip David Corfield (Feb 03 2025 at 19:36):

Glad to help!

And in terms of interpretation, is it that what had to enter as a 4-simplex in the case of a bicategory takes on factorized form as a double category, as 3×13 \times 1, 2×22 \times 2, 1×31 \times 3-bisimplices?

view this post on Zulip John Baez (Feb 03 2025 at 22:00):

Don't forget the 4×04 \times 0- and 0×40 \times 4-bisimplices!

view this post on Zulip John Baez (Feb 03 2025 at 22:02):

In the weakest imaginable sort of double category we might have both "horizontal" and "vertical" associators, showing up as 3×03 \times 0- and 0×30 \times 3-bisimplices, each obeying its own pentagon identity, which corresponds to 4×04 \times 0- and 0×40 \times 4-simplices.

view this post on Zulip John Baez (Feb 03 2025 at 22:03):

But people usually consider double categories that are strict in one direction, say the vertical one, so we only see 4×04 \times 0-shaped associators.

view this post on Zulip John Baez (Feb 03 2025 at 22:07):

I think 3×13 \times 1 is something about how the horizontal associators get along with vertical morphisms. 2×22 \times 2 should be about how horizontal composition gets along with vertical composition... maybe the interchange law?

view this post on Zulip John Baez (Feb 03 2025 at 22:07):

@Mike Shulman has probably worked this all out.

view this post on Zulip Mike Shulman (Feb 03 2025 at 23:12):

Yes, 2×22\times 2 should be the interchange law for the two composites of squares.

view this post on Zulip Mike Shulman (Feb 03 2025 at 23:14):

And 3×13\times 1 should be the "naturality" of the horizontal associators with respect to squares. That is, in a horizontally weak double category, horizontal composition of squares isn't strictly associative, and indeed it wouldn't even typecheck to ask it to be, since horizontal composition of arrows is not strictly associative either; but if you compose three squares horizontally in the two possible ways, you can compose the two results vertically with horizontal associators to get two things with the same boundary, and those things are equal.

view this post on Zulip John Baez (Feb 03 2025 at 23:15):

Good!

view this post on Zulip John Onstead (Feb 04 2025 at 02:12):

This topic was very interesting and I sort of went down a rabbit hole reading about different kinds of nerve. It seems that the kinds of things that have nerves consist of two "layers": some kind of underlying graph structure, and some kind of algebraic structure on top of that. This includes categories, double categories, and many more similar kinds of things! The nerve's lower elements then encode the underlying graph's properties while its higher levels encode the algebraic structure.

view this post on Zulip John Onstead (Feb 04 2025 at 02:12):

This turns out to be quite the general construction. Given a notion of "graph", a presheaf on some small category GG, and a notion of "free category monad", a familial monad on this presheaf category, one can define an algebra of this monad to be a category-like object with both "layers": the underlying graph of course, with the algebraic structure on top given by the monad algebra structure. Given this, the nerve is a presheaf on GG*, a suitable extension of GG whose additional elements encode the operations and equations described by the monad. If we let GG be the walking graph, then its extension with respect to the standard free category monad GG* is precisely the simplex category! Likewise, if GG is the walking double graph and the monad is the free double category monad (for at least some weakness level/notion of double category), then GG* is the bisimplex category!

view this post on Zulip David Corfield (Feb 05 2025 at 07:49):

Returning to the logical aspect, it's interesting to read Hayato Nasu's paper Internal Logic of Virtual Double Categories.

There we have types and terms as objects and tight 1-morphisms, as before. Then there are protypes as loose 1-morphisms and protypes as 2-morphisms. Interpreted in predicate Logic, these are seen as formulas and proofs of Horn clauses.

Interesting, the sense there of the level shift. Relations as a kind of type.

view this post on Zulip Pablo Donato (Feb 05 2025 at 13:29):

Coming back to Peirce, I'd like to share this very recent book called "Advances in Peircean Mathematics" edited by Fernando Zalamea, which should be quite relevant to the discussion: https://www.degruyter.com/document/doi/10.1515/9783110717631/html?lang=en

In particular, I recommend Chapter 1 that tries to give a (higher) category-theoretic account of Peirce's pragmaticist maxim. Here's the commentary of the chapter given by Zalamea in the introduction of the book:

Chapter 1 offers the first formal axiomatization of Peirce’s Pragmaticist Maxim, using sophisticated ideas, arguments, and variations of the machinery of Category Theory. The use of relational tools comes as a natural technique to capture the Maxim, but Arengas sharpens much the strata and layers of our comprehension of Peirce, thanks to his systematic use of refined categorical coverings (adjunctions, monads, descent theory). Not only the multiplicity of the Pragmaticist Maxim explodes in several formal contexts, but it becomes susceptible of proof in all of them, something that Arengas carries out with great technical precision. In this way, a strong Mathematical Metaphysics is obtained, something which would have bewildered the very Peirce.

view this post on Zulip John Baez (Feb 06 2025 at 18:57):

@David Corfield - here are some preliminary results on the bisimplex that's a product of two triangles:

https://mathstodon.xyz/@johncarlosbaez/113958248085070170

view this post on Zulip Hayato Nasu (Feb 07 2025 at 05:56):

David Corfield said:

Returning to the logical aspect, it's interesting to read Hayato Nasu's paper Internal Logic of Virtual Double Categories.

There we have types and terms as objects and tight 1-morphisms, as before. Then there are protypes as loose 1-morphisms and protypes as 2-morphisms. Interpreted in predicate Logic, these are seen as formulas and proofs of Horn clauses.

Interesting, the sense there of the level shift. Relations as a kind of type.

If I may add a remark to this, my recent thesis studies virtual double categories from a logical perspective, which aims to discover the semantical side of that story.

The most relevant result for this line of thought would be Corollary 2.3.37 stating that a cartesian equipment constructed from a certain kind of fibrations through the Bil-construction, which is also called Fr-construction in Mike Shulman's paper "Framed bicategories and monoidal fibrations," is characterized by the Frobenius axiom as in Walters and Wood's "Frobenius objects in Cartesian bicategories." I believe this indicates that the extent to which this axiom holds reflects how far the foundation based on relations is from the ordinary one (based on unilateral predicates).

view this post on Zulip David Corfield (Feb 07 2025 at 08:37):

@Hayato Nasu Thanks! That chimes with @Pawel Sobocinski 's comment above.

Gosh, that's really just at Masters level. I can only imagine what a PhD thesis might bring.

view this post on Zulip David Corfield (Feb 07 2025 at 08:57):

@John Baez Excellent. Now you just need to comprehend the logical meaning of its components.

view this post on Zulip John Baez (Feb 07 2025 at 23:13):

Yeah, that should keep me happy for a few more bouts of insomnia! Each triangle expresses a composition of 1-cells:

(a,b)ab (a, b) \mapsto a \circ b

Each triangular prism expresses a composition of 2-cells:

(f:aa,g:bb)(fg:abab) (f: a \to a', g: b \to b') \mapsto (f \circ g : a \circ b \to a' \circ b')

view this post on Zulip John Baez (Feb 07 2025 at 23:13):

This would be so much easier if I could quickly draw diagrams here: then you'd see the triangular prism.

view this post on Zulip John Baez (Feb 07 2025 at 23:15):

Then we wind up getting a 4d solid with 6 triangular prisms as faces, which come in two groups of 3. I need to run or I'd try to explain this....

view this post on Zulip David Corfield (Feb 08 2025 at 09:19):

The beauty of this quest is that it can be endlessly continued. Triple products of triangles await for when the insomnia gets really bad.

A wild Peircean thought: maybe something special kicks in at triple categories as you close the triad.

Hmm, but I was just hearing from David Jaz Myers yesterday about their use in dynamical systems and some idea @Matteo Capucci (he/him) has about the three dimensions (?).

But now I think of it, I had some discussion on this before:

Christian Williams had some ideas:

Dbl cats are logics: dim V is process (function) and dim H is relation.

Trp cats are metalogics: dim V is “metaprocess” (V-profunctors containing hetero-processes) and dim H is “metarelation” (H-profunctors), while dim T is transformation of inference (double functors).

That sounds rather like CatColab's changes of doctrine.

What would be perfect is for triple categories to make sense of Peirce's enigmatic Gamma graph system. I've had for a while a thought to see if any sense could be made of these in the context of the Licata-Shulman-Riley adjoint logic program.
image.png
What Is an n-Theory?.

view this post on Zulip John Baez (Feb 09 2025 at 00:43):

I don't believe there's anything uniquely magic about 3, though it has certain virtues like being the first non-even prime (a portent of things to come).

Amusingly, some ancient Greek mathematicians said 2 isn't a prime because primes can't be even. But a bit more seriously, I think very early Greeks didn't consider 2 to be a 'number', because ancient Greek has three grammatical numbers: singular, dual and plural. So we only get to honest 'numbers' when we reach 3. And we see this even in common usage today: we say we have a pair of hands, not a few hands or a number of hands.

Maybe this bears on Peirce, but I have trouble taking Peirce's fixation on the number 3 seriously. All numbers have their own virtues, while some shine more brightly than others.

view this post on Zulip David Corfield (Feb 09 2025 at 08:28):

John Baez said:

All numbers have their own virtues, while some shine more brightly than others.

It's not about natural numbers. 3:N\vdash 3: \mathbb{N} is just a term belonging to a type, so merely a morphism. Then it's status is no different to any other n:N\vdash n: \mathbb{N}. This is about relations, especially ones with an inter-level flavour.

Maybe nothing special occurs at n=3n=3 in the process of forming nn-fold categories. Or perhaps we've already reached the third level, seeing that 00-fold categories are sets, so have our triad 0,1,20, 1, 2.

Presumably the thesis you advised by Christian Williams has something to say:

We construct a three-dimensional category of categories, functors, profunctors, and matrix categories; squares are transformations, matrix functors, and matrix profunctors, and cubes are matrix transformations. This structure is a “bifibrant triple category without interchange”, which we call a metalogic.

view this post on Zulip John Baez (Feb 09 2025 at 19:12):

My point about natural numbers was meant to imply: while a Peircean might think "something special kicks in at triple categories", I'd say "probably, but I bet something else special kicks in at quadruple categories".

view this post on Zulip David Corfield (Feb 10 2025 at 08:08):

Right. But then maybe that special thing at the fourth step is pointing us to a new overlapping triple, and we should be looking for some different construction that better presents the novel element.

All speculation of course, but this is a continuation of the account I've been contemplating: It looks like the nn-category sequence, involving n+2n+2 layers of 0,,n0-, \cdots, n- morphisms + composition, should be extended to n=2n=2. Sure enough, 2-categories are a wonderful thing. However, something is lacking and rather than 4 layers of interlocking, if we can construe these as two triple layers, we may come to the idea of a double category. This is a better way to capture the novelty of structure that emerges at this level.

Indeed, had I had my Peircean wits about me 15 years ago, I might have jumped onto what @Mike Shulman was telling us about the joys of double categories.

So even if quadruple categories were to throw up something new, it might still be the case that a novel construction would make better sense of it.

view this post on Zulip David Corfield (Feb 10 2025 at 08:12):

If people can bear some more triadic thinking, I'm going to be speaking at the Oxford Topos Seminar (timing yet to be specified, but to be announced here at some stage next week, i.e., week beginning 17 Feb) on Peirce's three modes of inference -- deduction, induction, abduction -- as seen in a category-theoretic light.

view this post on Zulip John Baez (Feb 10 2025 at 18:30):

If you want to see 3d slices of a product of two equilateral triangles, @David Corfield, you can look at this movie while crossing your eyes so that the two images overlay into one image with perspective:

You'll see repeated slicings, at random angles.

A fellow named "Claude" made this in reply to my post.

view this post on Zulip David Corfield (Feb 10 2025 at 18:39):

That's just great. Well done, Claude.

view this post on Zulip Mike Shulman (Feb 10 2025 at 19:58):

I do think it's true that (m,n)(m,n)-categories and nn-fold categories get progressively less ubiquitous and useful with increasing nn (in contrast to mm, which as we now know is useful to take all the way to \infty right away). 0-categories are literally everywhere in mathematics; 1-categories are ubiquitous but some people do without them; 2-categories and double categories are good for a lot of things but most mathematicians get away without them; 3-categories and triple categories have pretty specialized uses inside category theory; I could probably count on one hand the number of serious uses of 4-categories or quadruple categories I've ever seen.

view this post on Zulip John Baez (Feb 10 2025 at 20:07):

But it's hard to tell what's useful until enough people know about it and try using it. Most mathematicians don't consider double categories useful, because most have never even heard of double categories. I optimistically believe that someday most mathematicians will consider them useful (though the number of mathematicians may collapse due to global warming and other crises). Then some of them will explore triple categories and so on. I believe there are exciting mathematical worlds still waiting for us to discover them.

view this post on Zulip David Corfield (Feb 11 2025 at 09:17):

Oh, are Peirce's graphs just a matter of a 2d rendering of the 3d plumbing of labelled pipes? Take the alpha-propositional system. The disjunction looks like this:
image.png
but why not see it as looking down a pair of pants, with leg holes labelled?

Maybe one sees the system as portraying pipe-plumbing from the perspective of one end looking through a pipe.
image.png.
Any labels written straight on the sheet of assertion are those arising from an initial cap. Pipes may be joined if labels match.

But it's magical plumbing, because the pipes are special (in the Frobenius algebra sense), so from A(BC)A \to (B \vee C), BDB \to D, and CDC \to D, we can deduce ADA \to D:
image.png
And the difference in the parity of the sheet records the end of the pipes your labels belong to. Then a ¬A\neg A graph caps off an AA end.

But maybe I'm just rehashing stuff. I see I was noting the 3d nature of modus ponens in a thread where I recommend Peirce's beta system to @Mike Shulman as a calculus for monoidal fibrations.

Here he is the next year, bumping the beta-system diagrams up a dimension:
image.png

view this post on Zulip Pablo Donato (Feb 11 2025 at 22:23):

@David Corfield I think the pipe analogy really applies to the lines of identity in Beta, since they satisfy the Frobenius equations that you depicted in 3D above? Then the teridentity is exactly the branching pipe (actually I thought of this analogy and wrote about it in my thesis).
Screenshot 2025-02-11 at 23.10.09.png

But I love the idea to see the cuts themselves as literally "cutting through pipes", so that the Frobenius algebra occurs both at the propositional and "individual" levels (or types and terms levels)

view this post on Zulip John Baez (Feb 12 2025 at 00:08):

David showed us a circle containing two smaller circles.

You can get the set of nested (topological) circles on the plane as follows. A pivotal category is roughly a monoidal category where every object has a left dual that is also its right dual. Take the free pivotal category on one self-dual object. Then if II is the unit for the tensor product, hom(I,I)\text{hom}(I,I) is the set of nested circles in the plane, up to homeomorphism.

So for example a typical element consists of 3 disjoint circles in the plane, one of which contains two smaller circles, one of which contains 37 smaller circles, while the other contains 2 smaller circles.

view this post on Zulip David Corfield (Feb 12 2025 at 09:59):

Maybe when we come to the system beta, it's about electricians and plumbers working together in the dangerous practice of sending wires down pipes :).

There's already something of this in the field of tape diagrams:
image.png

...tape diagrams are, literally, string diagrams of string diagrams.

Back with just the propositional plumbing, I guess the rules depend on which variety of logic you're in. Just about any logic will allow AAA \to A, represented as a pipe labelled AA at each end, or on the plane as a circle enclosing both AA and an enclosed AA.

And I guess linear logic is not allowing forking pipes, or pipes which drop a label as you pass down them.

So what makes the issue with excluded middle? Presumably, intuitionists can't see
image.png
merely as a 'not AA implies not AA' pipe.

On the other hand, to deduce ¬A\neg A from ABA \to B and ¬B\neg B is fine -- on the graph shifting the BB cap to fit on the end of a given AA to BB pipe, to cap off AA, so 'not AA'.

We need plumbing rules. Probably including how to bend pipes back to allow the kind of duality John mentions.