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.
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?
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.
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.
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.
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 , or a double category, which then turns out to be more general than a 2-category.
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?
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.
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
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)
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?
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 , which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of , that is, teridentity has already occurred. The conjunction of binary identities as string diagrams/existential graphs corresponds to the formula : 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 .
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 and etc. Something like entries-only star-polycategories might be a bit more faithful, as well as interesting to develop for its own sake.
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.
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!
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.
Matt Earnshaw said:
For example, we can define , which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of , that is, teridentity has already occurred. The conjunction of binary identities as string diagrams/existential graphs corresponds to the formula : 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 .
Wait so how do you do 4-ary identity?
Won't it just be , arising from the formula by identification of and , and of and ?
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 separate entities, construct the regular polygon on vertices, triangulate it, and take the Poincaré dual of the resulting diagram. What you get is 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.
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.
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':
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.
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.
Morgan Rogers (he/him) said:
Matt Earnshaw said:
For example, we can define , which apparently reduces "teridentity" to binary identity. This however contains a "hidden" identity, between the free instances of , 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 , 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?
4-ary identity is obtained by composition of two teridentities, e.g. , 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
Uhm but then why is not a good 3-ary identity?
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".
Matt Earnshaw said:
4-ary identity is obtained by composition of two teridentities, e.g. , 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 in that way. However, that only works under the presumption that one can find a witness; if there are no , 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.
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.
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.
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
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?
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
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.
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 , , -bisimplices?
Don't forget the - and -bisimplices!
In the weakest imaginable sort of double category we might have both "horizontal" and "vertical" associators, showing up as - and -bisimplices, each obeying its own pentagon identity, which corresponds to - and -simplices.
But people usually consider double categories that are strict in one direction, say the vertical one, so we only see -shaped associators.
I think is something about how the horizontal associators get along with vertical morphisms. should be about how horizontal composition gets along with vertical composition... maybe the interchange law?
@Mike Shulman has probably worked this all out.
Yes, should be the interchange law for the two composites of squares.
And 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.
Good!
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.
This turns out to be quite the general construction. Given a notion of "graph", a presheaf on some small category , 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 , a suitable extension of whose additional elements encode the operations and equations described by the monad. If we let be the walking graph, then its extension with respect to the standard free category monad is precisely the simplex category! Likewise, if 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 is the bisimplex category!
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.
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.
@David Corfield - here are some preliminary results on the bisimplex that's a product of two triangles:
https://mathstodon.xyz/@johncarlosbaez/113958248085070170
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).
@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.
@John Baez Excellent. Now you just need to comprehend the logical meaning of its components.
Yeah, that should keep me happy for a few more bouts of insomnia! Each triangle expresses a composition of 1-cells:
Each triangular prism expresses a composition of 2-cells:
This would be so much easier if I could quickly draw diagrams here: then you'd see the triangular prism.
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....
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?.
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.
John Baez said:
All numbers have their own virtues, while some shine more brightly than others.
It's not about natural numbers. is just a term belonging to a type, so merely a morphism. Then it's status is no different to any other . This is about relations, especially ones with an inter-level flavour.
Maybe nothing special occurs at in the process of forming -fold categories. Or perhaps we've already reached the third level, seeing that -fold categories are sets, so have our triad .
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.
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".
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 -category sequence, involving layers of morphisms + composition, should be extended to . 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.
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.
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.
That's just great. Well done, Claude.
I do think it's true that -categories and -fold categories get progressively less ubiquitous and useful with increasing (in contrast to , which as we now know is useful to take all the way to 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.
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.
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 , , and , we can deduce :
image.png
And the difference in the parity of the sheet records the end of the pipes your labels belong to. Then a graph caps off an 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
@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)
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 is the unit for the tensor product, 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.
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 , represented as a pipe labelled at each end, or on the plane as a circle enclosing both and an enclosed .
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 implies not ' pipe.
On the other hand, to deduce from and is fine -- on the graph shifting the cap to fit on the end of a given to pipe, to cap off , so 'not '.
We need plumbing rules. Probably including how to bend pipes back to allow the kind of duality John mentions.