Formalization of homotopy pushouts in homotopy type theory
| Název práce v češtině: | Formalizace homotopických pushoutů v homotopické teorii typů |
|---|---|
| Název v anglickém jazyce: | Formalization of homotopy pushouts in homotopy type theory |
| Klíčová slova: | syntetická homotopická teorie|homotopická teorie typů|univalentní základy matematiky|formalizace|homotopické pushouty |
| Klíčová slova anglicky: | synthetic homotopy theory|homotopy type theory|univalent foundations of mathematics|formalization|homotopy pushouts |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | Egbert Rijke, Ph.D. |
| Řešitel: | Bc. Vojtěch Štěpančík - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 16.10.2023 |
| Datum zadání: | 17.10.2023 |
| Datum potvrzení stud. oddělením: | 17.10.2023 |
| Zásady pro vypracování |
| 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. |
| Seznam odborné literatury |
| 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 |