82 citations · 120 across the 21 of their papers we have counts for
22 papers
An Algebraic Abstraction of the Localic Sheafification via the Tripos-to-Topos Construction
Maria Emilia Maietti, Davide Trotta
Localic and realizability toposes are two central classes of toposes in categorical logic, both arising from the Hyland, Johnstone and Pitts tripos-to-topos construction. We invest…
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…
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…
A topological counterpart of well-founded trees in dependent type theory
Maria Emilia Maietti, Pietro Sabelli
Within dependent type theory, we provide a topological counterpart of well-founded trees (for short, W-types) by using a proof-relevant version of the notion of inductively generat…
Quotients, pure existential completions and arithmetic universes
Maria Emilia Maietti, Davide Trotta
We provide a new description of Joyal's arithmetic universes through a characterization of the exact and regular completions of pure existential completions. We show that the regul…
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.…
Generalized existential completions and their regular and exact completions
Maria Emilia Maietti, Davide Trotta
This paper aims to apply the tool of generalized existential completions of conjunctive doctrines, concerning a class of morphisms of their base category, to deepen the study o…
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…
Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice
Maria Emilia Maietti, Samuele Maschio, Michael Rathjen
In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive definitions suf…
A realizability semantics for inductive formal topologies, Church's Thesis and Axiom of Choice
Maria Emilia Maietti, Samuele Maschio, Michael Rathjen
We present a Kleene realizability semantics for the intensional level of the Minimalist Foundation, for short mtt, extended with inductively generated formal topologies, Church's t…
A predicative variant of Hyland's Effective Topos
Maria Emilia Maietti, Samuele Maschio
Here, we present a subcategory pEff of Hyland's Effective Topos Eff which can be considered a predicative variant of Eff itself. The construction of pEff is motivated by the desire…
Elementary Quotient Completions, Church's Thesis, and Partioned Assemblies
Maria Emilia Maietti, Fabio Pasquali, Giuseppe Rosolini
Hyland's effective topos offers an important realizability model for constructive mathematics in the form of a category whose internal logic validates Church's Thesis. It also cont…
An extensional Kleene realizability semantics for the Minimalist Foundation
Maria Emilia Maietti, Samuele Maschio
We build a Kleene realizability semantics for the two-level Minimalist Foundation MF, ideated by Maietti and Sambin in 2005 and completed by Maietti in 2009. Thanks to this semanti…
Unifying exact completions
Maria Emilia Maietti, Giuseppe Rosolini
We define the notion of exact completion with respect to an existential elementary doctrine. We observe that the forgetful functor from the 2-category exact categories to existenti…
Convergence in Formal Topology: a unifying notion
Francesco Ciraulo, Maria Emilia Maietti, Giovanni Sambin
Several variations on the definition of a Formal Topology exist in the literature. They differ on how they express convergence, the formal property corresponding to the fact that o…
Elementary quotient completion
Maria Emilia Maietti, Giuseppe Rosolini
We extend the notion of exact completion on a weakly lex category to elementary doctrines. We show how any such doctrine admits an elementary quotient completion, which freely adds…
Constructive version of Boolean algebra
Francesco Ciraulo, Maria Emilia Maietti, Paola Toto
The notion of overlap algebra introduced by G. Sambin provides a constructive version of complete Boolean algebra. Here we first show some properties concerning overlap algebras: w…
Quotient completion for the foundation of constructive mathematics
Maria Emilia Maietti, Giuseppe Rosolini
We apply some tools developed in categorical logic to give an abstract description of constructions used to formalize constructive mathematics in foundations based on intensional t…
Subspaces of an arithmetic universe via type theory
Maria Emilia Maietti
We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.
Subspaces of an arithmetic universe via type theory
Maria Emilia Maietti
We define the notion of subspace of an arithmetic universe by using its internal dependent type theory.
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…