\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*{point-free topology}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topology}{}\paragraph*{{Topology}}\label{topology}

[[!include topology - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{examples_and_definitions}{Examples and Definitions}\dotfill \pageref*{examples_and_definitions} \linebreak
\noindent\hyperlink{locale_theory}{Locale theory}\dotfill \pageref*{locale_theory} \linebreak
\noindent\hyperlink{propositional_geometric_theories}{Propositional geometric theories}\dotfill \pageref*{propositional_geometric_theories} \linebreak
\noindent\hyperlink{formal_topology}{Formal topology}\dotfill \pageref*{formal_topology} \linebreak
\noindent\hyperlink{general_definition}{General definition}\dotfill \pageref*{general_definition} \linebreak
\noindent\hyperlink{pointwise_reasoning}{Pointwise reasoning}\dotfill \pageref*{pointwise_reasoning} \linebreak
\noindent\hyperlink{bundles}{Bundles}\dotfill \pageref*{bundles} \linebreak
\noindent\hyperlink{set_of_points}{Set of points}\dotfill \pageref*{set_of_points} \linebreak
\noindent\hyperlink{applications}{Applications}\dotfill \pageref*{applications} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

\textbf{Point-free topology} refers to various formulations of [[topology]] that are not based on the notion of [[topological space]] as a [[set]] of [[points]] equipped with [[extra structure]]. What they generally have in common is that instead the points are described as [[models]] of a [[geometric theory]]. This change has some important consequences.

First, it conveniently describes the points not only in one's favourite [[category of sets]], but also in arbitrary [[Grothendieck topos|Grothendieck toposes]].

Second, it opens up the possibility of using predicate geometric theories, to obtain generalized spaces (the [[classifying toposes]]) in the sense of Grothendieck. This article will mostly concern itself with the ungeneralized point-free spaces, corresponding to propositional geometric theories.

The phrase ``point-free topology'' is often taken as synonymous with \emph{pointless topology} \hyperlink{Johnstone83}{Johnstone 83}. However, let us reserve ``pointless'' for approaches that avoid mentioning points and refer directly to the geometric theory presentation and structures deriving from it.

\hypertarget{examples_and_definitions}{}\subsection*{{Examples and Definitions}}\label{examples_and_definitions}

\hypertarget{locale_theory}{}\subsubsection*{{Locale theory}}\label{locale_theory}

In [[locale theory]], one studies the set of [[open subspaces]] (with the extra structure of a [[frame]]) as the fundamental notion. If $A$ is the frame, then the [[geometric theory]] is that of completely prime filters of $A$. It has a propositional symbol $\phi_a$ for each element of $A$, and axioms -

\begin{itemize}%
\item $\phi_a \vdash \phi_b$ (if $a \leq b$)


\item $\top \vdash \phi_1$


\item $\phi_a \wedge \phi_b \vdash \phi_{a\wedge b}$


\item $\phi_{\bigvee_i a_i} \vdash \bigvee_i \phi_{a_i}$



\end{itemize}
This simply makes a direct correspondence between the algebra of $A$ and the geometric logic. Of course it also corresponds to the finite intersections and arbitrary unions of open sets, which shows how geometric logic is matched to topology.

The classifying topos is the topos of sheaves over $A$.

The frame is a presentation-independent representation of the theory. It can be recovered from the theory as the Lindenbaum algebra of formulae modulo equivalence.

\hypertarget{propositional_geometric_theories}{}\subsubsection*{{Propositional geometric theories}}\label{propositional_geometric_theories}

A presentation of a frame by generators and relations corresponds more directly to a general propositional [[geometric theory]]. The generators are the signature (propositional symbols) and the relations can be straightforwardly converted to axioms.

\hypertarget{formal_topology}{}\subsubsection*{{Formal topology}}\label{formal_topology}

In [[formal topology]], one studies a set $B$ of \emph{[[base for a topology|basic]]} open subspaces, with a \emph{cover relation} $a\triangleleft U$ between elements and subsets of $B$, to show when one basic open is covered by a family of others. There are various flavours of this. $\triangleleft$ may be the full cover relation or a generating part, and there may sometime be included the extra structure of a [[positivity predicate|positivity]]. In each case the formal topology has the structure of a [[posite]] and so gives rise to a geometric theory of flat continuous functors. Its propositional symbols are $\phi_a$ for each $a\in B$. The axioms are -

\begin{itemize}%
\item $\top \vdash \bigvee_{a\in B} \phi_a$


\item $\phi_a \wedge \phi_b \vdash \bigvee\{\phi_c\mid c\triangleleft\{a\} \wedge c\triangleleft\{b\}\}$


\item $\phi_a \vdash \bigvee_{b\in U}\phi_{b}$ (if $a\triangleleft U$)



\end{itemize}
The models are known as \emph{formal points}.

\hypertarget{general_definition}{}\subsubsection*{{General definition}}\label{general_definition}

It is probably impossible to give a real definition of ``a notion of point-free topology''. However, one way to capture the notion of ``point-free-ness'' is by a version of [[well-pointed category|well-pointedness]].

Specifically, suppose that one defines a [[category]] (or $(\infty,1)$-[[(infinity,1)-category|category]]) $S$, whose [[objects]] one thinks of as [[spaces]], and that one intends $Hom(X,Y)$ to be the [[set]] (or $\infty$-[[infinity-groupoid|groupoid]]) of \emph{all} continuous maps from $X$ to $Y$ (whereas $Ob(S)$ need not be the class of all spaces). Also suppose that $S$ has a [[terminal object]] $pt$, which one interprets as the [[point]]. Then we may call this a \textbf{pointwise} formulation of topology if $pt$ is a [[generator]] in $S$, and \textbf{pointless} if this is not provable (or, for a stronger variation, provably false).

\hypertarget{pointwise_reasoning}{}\subsection*{{Pointwise reasoning}}\label{pointwise_reasoning}

The traditional way of doing topology using points may be called \textbf{pointwise topology}. Obviously that is natural in point-set topology, but for point-free there is an apparent problem: there may not be enough points to support, semantically, all the syntactic distinctions between formulae in the geometric logic. In other words, geometric logic is not necessarily complete.

It is possible to circumvent this by reasoning in an entirely \emph{pointless} style, without reference to the points. For instance with locales, the maps are defined to be the frame homomorphisms, backwards.

Surprisingly, however, it is also possible to reason pointwise: a map from $X$ to $Y$ can be defined by saying how points of $X$ transform to points of $Y$. What makes this work is that there are enough points (models of the geometric theory) if you allow for those that live outside your favourite category of sets. In essence, if the construction is defined for the generic point of $X$ in the topos of sheaves over $X$, then the universal property of classifying toposes gives a point-free map (geometric morphism). The catch is that, to allow the construction to be transported from one topos to another, it has to be \emph{geometric} - preserved by inverse image functors. Thus continuity becomes a logical issue, of geometricity.

Further details and references are in Vickers \hyperlink{Vickers07}{2007} and \hyperlink{Vickers14}{2014}.

\hypertarget{bundles}{}\subsection*{{Bundles}}\label{bundles}

A decisive advantage of point-free topology is that it gives a fibrewise topology of \textbf{bundles}, understood broadly as maps into a base space. (Note - for generalized spaces, i.e. toposes, bundles must be understood as \emph{bounded} geometric morphisms.)

It is shown in \hyperlink{JoyalTierney84}{Joyal, Tierney} that, for any elementary topos $\mathcal{E}$, there is an equivalence between localic bundles over $\mathcal{E}$ (i.e. localic geometric morphisms into it) and internal \emph{point-free spaces} in $\mathcal{E}$. The result does not work point-set.

Joyal and Tierney proved their result for internal frames. However, in some ways it works better for presentations of frames by generators and relations, if there is some geometric theory $\mathbb{T}_0$ of which the systems of generators and relations are models. This is not the case for frames - the frame structure is not geometric. \hyperlink{Vickers07}{Vickers 2007} works it out for the general case of ``GRD-systems'', systems of generators, relations and ``disjuncts''. Each model $P$ of the geometric theory $\mathbb{T}_0$ itself presents another geometric theory (for its point-free space), and this can be used to make a theory $\mathbb{T}_1$, extending $\mathbb{T}_0$, that classifies ``pointed'' presentations. There is a forgetful map (forget the point) $p\colon \mathcal{S}[\mathbb{T}_1] \to \mathcal{S}[\mathbb{T}_0]$ between the classifying toposes. Then a presentation in $\mathcal{E}$ is a map $P\colon\mathcal{E}\to\mathcal{S}[\mathbb{T}_0]$, and the localic bundle constructed by Joyal and Tierney is a bipullback of $p$ along $P$.

What this account reveals is that the bundle is - using $P$ - a continuous space-valued map on $\mathcal{E}$. For each point $x$ of $\mathcal{E}$, the fibre is $P(x)$ - because fibres are just pullbacks.

\hypertarget{set_of_points}{}\subsection*{{Set of points}}\label{set_of_points}

Depending on the foundational setting, a point-free space may or may not have a set of points, a discrete coreflection. This can be done in topos theory, but relies on an impredicative use of power\_sets\_. (Formal topology arose out of a desire to work predicatively.)

However, even when it exists, the set of points does not generally represent the space well.

This is best understood in terms of bundles over $X$. The ``set of points'' of a bundle $p\colon Y\to X$ is a sheaf over $X$, hence a local homeomorphism $q\colon Z\to X$. As a discrete coreflection it must also have a bundle map $f$ from $q$ to $p$. However, local homeomorphisms have an \emph{opfibrational} property that limits their ability to approximate general bundles. Suppose $x \sqsubseteq x'$ are two points of $X$ that are related by the specialization order. Then there is a corresponding fibre map $q^{-1}(x) \to q^{-1}(x')$.

As an example, take $X$ to be the Sierpinski space $\mathbb{S}$. Its points are subsets of a singleton $\{\ast\}$ and include $\bot=\emptyset\sqsubseteq\top=\{\ast\}$. Its sheaves are functions - the fibre maps $Z_{\bot}\to Z_{\top}$.

Now consider the bundle $p\colon 1\to\mathbb{S}$ that picks out the closed point $\bot$. Its fibres over $\bot$ and $\top$ are singleton and empty. Let $q\colon Z \to \mathbb{S}$ be its discrete coreflection. Because there is a bundle map from $q$ to $p$, the fibre $Z_\top$ must be empty. But then because $q$ is a local homeomorphism, $Z_\bot$ must also be empty. $Z$, the ``set of points'' of $p$, is the empty space over $\mathbb{S}$.

We see that a non-trivial space can have have an empty set of points for purely topological reasons, nothing to do with logic or a pathological nature of point-free spaces.

\hypertarget{applications}{}\subsection*{{Applications}}\label{applications}

\begin{itemize}%
\item [[Banach-Tarski paradox]]

\end{itemize}
\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[localic homotopy theory]]

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

