\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*{Bishop&#39;s constructive mathematics}

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

\hypertarget{constructivism_realizability_computability}{}\paragraph*{{Constructivism, Realizability, Computability}}\label{constructivism_realizability_computability}

[[!include constructivism - contents]]

\hypertarget{bishops_constructive_mathematics}{}\section*{{Bishop's constructive mathematics}}\label{bishops_constructive_mathematics}

\noindent\hyperlink{overview}{Overview}\dotfill \pageref*{overview} \linebreak
\noindent\hyperlink{WhatItIs}{What is it?}\dotfill \pageref*{WhatItIs} \linebreak
\noindent\hyperlink{Triposes}{Relation to triposes}\dotfill \pageref*{Triposes} \linebreak
\noindent\hyperlink{Continuity}{Bishop's notion of continuity}\dotfill \pageref*{Continuity} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{overview}{}\subsection*{{Overview}}\label{overview}

In 1967, [[Errett Bishop]] revived interest and practice of [[constructive mathematics]] with his book [[Foundations of Constructive Analysis]], in which he showed that contrary to previous perceptions, large swaths of mathematics could be developed constructively with only minor changes from the classical theory.

While [[Brouwer]] had insisted that mathematics was primary to [[logic]], the [[intuitionism|intuitionists]] who followed him went more into intuitionistic [[foundations]] and [[philosophy]] than into mathematics as such. The [[Russian constructivism|Russian school]] of constructivism focussed on [[recursion theory]] and was far removed from modern [[Bourbaki]]-style mathematics. There was a pervasive feeling that constructive mathematics, particularly constructive [[analysis]], was simply unworkable; Bishop attacked this idea, not by arguing against it, but by simply demonstrating how constructive analysis could be done.

Bishop's work was primarily in [[analysis]], because constructive mathematics is more difficult at an elementary level there than in some other fields such as [[combinatorics]]. Bishop's style was extended to constructive [[algebra]] by his disciple [[Fred Richman]]. On the other hand, other fields such as point-set [[topology]] are so much \emph{more} difficult constructively that Bishop did not even consider them; later authors have attacked the problem with tools such as [[apartness spaces]] and [[locales]]/[[formal topologies]]. In fact, even Bishop's treatment of analysis has actual flaws regarding the notion of continuous function (see \hyperlink{Continuity}{below}) that seem to be best fixed by using locales.

Bishop's work is important not only for its historical role in reviving interest in constructive mathematics and belief in its feasibility, but because the framework for constructive mathematics that he laid out has played a central role in a great deal of later work. Known as \textbf{Bishop's constructive mathematics} and abbreviated \textbf{BISH} or \textbf{BCM}, this framework is often viewed as a sort of ``common core'' of all kinds of constructive mathematics. However, this is not really a true statement about the mathematics that Bishop himself did, which in particular is not compatible with the [[internal logic]] of [[elementary toposes]] (see \hyperlink{WhatItIs}{below}) --- but for added confusion, some mathematicians who say they are working in ``Bishop's constructive mathematics'' are in fact working in a theory about which this statement \emph{is} true. Thus, unless one really does want to work in the mathematics that Bishop himself did, it is better to work in ``pure neutral'' constructive mathematics and say so explicitly, while clearly mentioning any additional principles one may be assuming.

This page will discuss Bishop's constructive mathematics \emph{as Bishop did it}; see [[constructive mathematics]] for ``pure neutral'' constructive mathematics that is valid in any topos. Unfortunately, the confusion surrounding BISH means that any individual paper claiming to use BISH must be read carefully to find out exactly what framework it \emph{is} using.

\hypertarget{WhatItIs}{}\subsection*{{What is it?}}\label{WhatItIs}

Bishop's constructive mathematics is often described as ``obtained from classical mathematics by removing the law of [[excluded middle]] and the [[axiom of choice]]''. It is also claimed that ``every other variety of constructive mathematics, including classical mathematics, can be obtained from Bishop's constructive mathematics by adding further assumptions'' (e.g. \hyperlink{BridgesRichman}{BridgesRichman}). However, neither of these statements is really true.

First of all, Bishop accepted the principle of [[countable choice]]. Since countable choice fails in the [[internal logic]] of many [[toposes]], this means that if we want to do constructive mathematics because it is valid in toposes, we cannot use Bishop's framework. (Regarding countable choice see also \hyperlink{Richman00}{Richman}.) Similarly, although it is true (as often claimed) that ``every constructive proof in BISH is also a classical proof'' if by ``classical'' one includes both excluded middle and choice, it is not true if ``classical'' includes foundational theories like [[ZF]] (without the axiom of choice).

However, focusing attention on countable choice is misleading, because it may lead one to think that we could simply ``remove that assumption'' from BISH, and that proofs in BISH that don't happen to invoke countable choice would be topos-valid. In fact it is not really possible to ``remove countable choice'' from BISH, because it is not an axiom but a \emph{theorem}, and BISH also proves other non-topos-valid principles like the [[presentation axiom]].

The central point is the following: although the carriers of mathematical structure in BISH are, like in other mathematical frameworks, called [[sets]], BISH is not an \emph{axiomatic [[set theory]]} but a \emph{definitional set theory}. That is, the notion of ``set'' in BISH is not an undefined one given meaning by axioms and rules the way it is in [[ZFC]] or [[ETCS]] (and also some ways of using [[type theory]] as a foundation, such as [[homotopy type theory]]). Instead, the notion of ``set'' is \emph{defined} in terms of more basic notions such as ``construction'' and ``method''. (See [[Bishop set]].) This definition then allows us to \emph{prove} that sets satisfy various properties, including countable choice. But Bishop directly uses ``constructions'' and ``methods'' throughout in addition to the ``sets'' that are defined from them, so his mathematics cannot be simply interpreted into an axiomatic set theory with certain assumptions added such as countable choice.

Bishop did not formalize his foundations, and in particular did not specify rules for how ``constructions'' and ``methods'' should behave. However, many people believe that a fairly faithful reading is obtained by viewing ``methods'' as the [[terms]] in a [[dependent type theory]], whose [[types]] are classifiers for families of ``constructions''. (Indeed, making this work was one of [[Per Martin-Lof]]`s original motivations for defining dependent type theory.) Bishop's \emph{logic} is then the \emph{untruncated} [[propositions as types]] logic of this type theory, with for instance ``or'' interpreted as the [[sum type]] and ``there exists'' interpreted as the [[dependent sum type]]. Bishop: ``choice is implied by the very meaning of existence''. (Other possible formalizations of Bishop's mathematics use Feferman's [[explicit mathematics]] or [[NuPrl]]. ``Nuprl can be seen as expressing the philosophical ideas of Brouwer and Bishop'' (expressed \href{http://www.nuprl.org/book/Overview.html}{here} ). Alternatively, one can try to isolate the principles implied by Bishop's definitional set theory to formulate an axiomatic set theory in which Bishop's work can be formalized --- one common proposal is [[CZF]] with the [[presentation axiom]] --- but this is getting further from what Bishop actually did.)

Thus, for instance, when Bishop says that a set is defined by specifying how to construct an element of it and how to say when two such elements are equal, we take this as meaning that a set is specified by a type $A$ and an equality relation $E : A \to A \to Type$ satisfying the laws of an [[equivalence relation]] (a.k.a. a [[setoid]] in the type theory). And whenever Bishop says ``for all $x$ there exists a $y$'', he means $\prod_{x:A} \sum_{y:B}$, which by the commutation of $\Pi$ and $\Sigma$ entails the existence of a function $A\to B$. This ``function'' is in the sense of the underlying type theory, i.e. an element of a function type; inside BISH it would be called a ``method'' or ``operation'', with the word ``function'' reserved for operations that respect the specified setoid equalities. Since not every operation is a function, the full axiom of choice does not hold in BISH; but it does hold whenever the equality on $A$ is ``minimal'' or ``identity'' or ``Leibniz'' (that is, the [[identity type]] of the type theory). In particular, since this is true for $\mathbb{N}$, countable choice holds.

Now we can see the more basic problem with saying that BISH specializes to other theories such as topos-logic or ZF. It's not just that BISH proves statements that ``don't hold'' in these other theories; rather, the latter \emph{have} no ``constructions/methods'' layer underneath, so there isn't even any natural way to \emph{try} to interpret BISH into them. (One might even argue that the same is true for the other flavors of constructivism that are generally believed to be specializations of BISH, such as Brouwer's [[intuitionistic mathematics]] and [[Russian constructivism]], but I'm not familiar enough with the philosophy of those theories to make that claim.) The only halfhearted possibility seems to be to interpret the objects of the topos (or sets of ZF) as being the \emph{types} in the underlying type theory; but in this case BISH is not talking about the same things as the other theory, and theorems of BISH do not specialize to the corresponding theorems of the other theory. (For classical mathematics \emph{with} choice, though, it happens that this specialization is correct: every setoid is isomorphic to a set, namely the actual quotient of its equality equivalence relation.)

\hypertarget{Triposes}{}\subsection*{{Relation to triposes}}\label{Triposes}

One of the most distinctive aspects of Bishop's framework for mathematics is the notion that a ``set'' is something \emph{equipped with an equality relation}, so that for instance we can construct a ``quotient'' of a set by simply equipping the same underlying ``collection'' with a new equality relation. There is a way to preserve this idea in a theory that is general enough to include topos logic, but the result looks rather different from Bishop's.

First we have to allow a more general ``logic'' than untruncated propositions-as-types, such as the topos logic of [[subobjects]]. Semantically, this can be described as working in a [[first-order hyperdoctrine]]. Second, such a more general logic will no longer satisfy the [[function comprehension]] (unique choice) principle \emph{with respect to setoids} (though it may with respect to the ``natural'' equality of objects of the topos). In fact it is nearly impossible for it to do so: if it does, then the morphisms in the base category of the hyperdoctrine satisfy the full axiom of choice! For if $R$ is a total relation from $A$ to $B$ in such a hyperdoctrine, define a setoid equality on $A\times B$ by setting $(x_1,y_1) = (x_2,y_2)$ iff $x_1=x_2$ (in the minimal Leibniz sense) and $R(x_1,y_1) \leftrightarrow R(x_2,y_2)$. Then $R$ induces a total functional relation from $A$ to $A\times B$ by $R'(x,(x',y)) = (x=x') \wedge R(x,y)$, and if there is an operation $f:A\to A\times B$ such that $R'(x,f(x))$ then $\pi_1 f : A \to B$ satisfies $R(x,\pi_1 f(x))$ and so is a choice function.

Thus, to obtain function comprehension, which is a \emph{sine qua non} for much mathematics, we have to essentially generalize the notion of ``function'' to be not just an operation (a term in the underlying type theory) that preserves equality, but a total functional relation. The ``sets'' in a hyperdoctrine, with the ``functions'' of this sort between them, are most studied in the case of [[triposes]] and are called the \emph{tripos-to-topos construction}.

Thus, working with ``sets'' in tripos logic (defined there as [[partial equivalence relations]], since a tripos may lack ``comprehensions'' to allow us to assert conditions on a construction to define an element of a set) can be viewed as a generalization of BISH to include topos logic and ZF. But a proof in BISH is not always valid in tripos logic, even if it doesn't explicitly invoke principles like countable choice, since it can use facts such as that every function has an underlying ``operation'' and that every existence statement comes with an ``method'' selecting its witnesses.

\hypertarget{Continuity}{}\subsection*{{Bishop's notion of continuity}}\label{Continuity}

Bishop rejected the usual notion of pointwise [[continuous function]] (and more generally [[topological spaces]]) as inadequate for analysis and instead defined a ``continuous function'' (from $\mathbb{R}$ to $\mathbb{R}$) to be ``locally uniformly continuous''. However, there is some confusion about this definition diagnosed by \hyperlink{Waaldijk}{Waaldijk}. In particular, the two books \emph{FCA} and \emph{CA} use different definitions, which can be reconciled only using the [[fan theorem]] (which Bishop rejected). There is a similar problem with the notion of [[locally compact space]]. In fact, Waaldijk showed more strongly that if there is \emph{any} notion of ``kontinuous'' function between subsets of $\mathbb{R}$ which is (1) closed under composition, (2) specializes on closed intervals to uniformly continuous functions, and (3) includes $f(x)= \frac{1}{x}$, then the fan theorem holds. This seems quite damaging to the prospect of a treatment of analysis as Bishop envisioned it.

A more modern perspective is to use [[locale]] theory (or the predicative variant [[formal topologies]]) instead. \hyperlink{Palmgren03}{Palmgren} shows that the continuous endomaps of the [[locale of real numbers]] $\mathbb{R}$ coincide with Bishop's locally uniformly continuous functions, whereas for spaces other than $\mathbb{R}$ itself locale maps are better-behaved than Bishops': in particular, they are of course closed under composition, and they contain inversion (suitably interpreted). Similarly, locally compact spaces and measure theory are arguably better done with locales than spaces. In particular, see [[localic completion]] and the references below.

Alternatively, one can consider sheaves over the localic unit interval to model the [[fan theorem]]. This approach is pushed even further in [[continuous truth]]. This may be seen as a modern approach to Brouwer's intuitions, where instead of postulating [[choice sequences]] to justify the [[fan theorem]], one works directly with representations of topological spaces and continuous functions between them. These are not unlike Bishop's basic ``operations''.

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

Books about or using Bishop's constructive mathematics include:

\begin{itemize}%
\item [[Errett Bishop]], \emph{[[Foundations of Constructive Analysis]]} (1967), the work which made him famous in the foundations of mathematics circles;


\item [[Errett Bishop]] and [[Henry Cheng]], \emph{Constructive Measure Theory} (1972), featuring a better [[measure theory]] than in \emph{FCA};


\item [[Errett Bishop]] and [[Douglas Bridges]], \emph{Constructive Analysis} (1985), a revised version of \emph{FCA}, incorporating the measure theory of \emph{CMT}.


\item [[Ray Mines]], [[Fred Richman]], and [[Wim Ruitenberg]], \emph{A course in constructive algebra} (1988)


\item [[Douglas Bridges]] and [[Luminiţa Vîţă]], \emph{Apartness and Uniformity: A Constructive Development} (2011)


\item [[Douglas Bridges]] and [[Fred Richman]], \emph{Varieties of constructive mathematics} (1987)



\end{itemize}
Other papers mentioned above:

\begin{itemize}%
\item [[Frank Waaldijk]], \emph{On the foundations of constructive mathematics - especially in relation to the theory of continuous functions} (2001). \href{http://www.fwaaldijk.nl/mathematics.html}{web site}


\item [[Fred Richman]] (2000). \href{http://math.fau.edu/richman/html/nsf.htm}{Constructive mathematics without choice}.



\end{itemize}
For more about the localic approach, see:

\begin{itemize}%
\item [[Erik Palmgren]], \emph{Continuity on the real line and in formal spaces}. (2003). Revised version of U.U.D.M. Report 2003:32. \href{http://www2.math.uu.se/~palmgren/crealform-rvd2.pdf}{link}

\end{itemize}
\begin{itemize}%
\item [[Erik Palmgren]], \emph{From intuitionistic to point-free topology} (2005) U.U.D.M. Report 2005:47. \href{http://www2.math.uu.se/~palmgren/homotopy.pdf}{link}

\end{itemize}
\begin{itemize}%
\item [[Erik Palmgren]], \emph{A constructive and functorial embedding of locally compact metric spaces into locales}. Topology and its Applications, 154 (2007), 1854--1880.


\item [[Erik Palmgren]], \emph{Resolution of the uniform lower bound problem in constructive analysis}, \href{http://onlinelibrary.wiley.com/doi/10.1002/malq.200710034/full}{link}


\item [[Bas Spitters]], \emph{Locatedness and overt sublocales}, doi:10.1016/j.apal.2010.07.002 APAL


\item [[Thierry Coquand]], [[Erik Palmgren]], [[Bas Spitters]], \emph{Metric complements of overt closed sets}, Mathematical Logic Quarterly, 57(4), 373-378, 2011. \href{http://dx.doi.org/10.1002/malq.201010011}{link}


\item T Kawai, \emph{A point-free characterisation of Bishop locally compact metric spaces}, \href{http://www.logicandanalysis.com/index.php/jla/article/viewFile/239/120}{link}


\item T Kawai, \emph{Localic completion of uniform spaces}, \href{https://arxiv.org/pdf/1703.02255}{arxiv}



\end{itemize}
[[!redirects BCM]] [[!redirects BISH]]



\end{document}