The Seifert-van Kampen Theorem in Homotopy Type Theory

Kuen-Bang Hou (Favonia), Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In Jean-Marc Talbot, Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France. Volume 62 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. [doi]

@inproceedings{FavoniaS16,
  title = {The Seifert-van Kampen Theorem in Homotopy Type Theory},
  author = {Kuen-Bang Hou (Favonia) and Michael Shulman},
  year = {2016},
  doi = {10.4230/LIPIcs.CSL.2016.22},
  url = {http://dx.doi.org/10.4230/LIPIcs.CSL.2016.22},
  researchr = {https://researchr.org/publication/FavoniaS16},
  cites = {0},
  citedby = {0},
  booktitle = {25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France},
  editor = {Jean-Marc Talbot and Laurent Regnier},
  volume = {62},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-95977-022-4},
}