#functionaprogramming — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #functionaprogramming, aggregated by home.social.
-
Had a very interesting #CategoryTheory meetup today. We discussed free construction and did some exercises and the answers seemed unsatisfying.
The basic source of discomfort was this - When we are given a graph, to convert it into a category, we add seemingly arbitrary morphisms to it. Some object doesn't have an identity arrow? Add it! There is no arrow for the composition of two arrows, add it! This seemed like we were *completing* the graph rather than *converting* it into a category.
We are all learning Category theory and none of us had an answer for this. We didn't even know if the way we were doing free construction was correct. There were exercises on free construction, and we looked at a few solutions from other people online, and they all seemed to suffer from the same problem.
Well after the meetup I searched online, and within 2 minutes had the answer. I was only able to find it because having mulled the problem over, I knew what to search for.
Basically the free construction from a graph does not convert arrows to morphisms. It converts *paths* to morphisms. So for an object without arrows, there is still a morphism which represents "take no path". This is the identity morphism. We have not added it to the graph, it is always present for every node in the graph if we define morphisms as paths.
For a graph with a single object with one arrow pointing to itself, the number of morphisms (i.e. paths) is infinite because you can cross the arrow any number of times.
For a graph with two objects and one directional arrow between them, we have only one possible path (once you cross the arrow to go to the other object, there is no way back), so there is only one morphism apart from identities.
This makes so much more sense to me, because this means that free construction does *not* add any arrows to the diagram or change the diagram in any way - we just define a category out of the existing structure.
Most other (secondary) sources on the web are wrong about what the free construction is. If we hadn't gone into this question in the meetup, I wouldn't even have known there was a gap in my understanding.
Basically, I'm looking forward to the next meetup!