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.
Avi Craimer (Nov 15 2020 at 01:55):Continuing the topic from over here:
https://categorytheory.zulipchat.com/#narrow/stream/229111-general/topic/category.20theory.20software/
Avi Craimer (Nov 15 2020 at 02:10):I've started working on web based tool to visualize category theory diagrams of the sort used in introductory teaching texts. My goal is to make something that could be used to build interactive educational materials for learning category theory.
To start I want to support support higher-order network diagrams up to 3rd order edges (it seems that most proofs only use up to 2-edges for natural transformations). I also want to allow a single universe of conceptual relationships be visualized in a variety of different ways, with some kind of highlighting to show common elements across between different visualizations.
In terms of the programming, I'm using Typescript, with D3 for the force simulation and React for the user interface. I haven't given much thought to any kind of backend (for now I'll probably make the whole app state saveable as JSON in local storage).
If anybody wants to help out let me know.
Jules Hedges (Nov 15 2020 at 11:14):Cool
Jules Hedges (Nov 15 2020 at 11:14):I don't see what you mean about "3rd order".... by that do you mean that the faces / 2-cells of the graph are first class things?
Jules Hedges (Nov 15 2020 at 11:16):I might suggest that for commutative diagrams snapping to a grid might produce better results than force simulation. Everybody is familiar with grid-based diagrams produced by tikzcd etc, and force simulation might produce some weird shapes
Matteo Capucci (he/him) (Nov 15 2020 at 11:47):Great! Do you a public repo one can join/snoop?
Avi Craimer (Nov 15 2020 at 16:35):Matteo Capucci said:
Great! Do you a public repo one can join/snoop?
The public repo is here.
https://github.com/AviCraimer/category-theory-diagrams
There isn't much besides the boiler-plate yet. I've just started writing the data structures for the higher order networks.
Avi Craimer (Nov 15 2020 at 16:42):Jules Hedges said:
I don't see what you mean about "3rd order".... by that do you mean that the faces / 2-cells of the graph are first class things?
So, in a regular graph you have vertexes and edges. I am defining a 2-edge as an edge between edges, and 3-edge as an edge between 2-edges.
Over in this topic I asked whether the concept of a higher order graph existed in mathematical discourse. To my surprise the answer was that it doesn't exactly exist. Something called a globular set comes close, but adds extra equational constrains onto the higher order network structure.
I am thinking of this from the point of view of visual diagrams. So what matters in practice is how many levels of edges between edges one needs to lay out graphically. Since most category theory proofs only use edges between edges (e.g., for natural transformations), my hope is that supporting up to 3-edges should be sufficient. If it turns out that support for more levels is needed, that can always be added later.
Avi Craimer (Nov 15 2020 at 16:45):Jules Hedges said:
I might suggest that for commutative diagrams snapping to a grid might produce better results than force simulation. Everybody is familiar with grid-based diagrams produced by tikzcd etc, and force simulation might produce some weird shapes
That's a good suggestion. I think I'll provide the option to do either kind of layout. It is useful to have a force layout to get things started so at least your elements are not all on top of each other. Then you could move things around and pin them to a grid if you like.
I imagine it might be useful to pin certain elements and then allow other elements to be automatically positioned with a force simulation that respects the fixed elements. Ideally, this gives the best of both worlds and avoids the need to manually position everything.