A Constructive Approach to Complete Spaces

TL;DR

This paper introduces cover spaces, a constructive generalization of metric and uniform spaces, providing a new framework for understanding completeness, compactness, and convergence in a constructive setting.

Contribution

It proposes cover spaces as a new class of spaces, offering an alternative to localic completion and enabling constructive definitions of key topological concepts.

Findings

Cover spaces form a topological concrete category.

The subcategory of complete spaces is full and reflective.

Constructive definitions of compactness and limits are achieved.

Abstract

In this paper, we present a constructive generalization of metric and uniform spaces by introducing a new class of spaces, called cover spaces. These spaces form a topological concrete category with a full reflective subcategory of complete spaces. This subcategory is closely related to a particular subcategory of locales, offering an alternative approach to localic completion. Additionally, we demonstrate how this framework provides simple constructive definitions of compact spaces, uniform convergence, and limits of nets.