\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{uniform locale}

\hypertarget{uniform_locales}{}\section*{{Uniform Locales}}\label{uniform_locales}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{basic_notions}{Basic notions}\dotfill \pageref*{basic_notions} \linebreak
\noindent\hyperlink{covering_uniformities}{Covering uniformities}\dotfill \pageref*{covering_uniformities} \linebreak
\noindent\hyperlink{entourage_uniformities}{Entourage uniformities}\dotfill \pageref*{entourage_uniformities} \linebreak
\noindent\hyperlink{from_entourage_uniformities_to_covering_uniformities}{From entourage uniformities to covering uniformities}\dotfill \pageref*{from_entourage_uniformities_to_covering_uniformities} \linebreak
\noindent\hyperlink{from_covering_uniformities_to_entourage_uniformities}{From covering uniformities to entourage uniformities}\dotfill \pageref*{from_covering_uniformities_to_entourage_uniformities} \linebreak
\noindent\hyperlink{equivalence_between_covering_uniformities_and_entourage_uniformities}{Equivalence between covering uniformities and entourage uniformities}\dotfill \pageref*{equivalence_between_covering_uniformities_and_entourage_uniformities} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{uniformizability}{Uniformizability}\dotfill \pageref*{uniformizability} \linebreak
\noindent\hyperlink{fine_uniformity}{Fine uniformity}\dotfill \pageref*{fine_uniformity} \linebreak
\noindent\hyperlink{compact_regular_locale}{Compact regular locale}\dotfill \pageref*{compact_regular_locale} \linebreak
\noindent\hyperlink{complete_uniform_locales}{Complete uniform locales}\dotfill \pageref*{complete_uniform_locales} \linebreak
\noindent\hyperlink{criteria_for_completeness}{Criteria for completeness}\dotfill \pageref*{criteria_for_completeness} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A \textbf{uniform locale} is to a [[uniform space]] as a [[locale]] is to a [[topological space]].

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

While an ordinary uniform space is defined directly in terms of subsets, and the underlying topology then constructed secondarily, in the absence of an underlying set it seems more convenient to define a uniform locale as additional structure on a given locale, together with an additional axiom which essentially says ``the underlying topology is the same as the one we started with.''

\hypertarget{basic_notions}{}\subsubsection*{{Basic notions}}\label{basic_notions}

For any $E\in Op(X\times X)$ and any [[sublocale]] $A$ of $X$, with inclusion map $i:A\to X$, we write $E[A]$ for the image of $(i\times 1)^*(E)$ of $A\times X$ under the projection $A\times X \to X$. If $A$ is [[overt space|overt]] (such as if $A$ is an open part of $X$ and $X$ is overt, or if [[excluded middle]] holds), then $E[A]$ is an open part of $X$, and can equivalently be defined as $\bigvee \{ V\in Op(X) \mid Pos(V\cap A) \}$, where $Pos(W)$ means ``$W$ is [[positive element|positive]]''. Otherwise, it is merely a sublocale.

Similarly, if $E,F\in Op(X\times X)$, we write $E\circ F$ for the image of $\pi_{23}^*(E) \cap \pi_{12}^*(F)$ under the projection $\pi_{13}:X\times X\times X\to X\times X$. If $X$ is overt, this is an open part of $X\times X$; otherwise it is merely a sublocale. We also write $E^{-1}$ for the pullback of $E$ along the twist map $X\times X \cong X\times X$.

\hypertarget{covering_uniformities}{}\subsubsection*{{Covering uniformities}}\label{covering_uniformities}

An open \textbf{[[open cover|cover]]} of a locale $X$ is a collection $C \subseteq Op(X)$ of open parts of $X$ whose [[join]] is $X$. For covers $C_i$, we define:

\begin{itemize}%
\item $C_1$ \textbf{refines} $C_2$, written $C_1 \prec C_2$, if every element of $C_1$ is $\le$ in some element of $C_2$.


\item $C_1 \wedge C_2 \coloneqq \{ A \wedge B \;|\; A \in C_1, B \in C_2 \}$; this is also a cover.


