### Abstract

Homotopy type theory is a recent research area connecting type theory with homotopy theory by interpreting types as spaces. In particular, one can prove and mechanize type-theoretic analogues of homotopy-theoretic theorems, yielding "synthetic homotopy theory". Here we consider the Seifert-van Kampen theorem, which characterizes the loop structure of spaces obtained by gluing. This is useful in homotopy theory because many spaces are constructed by gluing, and the loop structure helps distinguish distinct spaces. The synthetic proof showcases many new characteristics of synthetic homotopy theory, such as the "encode-decode" method, enforced homotopy-invariance, and lack of underlying sets.

Original language | English (US) |
---|---|

Title of host publication | Computer Science Logic 2016, CSL 2016 |

Editors | Jean-Marc Talbot, Laurent Regnier |

Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |

ISBN (Electronic) | 9783959770224 |

DOIs | |

State | Published - Aug 1 2016 |

Externally published | Yes |

Event | 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic - Marseille, France Duration: Aug 29 2016 → Sep 1 2016 |

### Publication series

Name | Leibniz International Proceedings in Informatics, LIPIcs |
---|---|

Volume | 62 |

ISSN (Print) | 1868-8969 |

### Conference

Conference | 25th EACSL Annual Conference on Computer Science Logic, CSL 2016 and the 30th Workshop on Computer Science Logic |
---|---|

Country | France |

City | Marseille |

Period | 8/29/16 → 9/1/16 |

### Keywords

- Fundamental group
- Homotopy pushout
- Homotopy type theory
- Mechanized reasoning

## Fingerprint Dive into the research topics of 'The Seifert-van Kampen theorem in homotopy type theory'. Together they form a unique fingerprint.

## Cite this

*Computer Science Logic 2016, CSL 2016*(Leibniz International Proceedings in Informatics, LIPIcs; Vol. 62). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2016.22