Synthetic Topology and Constructive Metric Spaces

The thesis presents the subject of synthetic topology, especially with relation to metric spaces. A model of synthetic topology is a categorical model in which objects possess an intrinsic topology in a suitable sense, and all morphisms are continuous with regard to it. We redefine synthetic topology in order to incorporate closed sets, and several generalizations are made. Real numbers are reconstructed (to suit the new background) as open Dedekind cuts. An extensive theory is developed when metric and intrinsic topology match. In the end the results are examined in four specific models.

• Publication year

  2021

• Venue

  Unknown venue

• Publication date

  2021-04-21

• Fields of study

  Mathematics

• Identifiers
  arXiv 2104.10399
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Metric spaces in synthetic topology

  2012influential reference
• Foundations for Computable Topology

  2011influential reference
• The Dedekind reals in abstract Stone duality

  2009influential reference
• Constructive Urysohn's Universal Metric Space

  2008cited by this paper
• Constructive Gelfand duality for C*-algebras

  2008cited by this paper
• Real numbers and other completions

  2008cited by this paper
• On the Cauchy completeness of the constructive Cauchy reals

  2007cited by this paper
• RealLib: An efficient implementation of exact real arithmetic

  2007cited by this paper
• The universal separable metric space of Urysohn and isometric embeddings thereof in Banach spaces

  2007cited by this paper
• First Steps in Synthetic Computability Theory

  2006cited by this paper
• On the collection of points of a formal space

  2006cited by this paper
• Computably Based Locally Compact Spaces

  2005cited by this paper
• Computable Analysis

  2005cited by this paper
• Constructive reverse mathematics: compactness properties

  2005cited by this paper
• Synthetic Topology: of Data Types and Classical Spaces

  2004cited by this paper
• Inductively generated formal topologies

  2003cited by this paper
• Continuous Lattices and Domains

  2003cited by this paper
• Sketches of an Elephant: A Topos Theory Compendium Volume 1

  2002influential reference
• An Elementary Approach to Exponential Spaces

  2001cited by this paper
• The iRRAM: Exact Arithmetic in C++

  2000cited by this paper
• Geometric and Higher Order Logic in terms of Abstract Stone Duality

  2000cited by this paper
• The fundamental theorem of algebra: a constructive development without choice

  2000cited by this paper
• Outline of Synthetic Differential Geometry

  1998cited by this paper
• Twenty-five years of constructive type theory.

  1998cited by this paper
• Notes on constructive set theory

  1997cited by this paper
• Sheaves In Geometry And Logic

  1992influential reference
• The universal separable metric space of Urysohn and isometric embeddings thereof in Вanach spaces

  1992cited by this paper
• Constructivism in Mathematics, Volume 2

  1991cited by this paper
• Constructivism in mathematics

  1988cited by this paper
• Intuitionistic Formal Spaces — A First Communication

  1987cited by this paper
• Varieties of Constructive Mathematics: CONSTRUCTIVE ALGEBRA

  1987cited by this paper
• An extension of the Galois theory of Grothendieck

  1984cited by this paper
• Open locales and exponentiation

  1984cited by this paper
• Church's thesis without tears

  1983cited by this paper
• The Effective Topos

  1982cited by this paper
• Encyclopedia of Mathematics and its Applications.

  1982cited by this paper
• Synthetic Differential Geometry

  1981cited by this paper
• On a Topological Topos

  1979cited by this paper
• The Type Theoretic Interpretation of Constructive Set Theory

  1978cited by this paper
• Non-Standard Analysis

  1977cited by this paper
• Constructive set theory

  1975cited by this paper
• Diagonal arguments and cartesian closed categories

  1969cited by this paper
• The Foundations of Intuitionistic Mathematics.

  1967cited by this paper
• Review: G. Kriesel, D. Lacombe, J. Shoenfield, Effective Operations and Partial Recursive Functionals; G. Kreisel, D. Lacombe, J. R. Shoenfield, Partial Recursive Functionals and Effective Operations

  1966cited by this paper
• The foundations of intuitionistic mathematics : especially in relation to recursive functions

  1965cited by this paper
• The Foundations of Intuitionistic Mathematics

  1965cited by this paper
• On the interpretation of intuitionistic number theory

  1945cited by this paper
• Sur un espace métrique séparable universel

  1945influential reference
• LSU Digital Commons LSU Digital Commons Comparing Cartesian closed categories of (core) compactly Comparing Cartesian closed categories of (core) compactly generated spaces generated spaces

  year unknowncited by this paper

• Compactness in Constructive Mathematics via Affine Logic

  2026cites this paper
• A Foundation for Synthetic Stone Duality

  2024cites this paper
• Spreen spaces and the synthetic Kreisel-Lacombe-Shoenfield-Tseitin theorem

  2023cites this paper
• Using the internal language of toposes in algebraic geometry

  2021cites this paper
• Synthetic topology in Homotopy Type Theory for probabilistic programming

  2019cites this paper
• Every metric space is separable in function realizability

  2018cites this paper
• Making discrete decisions based on continuous values

  2017cites this paper
• On fixed-point theorems in synthetic computability

  2017cites this paper
• The intrinsic topology of Martin-Löf universes

  2016cites this paper
• Unified Approach to Real Numbers in Various Mathematical Settings

  2014cites this paper
• Unified Approach to Real Numbers in Various Mathematical Settings

  2014cites this paper
• The intrinsic topology of a Martin-Löf universe

  2012cites this paper
• Continuity and Algebraic Structure of the Urysohn space

  2012cites this paper
• Continuity and Algebraic Structure of the Urysohn space

  2012cites this paper
• Type classes for efficient exact real arithmetic in Coq

  2011cites this paper