Zulip Chat Archive

Stream: graph theory

Topic: c-sets


Kyle Miller (Dec 13 2021 at 10:43):

Something I thought was interesting a while back is these blog posts about graph theory in Julia, formulated using CC-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 (Dec 13 2021 at 10:43):

The blog posts seem to be about a much more restrictive version, which are CC-sets (functors from a category CC to Set). They show ways of encoding different kinds of combinatorial objects as CC-sets for appropriate CC. 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 (Dec 13 2021 at 10:44):

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 (Dec 13 2021 at 10:44):

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


Last updated: Dec 20 2023 at 11:08 UTC