Maria Emilia Maietti

We provide applications of the elementary quotient completion introduced with Pino Rosolini in [MR13] to build

on one hand

  1. a constructive and predicative fibred version of Hyland’s Effective topos in [CMM24] based on [MM21] and validating the Formal Church’s thesis;

and on the other hand

  1. a constructive and predicative fibred quasi-topos of assemblies that validates Brouwer’s continuity principles and only the instance of the Formal Church’s thesis on quasi-topos morphisms.

These predicative topos-like constructions stem from the categorical analysis of the Effective topos and of its subcategory of Assemblies in terms of completions in [RR90, MPR19, MT21, MT23] and employs the tripos-to-quasi-topos construction provided in [MPR23]. They will be applied to provide predicative consistency proofs for the two-level Minimalist Foundation [MS05,M09] with the above-mentioned principles of effectiveness and continuity.

  • [CMM24] C.J. Cioffo, M.E. Maietti, and S. Maschio “Fibred sets within a predicative and constructive Effective Topos”, 2024
  • [M09] M.E. Maietti “A minimalist two-level foundation for constructive mathematics”, Ann. Pure Appl. Log. 160(3), 319-354, 2009
  • [MM21] M.E. Maietti, S. Maschio “A predicative variant of Hyland’s Effective Topos”, Journal of Symbolic Logic, vol 86 (2): 433-447, 2021
  • [MPR19] M.E. Maietti, F. Pasquali and G. Rosolini “Elementary Quotient Completions, Church’s Thesis, and Partitioned Assemblies”, Logical Methods in Computer Science, 15(2), 2019
  • [MPR23] M.E. Maietti, F. Pasquali and G. Rosolini “Quasi-toposes as elementary quotient completions”, https://arxiv.org/abs/2111.15299, 2023
  • [MR13] M.E. Maietti, G. Rosolini “Elementary quotient completion”, Theory and Applications of Categories, 27(17):445–463, 2013
  • [MS05] M.E. Maietti, G. Sambin “Toward a minimalist foundation for constructive mathematics”. In “From Sets and Types to Topology and Analysis” L. Crosilla and P. Schuster (ed.), Oxford Logic Guides, vol 48, p. 91-114. OUP, 2005
  • [MT21] M. E. Maietti, D. Trotta “Generalized existential completions and their regular and exact completions” https://arxiv.org/abs/2111.03850, 2021
  • [MT23] M. E. Maietti, D. Trotta “A characterization of generalized existential completions”, Ann. Pure Appl. Log. 174(4): 103234, 2023
  • [RR90] E. Robinson, G. Rosolini “Colimit completions and the Effective Topos”, Journal of Symbolic Logic, vol. 55 (2):678-699, 1990

Updated: