5 found
Sort by:
  1. Maria Emilia Maietti & Giuseppe Rosolini (2013). Quotient Completion for the Foundation of Constructive Mathematics. Logica Universalis 7 (3):371-402.
    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 type theory. The key concept we employ is that of a Lawvere hyperdoctrine for which we describe a notion of quotient completion. That notion includes the exact completion on a category with weak finite limits as an instance as well as examples from type theory that fall apart from this.
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  2. Maria Emilia Maietti & Giovanni Sambin (2013). Why Topology in the Minimalist Foundation Must Be Pointfree. Logic and Logical Philosophy 22 (2):167-199.
    We give arguments explaining why, when adopting a minimalist approach to constructive mathematics as that formalized in our two-level minimalist foundation, the choice for a pointfree approach to topology is not just a matter of convenience or mathematical elegance, but becomes compulsory. The main reason is that in our foundation real numbers, either as Dedekind cuts or as Cauchy sequences, do not form a set.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  3. Maria Emilia Maietti (2009). A Minimalist Two-Level Foundation for Constructive Mathematics. Annals of Pure and Applied Logic 160 (3):319-354.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Maria Emilia Maietti & Silvio Valentini (2004). A Structural Investigation on Formal Topology: Coreflection of Formal Covers and Exponentiability. Journal of Symbolic Logic 69 (4):967-1005.
    We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Maria Emilia Maietti & Silvio Valentini (1999). Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory? Mathematical Logic Quarterly 45 (4):521-532.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation