Reveal more computational contents.

Sorry that I forgot to push the changes.
Several previous commits won't build.
Move app-trans to Path.agda.
Add ->-is-prop.
Add various lemmas for paths.
The van Kampen theorem, done.