Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice

DOI10.46298/lmcs-18(4:5)2022OpenAlexW3146864628MaRDI QIDQ5060191

Samuele Maschio, Maria Emilia Maietti, Michael Rathjen

Publication date: 9 January 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

Church's thesisrealizabilityaxiom of choiceconstructive set theorypoint-free topology

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Related Items (1)

The compatibility of the minimalist foundation with homotopy type 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
• Quotient completion for the foundation of constructive mathematics
• A minimalist two-level foundation for constructive mathematics
• Constructivism in mathematics. An introduction. Volume II
• Inaccessibility in constructive set theory and type theory
• The strength of some Martin-Löf type theories
• Inductively generated formal topologies.
• Some points in formal topology.
• Inaccessible set axioms may have little consistency strength
• 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
• The strength of Martin-Löf type theory with a superuniverse. I
• Intuitionistic fixed point logic
• Unifying exact completions
• Containers: Constructing strictly positive types
• Pretopologies and a uniform presentation of sup-lattices, quantales and frames
• Elementary quotient completion
• The principle of pointfree continuity
• A construction of non-well-founded sets within Martin-Löf's type theory
• On the regular extension axiom and its variants
• ABSTRACT INDUCTIVE AND CO-INDUCTIVE DEFINITIONS
• Type Theory based on Dependent Inductive and Coinductive Types
• Convergence in formal topology: a unifying notion
• A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS
• Proof Theory of Constructive Systems: Inductive Types and Univalence
• Non-wellfounded trees in Homotopy Type Theory
• A structural investigation on formal topology: coreflection of formal covers and exponentiability
• Models of non-well-founded sets via an indexed final coalgebra theorem
• The strength of Martin-Löf type theory with a superuniverse. II
• Dynamics in Foundations: What Does It Mean in the Practice of Mathematics?

This page was built for publication: Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice