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.
Simon Burton (Dec 05 2020 at 19:41):I've been waiting for someone to do a video showing off homotopy.io, here it is: https://vimeo.com/484400667
"Jamie Vicary: Introducing homotopy.io: A proof assistant for geometrical higher category theory"
Henry Story (Dec 05 2020 at 19:43):Great tool to learn about string diagrams of any dimensions. I followed along trying out the examples of multi-dimensional string diagrams on the web site shown in the video, just using point and click :-)
Robin Piedeleu (Dec 13 2020 at 15:01):Thanks for sharing!
Towards the end, Jamie mentions another approach one could take to design a proof assistant for higher-categories: strict associators and interchangers, but weak unitors. He adds that proofs in this setting would resemble manipulations of (higher-dimensional analogues of) proof-nets with units. Does anyone know of more fleshed-out work that takes this view? Are there already combinatorial structures that captures precisely this level of weakness? Maybe @Amar Hadzihasanovic or @Antonin Delpeuch have some idea? (Sorry if this is a rather naive question but considering the many different approaches to higher-categories I am not sure where to start looking).
Nathanael Arkor (Dec 13 2020 at 15:15):Kock defines a notion of "fair categories", which are higher categories with weak units in Weak identity arrows in higher categories.
Kenji Maillard (Dec 13 2020 at 15:19):I also wondered when watching that part of the presentation whether it would amount to a proof of Simpson's Conjecture...
Amar Hadzihasanovic (Dec 13 2020 at 15:30):@Robin Piedeleu well my own diagrammatic omega-categories (section 6 of this) can be conceived as a semistrict-with-weak-units model of higher categories. There's still a (small?) gap in trying to prove that it's fully general.
The omega-groupoid case, with nonalgebraic units, had been done by Simon Henry, here.
Amar Hadzihasanovic (Dec 13 2020 at 15:32):And as Nathanael says, a lot of very interesting work in this spirit had been done by Joachim Kock and André Joyal.
Amar Hadzihasanovic (Dec 13 2020 at 15:34):None of this work, so far, has been concerned with formalisation or proof assistants.
Robin Piedeleu (Dec 13 2020 at 16:02):Thanks for all the pointers!
Kenji Maillard said:
I also wondered when watching that part of the presentation whether it would amount to a proof of Simpson's Conjecture...
I don't think so: seems like you could just have an explicit combinatorial construction of weakly-unital semistrict higher-categories without a proof that every fully weak higher-category is weakly equivalent to one of these. The work that people pointed to above should give examples of this.
Robin Piedeleu (Dec 13 2020 at 16:02):Or maybe I'm completely misunderstanding what giving a model of higher-categories means...
Kenji Maillard (Dec 13 2020 at 16:15):hm, you are right an explicit combinatorial presentation of these structures doesn't prove the conjecture.
I thought that Jamie Vicary was advertising these structures (both the weak unit ones and the weak interchange ones) because they are as strict as possible while maintaining "good properties". I interpreted these "good properties" as "can represent all weak omega-categories", but maybe it was rather "expected to be reasonable for an implementation" :thinking:
Robin Piedeleu (Dec 13 2020 at 16:18):Yes, and I suppose another good properties is to be (conjecturally) sufficiently expressive!
Robin Piedeleu (Dec 13 2020 at 16:31):Amar Hadzihasanovic said:
Robin Piedeleu well my own diagrammatic omega-categories (section 6 of this) can be conceived as a semistrict-with-weak-units model of higher categories. There's still a (small?) gap in trying to prove that it's fully general.
Did you give some thoughts to what sort of diagrams/graphs/other structures could best represent cells in your omega-categories? I don't mean the underlying combinatorial machinery, but rather a graphical calculus, like the one for associative -categories used in homotopy.io, which is a generalisation of the familiar diagrams for bicategories.
Amar Hadzihasanovic (Dec 13 2020 at 18:26):@Robin Piedeleu The diagrams that can be interpreted in diagrammatic sets are just a sub-class of the diagrams that can be interpreted in strict omega-categories
(some terms in this statement need to be clarified and there are a couple footnotes attached, but the substance is true).
Indeed, the main point of the project was to have a fully general, weak model in which existing diagrammatic proofs could be interpreted with minimal effort.
Amar Hadzihasanovic (Dec 13 2020 at 18:34):For example, the 2d string diagrams that make sense in a diagrammatic set are all the ones where every cell has at least one input and one output (so you may have to introduce some explicit units and unitors), and in a diagrammatic omega-category all the connected ones have a composite.
Amar Hadzihasanovic (Dec 13 2020 at 18:34):In general the philosophy is that at the price of explicitly handling (some) units and unitors, you can make sure that your diagrammatic proofs make sense in general weak higher categories.
Amar Hadzihasanovic (Dec 13 2020 at 18:35):If you're interested in some finer points, maybe we can continue discussing privately.
Robin Piedeleu (Dec 14 2020 at 09:28):Thanks, Amar, this is helpful.
I don't think I get the motivation for the "at least one input and one output" or connectedness conditions but I'll try to work through some example diagrams in low dimensions to get a better feel for them. I might contact you privately if I have other questions!