A minimalist two-level foundation for constructive mathematics

From MaRDI portal
Publication:1032635

DOI10.1016/J.APAL.2009.01.006zbMath1186.03075arXiv0811.2774OpenAlexW2005065769MaRDI QIDQ1032635

Maria Emilia Maietti

Publication date: 26 October 2009

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0811.2774




Related Items (30)

From type theory to setoids and backInductive and Coinductive Topological Generation with Church's thesis and the Axiom of ChoiceA Minimalist Foundation at WorkUnnamed ItemQuotient completion for the foundation of constructive mathematicsTriposes, exact completions, and Hilbert's \(\varepsilon\)-operatorDynamics in Foundations: What Does It Mean in the Practice of Mathematics?The compatibility of the minimalist foundation with homotopy type theoryTwo-level type theory and applicationsUnnamed ItemOn Choice Rules in Dependent Type TheoryUnnamed ItemThe principle of pointfree continuityMathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)Homotopy type-theoretic interpretations of constructive set theoriesConvergence in formal topology: a unifying notionA PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOSEmbedding locales and formal topologies into positive topologiesConsistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choiceA co-free construction for elementary doctrinesUnifying exact completionsSetoids and universesUnnamed ItemFormalization of Formal Topology by Means of the Interactive Theorem Prover MatitaNormalization by Evaluation for Typed Weak lambda-ReductionW-types in setoidsTopology as Faithful Communication Through RelationsCategories with families and first-order logic with dependent sortsA categorical reading of the numerical existence property in constructive foundationsOn the compatibility between the minimalist foundation and constructive set theory




Cites Work




This page was built for publication: A minimalist two-level foundation for constructive mathematics