Category Theory
Zulip Server
Archive

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.

Stream: theory: mathematics

Topic: Computer calculations with presheaves

Jens Hemelaer (May 29 2020 at 09:36):

Calculations with presheaves can be tricky, and I would often trust a computer more than myself in doing these calculations. Does anyone have suggestions regarding existing code for doing this kind of calculations?

I'm thinking of code that can compute e.g. products, coproducts and most importantly (external) homs of presheaves.

To keep it realistic, the categories on which you take presheaves can be very small, with only a few objects and morphisms. Similarly, the presheaves can be very small, with say at most 5 or 6 sections over each object.

Thomas Read (May 29 2020 at 10:16):

Lean could certainly in theory do that sort of calculation, although it's not going to be particularly user friendly. I imagine other proof assistants (e.g. Agda) would work just as well.

Jens Hemelaer (May 29 2020 at 10:26):

Thanks for the reply. I don't have much experience with Lean. With "computing external homs", I mean that I want to generate a list of all natural transformations from the first presheaf to the second one. My impression is that proof assistants don't do this kind of work for you.

Thomas Read (May 29 2020 at 11:01):

I think that if everything is nice and finite it should be able to automagically do that, and if it can't then someone will probably fix the definitions so that it can. If you're interested in this route you should ask on the Lean zulip (https://leanprover.zulipchat.com/) - they're unreasonably friendly over there! (or @Bhavik Mehta would probably know, if he's around)

Jens Hemelaer (May 29 2020 at 11:03):

Thanks!

Philip Zucker (May 29 2020 at 13:49):

@Evan Patterson @James Fairbanks Would catlab.jl be able to do such a thing?

sarahzrf (Jun 03 2020 at 23:37):

hmm, i feel like ive heard that lean has weird computational behavior

sarahzrf (Jun 03 2020 at 23:40):

Jens Hemelaer said:

Thanks for the reply. I don't have much experience with Lean. With "computing external homs", I mean that I want to generate a list of all natural transformations from the first presheaf to the second one. My impression is that proof assistants don't do this kind of work for you.

for type-theory based proof assistants, at least, whether they do this kind of work for you isn't a simple yes-no

sarahzrf (Jun 03 2020 at 23:44):

most type theoretic proof assistants are built on systems with intrinsic computational content, where terms that you write down can be simplified into more explicit forms

sarahzrf (Jun 03 2020 at 23:47):

in a maximally nice system with "canonicalization" properties, such as the calculus of inductive constructions (which is what coq is supposed to implement), each well-typed term can be computed down to a "canonical" form, where what "canonical" means is a bit technical and depends on what type you're talking about, but e.g., for $\mathbb N$ it's gonna be an expression that's just a numeral

sarahzrf (Jun 03 2020 at 23:49):

iirc, lean is also based on the calculus of inductive constructions, but i've heard that it breaks some of the system's computational properties somehow...? maybe not many of those breakages crop up in realistic scenarios, but i dont use lean

sarahzrf (Jun 03 2020 at 23:54):

but so this kind of type-theoretic proof assistant does sort of do this kind of work for you, insofar as you write down a formula for something and then it can compute out a fully explicit representation of the thing (at least in theory—mathematical styles of definition often do not lend themselves well to efficient computation)

sarahzrf (Jun 03 2020 at 23:55):

but on the other hand, they also sort of don't do the kind of work you're asking about for you, because the devil is in the details of what "fully explicit representation" means and what kind of object you're talking about

sarahzrf (Jun 03 2020 at 23:57):

if you're doing combinatorics, and the objects in question are natural numbers, then a fully explicit representation is a numeral, and this is indeed what you're probably looking for as a result of a computation

sarahzrf (Jun 03 2020 at 23:57):

but what you asked about is a hom-set!

sarahzrf (Jun 03 2020 at 23:58):

and sets are fucked up!

sarahzrf (Jun 03 2020 at 23:59):

the representation you're probably looking for is probably an expression like $\{a, b, c\}$—but this is not the kind of "fully explicit representation" that a system like CIC guarantees you

sarahzrf (Jun 04 2020 at 00:02):

so in that sense, coq will not compute a list of natural transformations for you, indeed—but that's less about coq not computing things for you, and more about the facts that

1. categories have hom-sets, not hom-lists;
2. constructively, sets are extremely different from lists

Dan Doel (Jun 04 2020 at 00:05):

I don't know if I'd say it'll compute it for you. You'll have to do quite a bit of work to make it happen.

Dan Doel (Jun 04 2020 at 00:07):

Like, I wouldn't be surprised if the original asker is disappointed in how much Coq actually does toward the problem. :)

Dan Doel (Jun 04 2020 at 00:08):

Unless there is some library that someone has already written.

sarahzrf (Jun 04 2020 at 00:16):

shhhhhhhhhhhhhhhhh

sarahzrf (Jun 04 2020 at 00:16):

dan you'd make a terrible salesperson

sarahzrf (Jun 04 2020 at 00:16):

=)

