BananaCats v 0.0 (alpha)

BananaCats is a diagramming tool for mathematicians, engineers, or physicists working, especially students of these fields, to create diagram-chasing tools, games, or just to further math itself. You will be able to search for and apply rules from the /standard_library directory. A diagram rule is just an arrow labeled with "Axiom. Some axiom text" or similarly for the cases of conjecture, theorem, lemma, definition. That feature is currently not complete in this release. Maybe tomorrow it will be ready.

Things should be organized in the standard_library. So for instance standard_library/Category Theory/Axioms. This structure is reflected in the source selection for a library search. How that will be done is we convert the selected graph parts into a networkx graph, one graph insertion-merge per .🌌 file. What results is a "graph database." We then use the subgraph isomorphism tools combined with smart regex variable-aware templates as Object/Arrow labels, in order to search for input graphs to any library rules that match the user's query graph. The results are displayed visually.

All graphs are asserted to commute. No attempt is made to check that a user's diagram commutes. In other words we don't auto-check things logically. That is too burdensome to code correctly. What we can do is allow the users to start with a diagram and apply primitive rules such as "identity is unique", glue diagrams together, take functorial images and auto-position the Objects/Arrows in the functor's image.

We also allow arrow-to-arrow, node-to-arrow, as well as node-to-node (the usual) arrow connections. Thus the visual language is expressive enough to encode natural maps as we see them in textbooks.

Category information must be kept in a label of a parent node, e.g. C:<b>Cat</b>, or A:<b>Ab</b>. That is there's no "dropdown menu" where you can set the category.

Of course you can enter in incorrect math, but so can you do on pen & paper. Once you master the tool, you will either be creating valid known math or furthing math with new definitions.