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.
John T (May 20 2025 at 04:02):I have been using and enjoying quiver, but recently I came across a problem that I might want another tool for.
I have a category C, some monads on it, a category D of 5-object diagrams in C of a certain form, and an endofunctor Q on D defined as a certain pullback. It takes 20 objects of C to write down what Q(X) looks like- at least 5 more to map anything into it- and I would like to show (or find conditions on C under which I can show) that Q is a comonad on D. I'd be happy to give particulars on the problem if anyone's interested, but for purposes of this question the point is just that the diagrams I have to draw to check the comonad axioms for this are getting to be a bit bigger than I'd consider manageable for my purposes (at least for drawing them out "manually" and not having much experience with tricks that might let me manage the size a bit better).
Ideally when doing this I'd like to be able to do things like copy and paste large sub-diagrams, quickly apply a functor to all elements of a selection, or perhaps even automatically extract all the unique minimal faces from a diagram so I can more easily get a manageable list of pieces to check commutativity for. I don't see an option to do these things in quiver (though again, it is fantastic for sharing diagrams and for putting them into LaTeX), and I was wondering what other tools I should take a look at, if any, that might let me be a bit lazier about this project. I'm more than open to hearing about more code-based proof-assistant tools as well, but I haven't gotten any experience with those sorts of things yet.
Thanks! -John
Ralph Sarkis (May 20 2025 at 06:30):@Ambroise's diagram editor has several features that other editors lack like allowing to copy-paste. I am not sure if it has multicell editing.
Nathanael Arkor (May 20 2025 at 07:02):Copy and pasting is long overdue in quiver and I will look into implementing it this week.
Nathanael Arkor (May 20 2025 at 07:03):quickly apply a functor to all elements of a selection
This is also something I've thought about, and I have some ideas for making it practical. I'll play around with these ideas later and see whether they seem usable.
Kevin Carlson (May 20 2025 at 17:24):Nathanael Arkor said:
Copy and pasting is long overdue in quiver and I will look into implementing it this week.
This is great. I’ve had several instances lately of needing to type large partially duplicative diagrams. Thank you for your invaluable work!
Kevin Carlson (May 20 2025 at 17:25):On the other hand I discovered the ‘B’ key for moving groups of objects around recently and it’s incredibly useful for laying out a diagram dynamically while actually working out a proof, enabling live-diagramming in some cases rather than just typing out a drawn diagram as I find is usually necessary in tikz.
Nathanael Arkor (May 20 2025 at 21:08):In case it's not obvious, you can also move around groups of object with the mouse too: just click and drag in the region around an object.
Nathanael Arkor (May 20 2025 at 21:08):I have been meaning to write a tutorial for keyboard shortcuts too, and I will also try to get around to this.
Kevin Carlson (May 20 2025 at 22:51):Yeah, that'd be great; I just realized I don't understand how to actually change the style of an arrow via keyboard, for instance. I can cycle through the three style columns with 'D', but don't see how to cycle through the rows. This is coming up perhaps surprisingly often as I'm typing a lot of "equals signs" as level-2 arrows with no heads.
Nathanael Arkor (May 21 2025 at 05:57):If you turn on keyboard hints from the toolbar, it will tell you which keys to press in this kind of situation.
Kevin Carlson (May 21 2025 at 17:28):Ah, thanks. I hadn't noticed that keyboard hints apply to the styling panel as well as the main diagram.
Nathanael Arkor (May 25 2025 at 12:38):I've added the ability to copy and paste in quiver. I may revisit how it works in the future, but it seems to work well enough for now. I will experiment with the more advanced label editing idea I alluded to above when I have some time.
Ambroise (May 25 2025 at 16:17):Hello @John T , I would be happy to talk with you about your use case. My diagram editor has some mechanization features based on Rocq, typically to build a commutative diagram step-by-step (see https://github.com/amblafont/vscode-yade-example/releases/download/v0.1/demo-yade-example.mp4, based on this repo). On the editing side, there is a command to select a subface (that you can copy and paste), but let me know ifyou have any other suggestion!
John T (May 30 2025 at 00:26):@Ambroise Thanks, it looks very interesting from the video and tutorial! I am not particularly familiar with Rocq, should I go read up on that somewhere before getting started if I'm interested in proving everything, or does it mostly come up in places that are simple enough to figure out on the fly? My diagram only has four faces thus far that I've had to assert commutativity for; everything else has followed from naturality or monad laws. I'd include a link to said diagram in quiver, but it's about 10k characters past the message limit :sweat_smile: