The Seifert–Van Kampen Theorem in Homotopy Type Theory (2016) [pdf]