Graphs and their algorithms are fundamental to computer science, but they can be difficult to formalise, especially in dependently-typed proof assistants. Part of the problem is that graphs aren’t as well-behaved as inductive data types like trees or lists; another problem is that graph algorithms (at least in standard presentations) often aren’t structurally recursive. Instead of trying to find a way to make graphs behave like other familiar inductive types, this paper builds a formal theory of graphs and their algorithms where graphs are treated as coinductive structures from the beginning. We formalise our theory in Agda. This approach has its own unique challenges: Agda is more comfortable with induction than coinduction. Additionally, our formalisation relies on quotient types, which tend to make coinduction even harder to deal with. Nonetheless, we develop reusable techniques to deal with these difficulties, and the simple graph representation at the heart of our work turns out to be flexible, powerful, and formalisable.