A minimalist two-level foundation for constructive mathematics

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

zbMATH Keywords

constructive mathematicsextensional set theoryintensional constructive type theory

Mathematics Subject Classification ID

Other constructive mathematics (03F65)

Related Items (30)

From type theory to setoids and back ⋮ Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ A Minimalist Foundation at Work ⋮ Unnamed Item ⋮ Quotient completion for the foundation of constructive mathematics ⋮ Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator ⋮ Dynamics in Foundations: What Does It Mean in the Practice of Mathematics? ⋮ The compatibility of the minimalist foundation with homotopy type theory ⋮ Two-level type theory and applications ⋮ Unnamed Item ⋮ On Choice Rules in Dependent Type Theory ⋮ Unnamed Item ⋮ The principle of pointfree continuity ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Homotopy type-theoretic interpretations of constructive set theories ⋮ Convergence in formal topology: a unifying notion ⋮ A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS ⋮ Embedding locales and formal topologies into positive topologies ⋮ Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice ⋮ A co-free construction for elementary doctrines ⋮ Unifying exact completions ⋮ Setoids and universes ⋮ Unnamed Item ⋮ Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita ⋮ Normalization by Evaluation for Typed Weak lambda-Reduction ⋮ W-types in setoids ⋮ Topology as Faithful Communication Through Relations ⋮ Categories with families and first-order logic with dependent sorts ⋮ A categorical reading of the numerical existence property in constructive foundations ⋮ On the compatibility between the minimalist foundation and constructive set theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Telescopic mappings in typed lambda calculus
• Constructivism in mathematics. An introduction. Volume I
• Categorical logic and type theory
• Regular and exact completions
• Some points in formal topology.
• Wellfounded trees in categories
• Locally cartesian closed exact completions
• Some free constructions in realizability and proof theory
• The formal system λδ
• Locally cartesian closed categories and type theory
• Modular correspondence between dependent type theories and categories including pretopoi and topoi
• Finiteness in a Minimalist Foundation
• HYPERDOCTRINES, NATURAL DEDUCTION AND THE BECK CONDITION
• Tripos theory
• Adjointness in Foundations
• Choice Implies Excluded Middle
• Setoids in type theory
• Extensional Constructs in Intensional Type Theory
• Internal type theory
• Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?
• EM + Ext₋ + AC_int is equivalent to AC_ext
• Quotients over Minimal Type Theory
• The generalised type-theoretic interpretation of constructive set theory
• Type theories, toposes and constructive set theory: Predicative aspects of AST

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