A minimalist two-level foundation for constructive mathematics
From MaRDI portal
Publication:1032635
DOI10.1016/J.APAL.2009.01.006zbMath1186.03075arXiv0811.2774OpenAlexW2005065769MaRDI QIDQ1032635
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 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− + ACint is equivalent to ACext
- 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