Make ap=>path-split private.
Make code more modular.
More refactoring.
Add equiv-is-prop.
Add trans-b-code-glue.
Naive van Kampen in Agda, done.
Rename VanKampen to NaiveVanKampen.
Separate out lemmas from PushoutDef to Pushout.
Modules are now parametrized by pushout-diag.