Modularize and clean up Categories.Category.Construction.Graphs

[sstucki]

The module Categories.Category.Construction.Graphs should be refactored.

The module currently contains
* basic definitions (graphs and their morphisms),
* the definition of the category of graphs,
* the functor mapping graphs to their free categories,
* an adjunction between the forgetful functor and the free functor,
* various helper/utility constructs and lemmas (e.g. path equality, etc.).

These should probably all go in separate modules. Some of the code should be moved to the standard library.

(See comments in the code for more details.)

[sstucki]

Note that there is currently a pending PR (#42) that involves changes to the module. Any further changes should probably be made after that PR has been closed.

[JacquesCarette]

I entirely agree, that module is a mess.

[JacquesCarette]

Closed by PR #262 .