Formalization of homotopy pushouts in homotopy type theory
| Thesis title in Czech: | Formalizace homotopických pushoutů v homotopické teorii typů |
|---|---|
| Thesis title in English: | Formalization of homotopy pushouts in homotopy type theory |
| Key words: | syntetická homotopická teorie|homotopická teorie typů|univalentní základy matematiky|formalizace|homotopické pushouty |
| English key words: | synthetic homotopy theory|homotopy type theory|univalent foundations of mathematics|formalization|homotopy pushouts |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | diploma thesis |
| Thesis language: | angličtina |
| Department: | Department of Algebra (32-KA) |
| Supervisor: | Egbert Rijke, Ph.D. |
| Author: | Bc. Vojtěch Štěpančík - assigned and confirmed by the Study Dept. |
| Date of registration: | 16.10.2023 |
| Date of assignment: | 17.10.2023 |
| Confirmed by Study dept. on: | 17.10.2023 |
| Guidelines |
| The student will gain a basic understanding of synthetic homotopy theory and its formalization in univalent foundations. They will study and present fundamental properties of homotopy pushouts and their applications, and formalize them in homotopy type theory using the Agda proof assistant in the agda-unimath library of formalized mathematics from a univalent point of view. |
| References |
| B. Munson & I. Volić, Cubical Homotopy Theory, 2015
E. Rijke, Introduction to Homotopy Type Theory, 2002 E. Rijke, Classifying Types, 2019 The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, 2013 D. Wärn, Path spaces of pushouts, unpublished preprint |