Gershom (Jun 04 2020 at 00:30):

I only know of the very old now Computational Category Theory project for this: http://www.cs.man.ac.uk/~david/categories/#:~:text=Computational%20Category%20Theory%20is%20an,it%20was%20developed%20by%20D.

I've tried reimplementing some scraps of some stuff for myself, but never systematically gone through and thought about the question. Even the question "what is the optimal representation for actually computing on a category" is relatively nonobvious.

Gershom (Jun 04 2020 at 00:30):

Lean or any proof assistant won't do anything for you here. If you work axiomatically, you'll get axiomatic results rather than enumerations. It will let you check that your code that you claim computes a thing actually computes the thing, but that's more work, not less!

Evan Patterson (Jun 04 2020 at 00:38):

Philip Zucker said:

Evan Patterson James Fairbanks Would catlab.jl be able to do such a thing?

I'm late to the party here, but no @Philip Zucker , currently Catlab cannot do this. However, I'd really like to have it! This is bread-and-butter stuff for category theory, with lots of potential uses.

I'm starting to think about it. Like @Gershom says, probably the most important part is getting the data structures right. If anyone has thoughts on this, I'd love to hear them.

Gershom (Jun 04 2020 at 00:44):

The representation in Computational Category Theory is (in haskell-speak): data Category o a = {s : a -> o, t : a -> o, compose : a -> a -> a, id : a -> a}. This is relatively similar to a reified record of the category typeclass in haskell. It is nice to represent concrete categories with, but in my experience it is wrong to actually compute categorical constructions on. There I think you want something monotyped, with an explicit set of objects, and some subset of explicit morphisms given as pairs. I've done something similar for posets, and for categories, you just need to lift some invariants! Now computing can be done easily but inefficiently just by enumerating and checking (i.e. translating quantified formulae, etc).

Gershom (Jun 04 2020 at 00:45):

This works, but blows up in complexity fast, and you want either better algos, or a more efficient representation, or both, and I don't know how much work has been devoted to this.

Evan Patterson (Jun 04 2020 at 00:54):

Ah yes, Catlab has essentially the same data structure for categories (and similar ones for other categorical structures, via a generic system for such). I agree that it is useful for certain purposes, but not really for doing computations and inferences within finitely presented categories. For that, I figure that a graph-style representation of some kind would be more useful.

Then there is the question of data structures for presheaves. If you have the presheaf category of graphs, then people know all sorts of useful representations (adjacency list, adjacency matrix, etc.) Can such data structures be created generically, for any category of presheaves on a finitely presented category?

sarahzrf (Jun 04 2020 at 01:16):

@Gershom re: checking that your code computing a thing computes the thing—i think there may be some merit to, like, reflection-y stuff here perhaps

sarahzrf (Jun 04 2020 at 01:16):

anyway uh

sarahzrf (Jun 04 2020 at 01:17):

i bet if you formalized finite categories in coq, all of this stuff would compute very nicely

sarahzrf (Jun 04 2020 at 01:17):

like, bishop-finite

sarahzrf (Jun 04 2020 at 01:18):

well... i guess proving that all of the constructions result in new bishop-finite things is basically where youre implementing the computation, but

sarahzrf (Jun 04 2020 at 01:18):

on the other hand, there's some existing library work on dealing with proving that types are bishop-finite?

sarahzrf (Jun 04 2020 at 01:18):

:)

Reid Barton (Jun 04 2020 at 01:46):

Right, so in Lean (and I assume Coq also) it's easy to imagine writing something that could automatically derive fintype for everything in sight, and then run it and get back a list of all the things. Of course it would be atrociously slow if defined naively. A lot more interesting, and also probably possible, is to export an encoding of the things as a SAT/SMT instance, and hand it to an external solver, and hopefully get a list of the things in a practical amount of time.

