6 papers · 1 filter
Quasitoposes as elementary quotient completions
Maria Emilia Maietti, Fabio Pasquali, Giuseppe Rosolini
The elementary quotient completion of an elementary doctrine in the sense of Lawvere was introduced in previous work by the first and third authors. It generalises the exact comple…
On the Compatibility of Constructive Predicative Mathematics with Weyl's Classical Predicativity
Michele Contente, Maria Emilia Maietti
It is well known that most constructive and predicative foundations aiming to develop Bishop's constructive analysis are incompatible with a classical predicative development of an…
Fibred sets within a predicative and constructive effective topos
Cipriano Junior Cioffo, Maria Emilia Maietti, Samuele Maschio
We describe the fibrational structure of sets within the predicative variant of Hyland's Effective Topos previously introduced in Feferman's predicat…
Equiconsistency of the Minimalist Foundation with its classical version
Maria Emilia Maietti, Pietro Sabelli
The Minimalist Foundation, for short MF, was conceived by the first author with G. Sambin in 2005, and fully formalized in 2009, as a common core among the most relevant constructi…
A minimalist two-level foundation for constructive mathematics
Maria Emilia Maietti
We present a two-level theory to formalize constructive mathematics as advocated in a previous paper with G. Sambin. One level is given by an intensional type theory, called Minima…
The Compatibility of the Minimalist Foundation with Homotopy Type Theory
Michele Contente, Maria Emilia Maietti
The Minimalist Foundation, for short MF, is a two-level foundation for constructive mathematics ideated by Maietti and Sambin in 2005 and then fully formalized by Maietti in 2009.…