Matei, Adriel (2025) Type Theory and its Homotopical Interpretation. Bachelor's Thesis, Mathematics.
|
Text
bMATH2025MateiAR.pdf Download (723kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
Toestemming.pdf Restricted to Registered users only Download (181kB) |
Abstract
Martin Löf's Type Theory is a constructive formal system that can serve as the foundation of mathematics, offering an alternative to Zermelo–Fraenkel set theory. This thesis intends to be a tour of Martin Löf's Type Theory, aimed at people without a background in the topic. We present the core inference rules of the formal system, constructing a series of important types, and offering a first definition of the integers. Attempting to produce an alternative construction of the integers surfaces some missing pieces in our system, leading to the exploration of core ideas from Homotopy Type Theory and univalent mathematics. Finally, we use these tools to produce a second construction of the integers, and show that our definitions are homotopically equivalent.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Seri, M. and Lorscheid, O. |
| Degree programme: | Mathematics |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 15 Jul 2025 09:36 |
| Last Modified: | 15 Jul 2025 09:36 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/36212 |
Actions (login required)
 |
View Item |