It would be useful to have an implementation for finite categories, that is, categories with finitely many objects and finitely many morphisms.
The importance of such categories is that they are closed under many constructions (finite limits of finite categories always exist, as do finite colimits, duals, internal homs, etc.), and all questions about them are decidable (completeness, connectedness, etc.).
Potential Use Case
A mathematician wonders "are limits in functor categories always computed pointwise?"
They boot up Catlab, and run a brute force search on small finite categories.
After a few seconds, Catlab tells them no! There is a limit in Fun(•→•, •⮆•→•) which is not computed pointwise.
Problem solved.
This sort of things happens often in other disciplines, e.g. algebraic geometers and commutative algebraists use Macaulay2 and Singular to run computations like these, and group theorists use GAP. Category theorists (currently) have no such tool.
I suggest (as was also recommended by @KevinArlin on Zulip) that a finite category be implemented internally by storing:
a list of objects
a list of morphisms
an assignment of a domain object for each morphism
an assignment of a codomain object for each morphism
an assignment of an identity morphism for each object
a composition relation
With this in place, the aforementioned constructions should not be too hard to implement, nor should it be very difficult to write code to check the aforementioned properties.
Wishlist:
[ ] The constructors for finite categories should be set up to validate inputs, i.e. throw an error if the user tries to create a finite category that is not well-defined.
[ ] It should be possible to construct a finite category from a finite presentation and a natural number N, which the user claims is an upper bound on the length of a reduced word in the category (wrt to the given presentation). If this claim is incorrect (this is checkable in finite time), the constructor should throw an error.
[ ] It should be easy (1 LOC) to construct products and coproducts of finite categories, as well as duals and functor categories.
[ ] It should be easy (1 LOC) to check if a finite category is complete.
Please note that I am beginner in both Julia and Catlab, so I may be overlooking some important details! I'm happy to help implement things wherever I can, but I think it would be unwise for me to get this off the ground, just because I'm completely unfamiliar with this codebase, and best practices for Julia in general.
It would be useful to have an implementation for finite categories, that is, categories with finitely many objects and finitely many morphisms.
The importance of such categories is that they are closed under many constructions (finite limits of finite categories always exist, as do finite colimits, duals, internal homs, etc.), and all questions about them are decidable (completeness, connectedness, etc.).
Potential Use Case
This sort of things happens often in other disciplines, e.g. algebraic geometers and commutative algebraists use Macaulay2 and Singular to run computations like these, and group theorists use GAP. Category theorists (currently) have no such tool.
I suggest (as was also recommended by @KevinArlin on Zulip) that a finite category be implemented internally by storing:
With this in place, the aforementioned constructions should not be too hard to implement, nor should it be very difficult to write code to check the aforementioned properties.
Wishlist:
Please note that I am beginner in both Julia and Catlab, so I may be overlooking some important details! I'm happy to help implement things wherever I can, but I think it would be unwise for me to get this off the ground, just because I'm completely unfamiliar with this codebase, and best practices for Julia in general.