Here are some of my latest thoughts on agda… 
Graphs are to categories as lists are to monoids
Numbers are the lengths of lists which are the flattenings of trees which are the spannings of graphs. Unlike the first three, graphs have two underlying types of interest –the vertices and the edges– and it is getting to grips with this complexity that we attempt to tackle by considering their ‘algebraic’ counterpart: Categories.
In our exploration of what graphs could possibly be and their relationships to lists are, we shall mechanise, or implement, our claims since there will be many details and it is easy to make mistakes –moreover as a self-learning project, I'd feel more confident to make
Life & Computing Science by Musa Al-hassy is licensed under a Creative Commons Attribution-ShareAlike 3.0 Unported License