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

Homotopy Type Theory Electronic Seminar Talks, 2023-04-20

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.

[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)