\item $E_C = \bigcup \{ U\times U \mid U\in C \}$, and $C[A] = E_C[A]$.


\item For $A \in Op(X)$, we write $C[A] = E_C[A]$ (see above definition). If $A$ is overt (such as if $X$ is overt, such as if [[excluded middle]] holds), this is equivalent to $\bigvee \{ B \in C \;|\; A \cap B \text{ is positive } \}$, where positive is in the sense of [[positive element]].


\item $C^* \coloneqq \{ C[A] \;|\; A \in C\}$.



\end{itemize}
We now define a \textbf{covering uniformity} on a locale $X$ to be a collection of covers, called \textbf{[[uniform covers]]}, such that

\begin{enumerate}%
\item If $C$ is a uniform cover and $C \prec C'$, then $C'$ is a uniform cover.


\item The cover $\{X\}$ is a uniform cover and if $C_1, C_2$ are uniform covers, then so is $C_1 \wedge C_2$.


\item If $C$ is a uniform cover, there exists a uniform cover $C'$ such that $(C')^* \prec C$.


\item The collection of uniform covers is \textbf{admissible}: for any open part $A\in Op(X)$, we have

\begin{displaymath}
A = \bigvee \{ B | \exists \;\text{ a uniform cover }\; C \;\text{ such that }\; C[B] \le A \}
\end{displaymath}


