A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS

DOI10.1017/jsl.2020.49OpenAlexW3094398884MaRDI QIDQ5159483

Maria Emilia Maietti, Samuele Maschio

Publication date: 27 October 2021

Published in: The Journal of Symbolic Logic (Search for Journal in Brave)

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

zbMATH Keywords

intuitionistic logicrecursion theorytoposesexact completionspredicative arithmetics

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) First-order arithmetic and fragments (03F30) Recursive functions and relations, subrecursive hierarchies (03D20) Intuitionistic mathematics (03F55)

Related Items (2)

Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice ⋮ 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
• Quotient completion for the foundation of constructive mathematics
• Aspects of predicative algebraic set theory. II: Realizability
• Realizability. An introduction to its categorical side
• A minimalist two-level foundation for constructive mathematics
• Axiomatizing higher-order Kleene realizability
• Locally cartesian closed exact completions
• Triposes, exact completions, and Hilbert's \(\varepsilon\)-operator
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• Some free constructions in realizability and proof theory
• Elementary quotient completion
• Colimit completions and the effective topos
• Tripos theory
• Relating Quotient Completions via Categorical Logic
• An extensional Kleene realizability semantics for the Minimalist Foundation
• Realizability: a historical essay

This page was built for publication: A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS