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.
Lock (Jul 24 2025 at 21:57):@Amar Hadzihasanovic https://arxiv.org/pdf/2404.07273 The author starts with defining shapes of higher-categorical diagrams (called "molecules", whch are an inductively generated subclass of some "oriented graded posets"); and the collection Mol of all such "molecules" form an ω-category, and also for any "regular directed complex" P the slice/nerve Mol/P also forms an ω-category, and more generally for any "diagrammatic set" X (i.e. a presheaf over the subcategory of "molecules" which are "atoms" with "maps" which are cartesian/fibrations) then the slice/nerve Mol/X also forms an ω-category... Then the authors proceed to present some more "shape categories" such as "globes/thetas", "oriented simplicies", "oriented cubes", "positive opetopes", etc. all based on the corresponding constructions on "regular directed complexes", such as "suspensions", "joins/cones", "tensor products/cylinders"... and for a clearer proof that molecules/pasting-diagrams are closed under tensor products, the author introduces a notion of "generalised pasting" for gluing two molecules at a portion of their boundaries. Finally to prove that the tensor product and the join constructions defined on "regular directed complexed" are compatible with any corresponding constructions on ω-categories, the author will postpone until the end of the book, a review of such corresponding tensor product and join constructions on "directed chain complexes"...
I have not read any "proof" in the author's book, I just skimmed through the introductions prefaces of each sections and validated some of the book's theorem statements against some prototypical low-dimensional visual examples of ω-categories diagrams. But it is noteworthy that the author managed to solve the hard task of finding a coherent set of definitions which allows for purely "mechanical" algebraic proofs of theorem statements (rather than relying on the "implicit intuition" of the (obviously-visually validated) prototypical examples)
While I can concede that the author has solved this question (with concrete evidence such as the author's rewalt python software):
It is not apparent that the author has also solved this question:
Even after skimming through the author's entire book, my overall analysis remains that the first benchmark for this question of "computational-logic (type theory) for ω-categories" is whether and how it it possible to express the "staking of 2-cells along their bases" (a.k.a "generalized pasting"):
https://cutt.cx/48RQ
omega-category_staking_Capture.PNG
... I have some hints, for PART 2, if the author confirms that this question is still unresolved by the book (which then received numerous false advertising at CT2025, lol). @Valeria de Paiva
Kevin Carlson (Jul 24 2025 at 22:42):This is a really long ratio of message to question, and the question itself may not be clear. How is your example anything to do with type theory, rather than combinatorics? I'm pretty certain you can easily express pasting diagrams like those in Amar's formalism. The accusation of false advertising is rather serious and should not come with an 'lol', or probably before you're very sure you understand all the facts that would determine whether it occurred. And why do you keep tagging Valeria in unrelated messages?
David Michael Roberts (Jul 25 2025 at 07:08):Disparaging the book as containing "proof"s (with scare quotes) as if to claim that none of them are actually proofs, is a strong claim. It would be good to point out an actual flaw, and to do that you have to read them.
Amar Hadzihasanovic (Jul 25 2025 at 07:15):Thank you for the review. I should just say that the title of the book is "combinatorics of higher-categorical diagrams", not “-categories”, and that the perspective is explicitly that this is really a theory of “directed cell complexes” which can be studied independently of any theory of higher-categorical structures. For comparison, simplicial complexes, abstract polytopes and other kinds of combinatorial-topological structures have been (and are) studied without necessarily involving homotopy theory.
Of course, strict -categories play a role in the book because it so happens that the pasting of molecules satisfies, up to unique isomorphism, the axioms of strict -categories, and this algebraic perspective is useful for computations, but this is just stating that “molecules with pasting are a particular instance of a strict -category” and not that molecules are some kind of formalisation of -categories.
I presume that with “computational logic of -categories” you are, indeed, thinking of some kind of logical/type-theoretic formalisation of (some flavour of) higher categories, which is explicitly outside the scope of the book.
(Well, computational aspects tout-court are also explicitly outside the scope, although those are something that, as you probably know, I have been working on with Diana Kessler).
Amar Hadzihasanovic (Jul 25 2025 at 07:19):@David Michael Roberts I assumed that the quotes around "proofs" are just some stylistic idiosyncrasy and not scare-quotes :grinning_face_with_smiling_eyes:
Amar Hadzihasanovic (Jul 25 2025 at 07:23):Also, to clarify, I was at CT2025, I am not sure who Lock is and whether we have talked, but I have barely mentioned the book (if at all) during the conference, so if there was "advertising" (whether false or not false) it did not come from me!
If others advertised the book it's a pleasant surprise for me, and I hope that they did not give an exaggerated picture of its achievements.
Clémence Chanavat (Jul 25 2025 at 08:25):Maybe Lock is referring to my short talk, a good portion of which is indeed dedicated to advertising generalised pasting. If so, then maybe they can be more specific about the "false" part of what they think was "false advertising".
Morgan Rogers (he/him) (Jul 25 2025 at 09:19):@Lock please stop tagging Valeria de Paiva in posts that have nothing to do with her.
Matteo Capucci (he/him) (Jul 25 2025 at 09:52):Amar Hadzihasanovic said:
I am not sure who Lock is and whether we have talked
Indeed, @Lock it is kind of distasteful to give unwarranted reviews, especially when peevish, without putting your reputation at stake, that's what trolls do. Please be more mindful when engaging with people here.