BananaCats - diagram editor & chaser (proof assist) for students of category theory. 🍌😹
-
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 fruitfulapproach@gmail.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.