\end{enumerate}
The last condition is the one saying that ``the induced topology is again the topology of $X$.''; the other conditions correspond precisely to the \href{uniform+space#ucov}{uniform-cover definition} of a uniform topological space.

\hypertarget{entourage_uniformities}{}\subsubsection*{{Entourage uniformities}}\label{entourage_uniformities}

An \textbf{entourage} (Picado and Pultr, Section XII.1.1) is an open part $E\in Op(X\times X)$ such that $\{u\in Op(X)\mid u\times u\le E\}$ is an open cover of $X$.

An \textbf{entourage uniformity} (Picado and Pultr, Section XII.2.3) on a locale $X$ is a collection of [[entourages]] such that:

\begin{enumerate}%
\item If $E$ is an entourage and $E\subseteq F$, then $F$ is also an entourage.


\item The open part $X\times X$ is an entourage and if $E$ and $F$ are entourages, then so is $E\cap F$.


\item If $E$ is an entourage, then so is $E^{-1}$.


\item For any entourage $E$, there exists an entourage $F$ such that $F\circ F \subseteq E$. The sublocale $F\circ F$ is not always open, but we can still ask it to be contained in the open sublocale $E$.


\item The collection of uniform entourages is \textbf{admissible}: for any $U\in Op(X)$ we have $U = \bigvee \{ V\in Op(X) \mid E[V] \subseteq U \text{ for some uniform entourage } E\}$.



\end{enumerate}
\hypertarget{from_entourage_uniformities_to_covering_uniformities}{}\subsubsection*{{From entourage uniformities to covering uniformities}}\label{from_entourage_uniformities_to_covering_uniformities}

Given an entourage $E$ on a locale $L$, we define an open cover $U_E$ by setting

\begin{displaymath}
U_E=\{x\in L\mid x\times x\subset E\}.
\end{displaymath}
Given an entourage uniformity $\{E_i\}_i$, we construct a covering uniformity out of it by taking all open covers $V$ that are refined by some $U_{E_i}$.

\hypertarget{from_covering_uniformities_to_entourage_uniformities}{}\subsubsection*{{From covering uniformities to entourage uniformities}}\label{from_covering_uniformities_to_entourage_uniformities}

Given an open cover $U$, we construct an entourage $E_U$ by setting \$$E_U=\bigvee_{x\in U}x\times x.$\$

Given a covering uniformity $\{U^i\}_i$, we construct an entourage uniformity out of it by taking all entourages $E$ that contain some $E_{U^i}$.

\hypertarget{equivalence_between_covering_uniformities_and_entourage_uniformities}{}\subsubsection*{{Equivalence between covering uniformities and entourage uniformities}}\label{equivalence_between_covering_uniformities_and_entourage_uniformities}

Theorem XII.3.3.4 in Picado and Pultr shows that the above correspondence is bijective. Furthermore, the categories of entourage uniform locales and covering uniform locales are equivalent (Corollary XII.3.4.3 in the cited book). However, since their book uses [[classical logic]] throughout, it is not entirely clear whether the same equivalence holds constructively.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{uniformizability}{}\subsubsection*{{Uniformizability}}\label{uniformizability}

A [[locale]] admits a uniformity if and only if it is [[completely regular]] ($\backslash$citeTheorem 2.8.2\{PP\}).

\hypertarget{fine_uniformity}{}\subsubsection*{{Fine uniformity}}\label{fine_uniformity}

Uniformities are closed under unions, so any [[completely regular]] [[locale]] admits a largest uniformity, the \textbf{fine uniformity}.

The fine uniformity consists of all normal covers, where a cover $U$ is \textbf{normal} if there is a sequence of covers $\{U_n\}_{n\ge0}$ such that $U=U_0$ and $U_{n+1}U_{n+1}$ refines $U_n$.

\hypertarget{compact_regular_locale}{}\subsubsection*{{Compact regular locale}}\label{compact_regular_locale}

On a [[compact]] [[regular]] [[locale]] the system of all covers forms a uniformity. Maps out of compact regular locales are automatically uniform.

\hypertarget{complete_uniform_locales}{}\subsubsection*{{Complete uniform locales}}\label{complete_uniform_locales}

A uniform locale $L$ is \textbf{complete} if every dense uniform embedding $L\to X$ is an isomorphism of uniform locales.

The category of complete uniform locales is a [[reflective subcategory]] of uniform locales. The reflection functor is known as the \textbf{completion} functor.

Concretely, the completion of a uniform locale $L$ with a system of uniform covers $A$ can be described as follows. Its opens are downward-closed subsets $U$ of the underlying [[frame]] of $L$ that satisfy the following saturation conditions:

\begin{itemize}%
\item If for some $a\in L$ we have $\{x\in L\mid x\lt_A a\}\subset U$, then also $a\in U$. Here $x\lt_A a$ means that there is $C\in A$ such that $C[x]\le a$.


\item If for some $C\in A$ and $a\in L$ we have $a\wedge C\subset U$, then also $a\in U$.



\end{itemize}
\hypertarget{criteria_for_completeness}{}\subsection*{{Criteria for completeness}}\label{criteria_for_completeness}

Every compact regular locale is complete. The fine uniformity on a [[paracompact locale]] is complete.

Isbell's theorem states that a [[locale]] is [[paracompact]] if and only if it admits a complete uniformity.

A [[completely regular]] [[locale]] is [[compact]] if and only if it admits a complete uniformity that has a basis in which all covers are finite.

\hypertarget{references}{}\subsection*{{References}}\label{references}

A detailed treatment of uniform locales can be fund in

\begin{itemize}%
\item [[Jorge Picado]], [[Aleš Pultr]], \emph{[[Frames and Locales]]}.

\end{itemize}
The following paper developes covering uniformities constructively, and includes citations to several other papers that do it classically:

\begin{itemize}%
\item [[Peter Johnstone]], 1989; A constructive theory of uniform locales. I. Uniform covers; General topology and applications, 179--193; Lecture Notes in Pure and Applied Mathematics 134 (1991).

\end{itemize}
A constructive and predicative theory in the programme of [[formal topology]] can be found here:

\begin{itemize}%
\item [[Giovanni Curi]]; On the collection of points of a formal space; Annals of Pure and Applied Logic 137 (2006) 1--3, 126--146.


\item [[Giovanni Curi]]; Constructive metrisability in point-free topology; Theoretical Computer Science 305 (2003) 1--3, 85--109.



\end{itemize}
[[!redirects uniform locale]] [[!redirects uniform locales]]

[[!redirects pointless uniformity]] [[!redirects pointless uniformities]]



\end{document}