An introduction to [[locale theory]] is

\begin{itemize}%
\item [[Peter Johnstone]] (1983); \emph{The point of pointless topology}; Bull. Amer. Math. Soc. (N.S.) Volume 8, Number 1, 41--53; \href{http://projecteuclid.org/euclid.bams/1183550014}{Euclid}.

\end{itemize}
This is, in its own words, to be read as the trailer for Johnstone's book \emph{[[Stone Spaces]]}, which see.

For a constructive treatment more appropriate to the ideas on this page see

\begin{itemize}%
\item [[Andre Joyal|Andr\'e{} Joyal]], [[Myles Tierney]], \emph{An extension of the Galois theory of Grothendieck}, Memoirs of the American Mathematical Society \textbf{51} (1984), no. 309

\end{itemize}
For [[formal topology]], see

\begin{itemize}%
\item [[Giovanni Sambin]] (2001); \emph{Some points in formal topology}; \href{http://www.math.unipd.it/~sambin/txt/SP.pdf}{pdf}.


\item [[Erik Palmgren]], \emph{From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory}, Logicism, Intuitionism, and Formalism Volume 341 of the series Synthese Library pp 237-253, 2005 (\href{http://www2.math.uu.se/~palmgren/homotopy_rev2.pdf}{pdf})



\end{itemize}
The pointwise reasoning is explained in the next references, though it was surely understood before them.

\begin{itemize}%
\item [[Steve Vickers]], \emph{The double powerlocale and exponentiation: a case study in geometric logic}, Theory and Applications of Categories \textbf{12} (2004) pp. 372-422 (\href{http://www.tac.mta.ca/tac/volumes/12/13/12-13.pdf}{pdf})


\item [[Steve Vickers]], \emph{Locales and toposes as spaces}, Chapter 8 in \emph{Handbook of Spatial Logics} (ed. Aiello, Pratt-Hartman, van Bentham), Springer, 2007, pp. 429-496.


\item [[Steve Vickers]], \emph{Continuity and geometric logic}, Journal of Applied Logic \textbf{12 (1)} (2014), pages 14-27 (\href{http://www.cs.bham.ac.uk/~sjv/GeoAspects.pdf}{pdf})



\end{itemize}
[[!redirects pointless topology]]

[[!redirects pointwise topology]] [[!redirects point-wise topology]]

[[!redirects pointfree topology]] [[!redirects point-free topology]]

[[!redirects pointless topology]]



\end{document}