Regular universes and formal spaces

DOI10.1016/J.APAL.2005.05.025zbMATH Open1079.03061OpenAlexW2075921072MaRDI QIDQ2575774FDOQ2575774

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)

Cites Work

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

Cited In (4)

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

   Recommendations

• The problem of the formalization of constructive topology 👍 👎
• Inductively generated formal topologies. 👍 👎
• Title not available (Why is that?) 👍 👎
• A structural investigation on formal topology: coreflection of formal covers and exponentiability 👍 👎
• Title not available (Why is that?) 👍 👎

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)