Regular universes and formal spaces

DOI10.1016/J.APAL.2005.05.025MaRDI QIDQ2575774zbMATH OpenOpenAlexFDO

Authors Erik Palmgren

Publication date 6 December 2005

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

Full work available at URL https://doi.org/10.1016/j.apal.2005.05.025

zbMATH Keywords

Type theoryPredicativityPoint-free topology

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Topological spaces and generalizations (closure spaces, etc.) (54A05)

Recommendations

• The problem of the formalization of constructive topology
• Inductively generated formal topologies.
• scientific article; zbMATH DE number 1302063
• A structural investigation on formal topology: coreflection of formal covers and exponentiability
• Formal Baire space in constructive set theory

Cites work

• scientific article; zbMATH DE number 3853324 (Why is no real title available?)
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 4070894 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 1302063 (Why is no real title available?)
• A general formulation of simultaneous inductive-recursive definitions in type theory
• Accessible Categories: The Foundations of Categorical Model Theory
• An extension of the Galois theory of Grothendieck
• Completeness results for intuitionistic and modal logic in a categorical setting
• Formal spaces and their effective presentations
• Heyting-valued interpretations for constructive set theory
• Inductively generated formal topologies.
• Maximal and partial points in formal spaces
• Representability of locally compact regular spaces by domains and formal spaces
• Sheaves in geometry and logic: a first introduction to topos theory
• Some points in formal topology.
• Type theories, toposes and constructive set theory: Predicative aspects of AST
• Type-theoretic interpretation of iterated, strictly positive inductive definitions
• \(\kappa\)-frames

Cited in

(4)

• The associated sheaf functor theorem in algebraic set theory
• A constructive and functorial embedding of locally compact metric spaces into locales
• Embedding locales and formal topologies into positive topologies
• Quotient topologies in constructive set theory and type theory

This page was built for publication: Regular universes and formal spaces

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2575774)