The patch topology in univalent foundations

DOI10.1017/S0960129525000088MaRDI QIDQ6936250zbMATH OpenFDO

Authors Igor Arrieta, Martín Escardo, Ayberk Tosun

Publication date 1 September 2025

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/S0960129525000088

zbMATH Keywords

constructive mathematicslocale theorypatch topologypointfree topologyspectral localeunivalent foundations

Mathematics Subject Classification ID

Type theory (03B38) Categorical logic, topoi (03G30) Frames, locales (06D22)

Cites work

• A representation of stably compact spaces, and patch topology.
• Cubical type theory: a constructive interpretation of the univalence axiom
• Dependently typed programming in Agda
• Formal Topology and Univalent Foundations
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 4152376 (Why is no real title available?)
• scientific article; zbMATH DE number 3787631 (Why is no real title available?)
• scientific article; zbMATH DE number 1330441 (Why is no real title available?)
• scientific article; zbMATH DE number 575948 (Why is no real title available?)
• scientific article; zbMATH DE number 2117177 (Why is no real title available?)
• Inductively generated formal topologies.
• Notions of anonymous existence in Martin-Löf type theory
• On some peculiar aspects of the constructive theory of point-free spaces
• On the existence of Stone-Čech compactification
• Patch locale of a spectral locale in univalent type theory
• Predicative Aspects of Order Theory in Univalent Foundations
• Properly injective spaces and function spaces
• The regular-locally compact coreflection of a stably locally compact locale

This page was built for publication: The patch topology in univalent foundations

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