Decidable reachability for finite quivers

[stschaef]

Here we prove that given a finite Quiver, it is decidable to determine if there exists a path between two vertices.

[stschaef]

I have been maintaining a small extension of Cubical to support an Agda development for building verified parsers

This "small extension" keeps growing. I have more substantive changes to come, mostly for reasoning about DecProps. I think its likely suited a different PR, so I am trying to gradually splinter off pieces that could be used more generally, with this reachability bit being the first

[felixwellen]

Thanks for the contribution!
Small improvements and additions are also very welcome (the smaller the PRs, the better) - as you can see we it might just take some time until somebody can have a look...