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.
Jade Master (Jul 04 2021 at 01:27):I've been playing a bit in globular.science. I wrote a proof that adjunctions compose here. I also printed out the sequence of string diagrams: image4.png
image3.png
image2.png
image1.png
Jade Master (Jul 04 2021 at 01:33):Well it's really half of a proof, one of the snake equations for the composite adjunction.
Spencer Breiner (Jul 04 2021 at 03:35):Note that there is an updated tool homotopy.io. There are some additional features for higher-dimensional diagrams, and I think also some usability improvements elsewhere.
Jade Master (Jul 04 2021 at 05:27):Yeah I tried using that one first but I had some issue, so I switched back to the earlier version :)
Nick Hu (Jul 06 2021 at 02:25):(There's an even more updated version available at beta.homotopy.io :silence:)
Nick Hu (Jul 06 2021 at 02:27):One of the reasons that globular feels different to work with is that the 4D homotopies are all hand-coded; homotopy.io is on the other hand built on a fundamentally new theoretical framework for finitely presented infinity categories with good combinatorial properties (theory of associative n-categories)
Nick Hu (Jul 06 2021 at 02:28):Everything that you can do in globular you can also do in homotopy.io (except the bugs, hopefully), but sometimes you need more steps