eric brunner (Jun 04 2020 at 03:24):

thank you for sharing.

Gershom (Jun 04 2020 at 04:49):

Great points Evan. Here is an interesting post on graphs and categories: https://golem.ph.utexas.edu/category/2011/03/which_graphs_can_be_given_a_ca.html

I think this relates to @Jacques Carette's question about the relationship between Cat and Quiv the other day. I'm not actually sure if every finitely presented category is the free category on some quiver. Perhaps the proper statement is "is equivalent to"? If we have something like that, then we would want to represent categories of N many objects as NxN matrixes under free completion, and we could proceed from there. (Hah, and now all @Jade Master's stuff about generalized floyd-warshall immediately comes into play, because this is the same as determining the hom between two objects). It would be fun to code this up, and then to consider how one might "read off" from this data, e.g. the existence of a specific limit or other universal object as a path minimization question.

In this setting would functors be some form of linear maps?

Evan Patterson (Jun 04 2020 at 05:18):

Not every finitely presented category is the free category on a graph, but every such category is the quotient of a free category on a graph, by some finite set of equations. (David Spivak explains this nicely in his book on CT for the sciences, if you want to read about it.) So, even in the general case, I would expect the graph structure to be useful: it doesn't tell you how to deal with the equations, but it still tells you, by traversing the graph, how you can compose morphisms. As for Jade's intriguing new work, I need to get caught up on that!

Evan Patterson (Jun 04 2020 at 05:21):

Also, thanks for the pointer to that interesting blog post.

Gershom (Jun 04 2020 at 05:43):

Ah, I see. E.g. if you have a one object graph, then you get the free monoid on the self loops, but you may want a monoid that has some extra relations. I suppose there is also a "cofree" category on a graph, which is terminal rather than initial with regards to categories on that graph, and in the monoid case this would be the setting where we identify all the arrows, so we get the terminal monoid. I imagine there's perhaps a "categorical envelope" as well, which sits in-between, which would be the smallest category such that the underlying graph coincides. (Would be some work to check if this actually exists). If it exists, that could be the right thing. We'd get it from treating "categorical graphs"(or something similar) as a reflective subcategory of graphs, perhaps.

Now I'm really interested in pursuing this! I can't find the phd thesis in the blog post, but here are some related articles by the author, though sadly I don't read french https://arxiv.org/search/math?searchtype=author&query=Allouch%2C+S

Gershom (Jun 04 2020 at 05:49):

(also fun, and mentioned on the discussion, tho not terribly useful per se: http://www.reluctantm.com/gcruttw/publications/ams2014CruttwellCountingFiniteCats.pdf although it does suggest that a library for working only with cauchy complete categories might be more tractable)

Evan Patterson (Jun 04 2020 at 05:54):

Interesting thought. I had never thought about whether there is a cofree category on a graph, but according to this Math.SE question, it does not exist.

Gershom (Jun 04 2020 at 06:12):

Hrm, what I suppose I was imagining wasn't a functor but just a function graph -> cat that gave some category with the same objects, and as few morphisms as possible, but that's not necessarily that interesting. Essentially the motivation is just we want to represent "as many categories as possible" with "as simple graphs as possible" and I'm not worried about having a functor, necessarily, since the operations we perform on the underlying graphs need not correspond to the categorical operations in Graph. Anyway, it's all too vague right, now but the approach seems intriguing.

Gershom (Jun 04 2020 at 06:12):

the reflector/envelope thing seems perhaps more promising, if there's such a gadget.

Gershom (Jun 04 2020 at 06:14):

(perhaps this relates to sketches -- the categorical completion of a graph, the complete categorical completion, the categorical completion with products, etc)

Jens Hemelaer (Jun 04 2020 at 06:25):

I asked in the Lean chat as @Thomas Read suggested, and the consensus seems to be that it is possible to do these calculations in Lean in theory, but the calculations will be very slow.

Jens Hemelaer (Jun 04 2020 at 06:31):

I already implemented what I wanted in Python. I should have posted the code here, but to be honest, I am a bit embarassed about the code quality. I will add some readability and then drop a link here.

Jens Hemelaer (Jun 04 2020 at 07:58):

Here is the code: pdf file, ipynb file (jupyter notebook).

Jens Hemelaer (Jun 04 2020 at 08:04):

Criticism welcome!

Jens Hemelaer (Jun 04 2020 at 08:40):

I should thank @Morgan Rogers because he came up with the kind of calculations that I wanted to implement.

sarahzrf (Jun 04 2020 at 08:53):

aww, i probably would've tried to coax coq into computing some of this in a day or two if you hadnt just gone and done it

sarahzrf (Jun 04 2020 at 08:53):

...maybe i will anyway, i'm skeptical that it would be unusably slow

sarahzrf (Jun 04 2020 at 08:53):

probably just unpleasantly slow :>

Jens Hemelaer (Jun 04 2020 at 09:01):

I would be interested to see your approach. The python version is very fast with the tiny examples. But as soon as you make the categories larger, the Hom-sets blow up exponentially, and the code becomes unusable anyway.

sarahzrf (Jun 04 2020 at 09:02):

i wouldve probably tried hacking on it a bit earlier tbh

sarahzrf (Jun 04 2020 at 09:03):

i just dont have a development environment set up rn—im on a new laptop

sarahzrf (Jun 04 2020 at 09:03):

been procrastinating on getting things working

Morgan Rogers (he/him) (Jun 04 2020 at 09:42):

A couple of thoughts occurred to me: the first is that there are algebra packages/languages that are good at counting algebraic structures; one could probably adapt something available in sage? I've only seen demos of sage, never used it myself...
The other is that perhaps it could be easier with the formal def of a category to look at presheaves in the form of discrete fibrations?

Bas Spitters (Jun 08 2020 at 20:36):

I don't think it does precisely what you want, but CAP may be relevant in this topic. It's a variant of the GAP computer algebra system, but for categories instead of groups.

Gershom (Jun 09 2020 at 17:40):

CAP looks really interesting, but the documentation seems pretty confusing, I guess especially if one is not fully indoctrinated into GAP already. Do you know of any simpler tutorials or explanations on this? https://homalg-project.github.io/CAP_project/CAP/doc/chap0.html

(e.g. the first example says that you can take a thing called LeftPresentations on some other thing and that gives a category, but its not evident why one would know this from the docs: https://homalg-project.github.io/CAP_project/CAP/doc/chap11.html)

eric brunner (Jun 22 2020 at 03:48):

thank you for the link. -e update: i found a jupyter workbook in one of the co-author's websites, i think it meets the "simpler tutorials or expo" bogie.

Jens Hemelaer (Jun 22 2020 at 08:11):

@eric brunner-williams (uoregon) Sounds good, could you post the link?

eric brunner (Jun 22 2020 at 14:39):

of course.
https://sebastianpos.github.io/Try-out-CAP/

Jens Hemelaer (Jun 22 2020 at 16:40):

thanks!

Kris Brown (Oct 25 2023 at 22:09):

Hi @Jens Hemelaer, I saw your recent comment and link to this thread. I'm happy to share that Catlab.jl has developed a lot since this thread started, including the features you mentioned (i.e. enumerating the sets of arrows between presheaves, exponential object of two presheaves, limits/colimits, representable functors, pullback of presheaves along a functor).

Patrick Nicodemus (Oct 25 2023 at 23:53):

I don't fully understand what this is good for. Is it symbolic manipulation, like computer algebra? Do the sets have to be finite, or do they have to be constructed out of existing standard Julia types?
Can I use this to help me prove theorems in category theory about presheaves?

Evan Patterson (Oct 26 2023 at 00:08):

The capabilities that Kris describes are for presheaves valued in finite sets, so combinatorial rather than symbolic. We have a complementary symbolic (computer algebra) approach in the works but it's not quite ready for general use yet.

It won't, in its current form, help you prove theorems in category theory about presheaves.

Jens Hemelaer (Oct 26 2023 at 07:43):

I think it helps to distinguish between positive results and negative results about presheaves. For example, for a directed graph $G$ you can write $V(G)$ for the set of vertices and $E(G)$ for the set of edges.
Then a positive result would be: $V(Y^X) \simeq V(Y)^{V(X)}$.
And a negative result: $E(Y^X) \not\simeq E(Y)^{E(X)}$.

If you have a computer program for calculations, it can help with proving negative results (for example, by taking specific $X$ and $Y$ and calculating that $E(Y)^{E(X)}$ has 4 elements and $E(Y^X)$ has 2).
I understand that both Bewl here and Catlab.jl can be used for this kind of calculations.
Whereas a theorem prover like Lean is more targeted at positive results.

John Baez (Oct 26 2023 at 08:09):

Patrick Nicodemus said:

I don't fully understand what this is good for. Is it symbolic manipulation, like computer algebra? Do the sets have to be finite, or do they have to be constructed out of existing standard Julia types?
Can I use this to help me prove theorems in category theory about presheaves?

Here's one thing CatLab.jl is good for: we use it create software to help epidemiologists model the spread of infectious disease! Our software, written in Julia, relies heavily on operations involving presheaf categories. For example, to 'stratify' a model, e.g. subdividing a population into age groups, we use pullbacks in a presheaf category.

There's a lot of other software in Julia that uses presheaf categories, too.

John Baez (Oct 26 2023 at 08:14):

Basically, presheaves are a powerful, flexible sort of data structure, and to work with them one wants to be able to do all the operations @Kris Brown mentioned: exponentials, limits and colimits, pulling them back along functors, pushing them forward, etc.

Morgan Rogers (he/him) (Oct 26 2023 at 12:28):

To back up what @Jens Hemelaer said, we used the code he developed to verify a counterexample that was becoming too unwieldy to check by hand. Any code that only handles finite objects is necessarily limited in the positive results regarding presheaves that it can prove.

Kevin Arlin (Oct 26 2023 at 15:51):

Right, it's often confusing to people what Catlab is about in the context of all the dependently typed proof assistants flying around lately. We're very interested in getting more category theorists as users, but Catlab is not (at least not yet) a theorem-prover. It's more accurate to think of it as a scientific computing library based around $C$-sets as the fundamental data structure. The category theory is there, in the first instance, to make it possible to formally write down operations usually done in an ad hoc manner by practicing scientists/data scientists etc, and also to allow us to generate performant code in a uniform way for any kind of $C$-set. These motivations are quite different from, for instance, "we want to prove theorems in topos theory."

Kevin Arlin (Oct 26 2023 at 15:55):

So I think the main use case of Catlab for pure/purish category theorists trying to prove theorems is in calculating complicated concrete examples--finite ones are best for now, but we're working very actively on fleshing out the symbolic/CAS-type abilities too.

Chris Grossack (they/them) (Oct 26 2023 at 17:49):

@Jens Hemelaer, I'm curious if you've thought about trying to merge some of your code into sage, especially since it's already written in python. Then everyone who uses sage as their CAS of choice (myself included) would automatically have access to all these features for computing with presheaves!

Morgan Rogers (he/him) (Oct 26 2023 at 20:45):

If you contribute to sage does that make you a sage?

Jens Hemelaer (Oct 26 2023 at 22:00):

Chris Grossack (they/them) said:

Jens Hemelaer, I'm curious if you've thought about trying to merge some of your code into sage, especially since it's already written in python. Then everyone who uses sage as their CAS of choice (myself included) would automatically have access to all these features for computing with presheaves!

No, I hadn't considered it, great idea!

Ryan Wisnesky (Oct 28 2023 at 06:49):

Folks who are interested in automated theorem proving may want to check out CQL, https://www.categoricaldata.net , which has implemented a number of theorem provers from existing literature that are specially tailored to work with category theory specifically. It can decide the word problem for all the finitely presented categories we have seen arising in the practice of data integration, as well as many kinds of group, entropic groupoids, etc, including for theories that do not admit a re-writing system (using 'unfailing completion'). And it is open source too if anyone wants to invoke its theorem provers!

Mike Shulman (Oct 28 2023 at 16:47):

Hmm, that's interesting. In implementing modal type theory we have the problem of deciding equality for 2-cells of a finitely presented 2-category. Could your methods be useful for this?

Ryan Wisnesky (Oct 28 2023 at 17:34):

I'm not entirely sure but I think it could be figured out quickly, and here are some initial thoughts. The theorem provers do/can emit proofs of equality in a finitely presented 1-category, which presumably are related to 2-cells in finitely presented 2-categories. We can certainly ask, 'are two equality proofs equivalent' for various notions of equivalent, where the hope would be 'equivalence' turns into e.g. checking equivalence of (lambda?) terms that represent the proofs / 2-cells. This approach seems related to the Hilken 1999 'towards a proof theory of re-writing' paper, but I haven't worked anything out rigorously. (If that made sense, working rigorously is probably the next step)

Mike Shulman (Oct 28 2023 at 22:39):

Is there a characterization of the class of finitely presented categories for which the algorithm can decide the word problem?

Ryan Wisnesky (Oct 28 2023 at 23:19):

there's a few different algorithms, but we should no doubt start here: https://epubs.siam.org/doi/10.1137/0214073 , where the basic result is that the presentation has to be entirely unary (so a category, not a product category, etc) and has to have an equivalent "quasi re-write system" (my terminology), where the rules are "not length increasing". that is, you have length reducing re-write rules and re-write rules that keep length the same. assuming that exists, the algorithm will find it and there are complexity results about how fast decisions can be made. cql's implementation has been optimized by profiling against real world problems over many years, and is so fast that it simply re-generates decisions procedures every time the cql user presses a key. other algorithms will be slower but more general; this one is a workhorse for when everything is unary. The paper is hard to find so I'm attaching a copy.
thue.pdf

Mike Shulman (Oct 29 2023 at 00:51):

Thanks, I'll have a look. Presumably there is some extra condition that prevents us from just taking an arbitrary presentation and making it a rewrite system by directing all of the relations from whichever side is longer to whichever side is shorter? The fact that the algorithm can automatically find the rewrite system is pretty nice.

Mike Shulman (Oct 29 2023 at 00:52):

I wonder whether anyone has already worked out an analogous algorithm for 2-categories.

Ryan Wisnesky (Oct 29 2023 at 01:19):

As you'll no doubt see in the SIAM paper, the existence of a "length function" (total order on terms) that allows orientation of the equations is equivalent to confluence and termination, the usual required notions for "Knuth Bendix completion" to work. In the general case, you can use SAT solvers (such as Z3) to try to find such orderings, which provides another CQL decision procedure algorithm (the most general one we have): http://cl-informatik.uibk.ac.at/users/swinkler/verona/papers/WM-IJCAR18.pdf .

Mike Shulman (Oct 29 2023 at 02:22):

Hmm, I guess I have to read it to know what that means. I thought "length" would have meant the length of the word in the generators.

Mike Shulman (Oct 29 2023 at 02:23):

If there's an algorithm for monoidal categories, I bet it would generalize pretty easily to 2-categories.

Naso (Oct 29 2023 at 04:32):

Jens Hemelaer said:

Calculations with presheaves can be tricky, and I would often trust a computer more than myself in doing these calculations. Does anyone have suggestions regarding existing code for doing this kind of calculations?

I'm thinking of code that can compute e.g. products, coproducts and most importantly (external) homs of presheaves.

To keep it realistic, the categories on which you take presheaves can be very small, with only a few objects and morphisms. Similarly, the presheaves can be very small, with say at most 5 or 6 sections over each object.

I had written a small program a while ago in F# to do these kind of calculations, but it is indeed limited to very tiny presheaves :smiling_face_with_tear: It can be used in a Jupyter notebook environment--- here is an example notebook

Ryan Wisnesky (Oct 29 2023 at 04:54):

length of the word in generators works well for monoids, but in general, you can consider more abstract notions; you just need for "something" to decrease on every rewrite to ensure termination. Here's a survey of methods: http://www.cs.tau.ac.il/~nachumd/papers/termination.pdf

Jens Hemelaer (Oct 29 2023 at 18:24):

Naso said:

Jens Hemelaer said:

Calculations with presheaves can be tricky, and I would often trust a computer more than myself in doing these calculations. Does anyone have suggestions regarding existing code for doing this kind of calculations?

I'm thinking of code that can compute e.g. products, coproducts and most importantly (external) homs of presheaves.

To keep it realistic, the categories on which you take presheaves can be very small, with only a few objects and morphisms. Similarly, the presheaves can be very small, with say at most 5 or 6 sections over each object.

I had written a small program a while ago in F# to do these kind of calculations, but it is indeed limited to very tiny presheaves :smiling_face_with_tear: It can be used in a Jupyter notebook environment--- here is an example notebook

Thanks for posting the link, I like the clean syntax and the LaTeX support.