c-sets

Stream: graph theory

[Kyle Miller]

Something I thought was interesting a while back is these blog posts about graph theory in Julia, formulated using $C$-sets. https://www.algebraicjulia.org/blog/tag/c-sets/ This is part of a project called AlgebraicJulia https://www.algebraicjulia.org/

They say it's part of the framework of generalized algebraic theories. As far as I can tell, having tried to parse the nlab page, generalized algebraic theories are more-or-less types you can define in Lean using structure, where all the types in sight are either bound variables, pi types, equalities, or Type.

[Kyle Miller]

The blog posts seem to be about a much more restrictive version, which are $C$-sets (functors from a category $C$ to Set). They show ways of encoding different kinds of combinatorial objects as $C$-sets for appropriate $C$. Though there's a limitation that you can't encode things like simple graphs using this scheme (no way to say graphs are loopless).

[Kyle Miller]

I'm not suggesting organizing things categorically like this, but I think it helps clarify some of the problems involved in the design of combinatorial objects.

[Kyle Miller]

One thing that would be cool is if there were a way to automatically generate morphism types given a structure definition.