Unsolved BananaCats - diagram editor & chaser (proof assist) for students of category theory. 🍌😹
enjoysmath last edited by
If anyone is interested in doing some PyQt5 coding and eventually connecting the app to Lean using its server mode (from Python 3.x), then please email me at email@example.com. I am currently the only coder. We would use probably github (free version) to host the code. So far it's going to be open source and free to download. I will put up a please donate button on a bubble.is project page that links to github. So if you're into bubble.is (drag-n-drop website creation including database workflows), then also contact me in order to help with the project page.
BananaCats is a visual diagram editor and chaser. I can show you a working prototype so far, though it doesn't do any chasing yet. Just editing. The editing is rather slick and is a culmination of all my PyQt5 2D graphics skills. It took two debugging experts (one other coder than me) to fix some of the geometry bugs. It supports persistent undo/redo stack. So even if you restart your machine you can undo/redo from whereever you left off in your drawing. That already works! It also does copy/paste with DnD and will eventually DnD to other apps (like the browser) text and images for posting questions say on MSE or a forum.
My code is very elegant and clean. I have been coding in PyQt5 for 6 years about. I have two professional (paid) projects under my belt. One of which is used by engineers several times a week (it's a tool).
I worked on the design last night in my sleep (just kidding). But when I woke up I felt refreshed and did a lot of design on cardboard (because I ran out of paper). Anyhow, it's a very nice and simple design. BananaCats_IsomorphismArrow.png Yoneda_BananaCats1.png ZoomspaceScreenshot5.png
Forgot to mention, BananaCats has been through 2-3 rewrites, so it's very well-written in that sense.
That is the official splash screen. It shows data loading / saving messages using QSplashScreen.