All Outputs (2)

The Münchhausen Method in Type Theory (2023)
Journal Article
Altenkirch, T., Kaposi, A., Šinkarovs, A., & Végh, T. (2023). The Münchhausen Method in Type Theory. LIPIcs, 269, https://doi.org/10.4230/LIPIcs.TYPES.2022.10

In one of his long tales, after falling into a swamp, Baron Münchhausen salvaged himself and the horse by lifting them both up by his hair. Inspired by this, the paper presents a technique to justify very dependent types. Such types reference the ter... Read More about The Münchhausen Method in Type Theory.

Should Type Theory Replace Set Theory as the Foundation of Mathematics? (2023)
Journal Article
Altenkirch, T. (2023). Should Type Theory Replace Set Theory as the Foundation of Mathematics?. Global Philosophy, 33(1), Article 21. https://doi.org/10.1007/s10516-023-09676-0

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (H... Read More about Should Type Theory Replace Set Theory as the Foundation of Mathematics?.