April 20: Maria Emilia Maietti, A comparison between the Minimalist Foundation and Homotopy Type Theory

[Carlo Angiuli]

The final HoTTEST seminar of the season takes place this Thursday at the usual (summer) time of 11:30am EDT = 15:30 UTC.

Our speaker is Maria Emilia Maietti, whose talk is titled "A comparison between the Minimalist Foundation and Homotopy Type Theory". The talk will be 60 minutes long, followed by up to 30 minutes of discussion. The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including videos and slides from past talks, is available at:

https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html

Carlo

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)

--

Maria Emilia Maietti

A comparison between the Minimalist Foundation and Homotopy Type Theory

In this talk, I will outline the main common aspects and differences between the two-level Minimalist Foundation (for short MF) in [4] according to [3] and Homotopy Type Theory (HoTT) in [5].

A crucial difference between the two foundations is that HoTT has the remarkable expressive power to interpret both levels of MF thanks to the presence of the Univalence Axiom and set quotients as described in [1].

On the opposite, the Minimalist Foundation has a strictly predicative strength à la Feferman as witnessed by the realizability interpretation in [2]. Moreover, thanks to the absence of choice principles (since existential quantifiers are defined primitively!) and exponentiation of functional relations, its classical version is compatible with classical predicativity à la Weyl.

[1] Contente, M., Maietti, M.E.: The Compatibility of the Minimalist Foundation with Homotopy Type Theory. March 2023. Arxiv https://arxiv.org/abs/2207.03802

[2] H. Ishihara, Maietti, M.E., Maschio S., Streicher T.: Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice. Archive for Mathematical Logic 57, 873–888 (2018)

[3] Maietti, M.E., Sambin, G.: Toward a minimalist foundation for constructive mathematics. In: L. Crosilla and P. Schuster (ed.) From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, no. 48 in Oxford Logic Guides,pp. 91-114. Oxford University Press (2005)

[4] Maietti, M.E.: A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic 160(3), 319{354 (2009)

[5] Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.