\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*{cocomplete well-pointed topos}

\hypertarget{the_cocomplete_locally_small_wellpointed_topos}{}\section*{{The (co)complete, locally small, well-pointed topos}}\label{the_cocomplete_locally_small_wellpointed_topos}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{in_constructiveintuitionistic_mathematics}{In Constructive/Intuitionistic Mathematics}\dotfill \pageref*{in_constructiveintuitionistic_mathematics} \linebreak


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

The [[Set|category of sets]] is, among other things, a [[well-pointed topos]] with a [[natural numbers object]] satisfying the [[axiom of choice]]---i.e. a model of [[ETCS]]. However, $Set$ cannot be characterized \emph{uniquely} by this or any other elementary property, i.e. by a property that doesn't refer, explicitly or implicitly, to the notion of set. This is a version of G\"o{}del's [[incompleteness theorem]].

However, $Set$ can be characterized uniquely by the addition of non-elementary categorial properties, the most notable and obvious of which are [[complete category|completeness]] and [[cocomplete category|cocompleteness]]. On the other hand, it is also true that any [[topos]] is complete and cocomplete relative to itself, in the sense that its [[self-indexing]] is complete and cocomplete as an [[indexed category]]. Thus, in order to characterize $Set$ in this way we have to mean ``external'' completeness and cocompleteness (which is the intuitive notion of completeness, in the context of some notion of set).

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

\begin{utheorem}
Let $S$ be a [[locally small category|locally small]], well-pointed topos (such as a locally small model of ETCS); the following are equivalent.

\begin{enumerate}%
\item $S$ is equivalent either to $Set$ or to the category of sets in some [[Grothendieck universe]].
\item $S$ admits all coproducts indexed by its own [[homsets]].
\item $S$ admits all products indexed by its own [[homsets]].

\end{enumerate}
\end{utheorem}
\begin{proof}
The implications from 1 to 2 and 1 to 3 are easy exercises, following from the ``second-order replacement axiom'' of a Grothendieck universe. And the implication from 3 to 2 follows because any [[topos]] which has some type of [[limit]] automatically also has the same sort of [[colimit]], because $S^{op}$ is [[monadic adjunction|monadic]] over $S$ (via the contravariant powerset functor). Thus, it remains to prove that 2 implies 1. So suppose that $S$ admits coproducts indexed by its homsets. In particular, for any $X\in S$ we can form the coproduct $\coprod_{x\colon 1\to X} 1$, which of course comes with a canonical map to $X$. This map is a bijection on [[global elements]], so since $S$ is well-pointed, it is an isomorphism.

Consider the ``global sections'' functor $\Gamma = S(1,-) \colon S\to Set$. Well-pointedness implies that this functor is [[faithful functor|faithful]] and [[conservative functor|conservative]]. However, since by the above we have $X\cong \coprod_{\Gamma(X)} 1$, it follows that $\Gamma$ is [[full functor|full]] as well, so that $S$ is equivalent to a [[full subcategory]] of $Set$. From now on we identify it with its [[essential image]].

Let $X\in S$ and suppose that $Y\subset X$ is a subset of $X$. By assumption on $S$, it admits the coproduct $\coprod_{x\colon 1\to X} Z_x$ where $Z_x$ is $1$ if $x\in Y$ and $\emptyset$ otherwise. But this coproduct maps to $Y$ via a bijection on global elements as before, so it is an isomorphism, and thus $Y\in S$ as well. Hence $S$ is closed in $Set$ under subsets. It follows that the full inclusion $S\hookrightarrow Set$ is a bijection on [[subobject]] lattices, and thus a [[logical functor]] (preserves [[power objects]]). Finally, the hypothesis on coproducts implies that the union of an $S$-set of $S$-sets is again an $S$-set.

If $S$ is essentially small, then these properties imply that it must be a Grothendieck universe. If $S$ is large, then it contains sets of arbitrarily large cardinality, hence (by closure under subsets) it contains sets of all cardinalities---thus it is all of $Set$.

(We have proven the axioms of a universe in a ``structural'' form. We can alternately directly construct an [[inaccessible cardinal]] such that $S$ is the category of sets in $V_\kappa$. We argue as before that $S$ is a full subcategory of $Set$, and let $\kappa$ be the smallest cardinal number not the cardinality of a set in $S$; it follows that $S$ consists precisely of the sets of cardinality $\lt\kappa$. Since $S$ is a topos with a NNO, $\kappa$ must be an uncountable strong [[limit cardinal|limit]]. Finally, if $X\in S$ and $Y_x \in S$ for each $x\in X$, then $\coprod_{x\colon 1\to X} Y_x\in S$, showing that $\kappa$ is [[regular cardinal|regular]], and hence inaccessible.)

\end{proof}
\begin{ucor}
$Set$ is, up to equivalence, the unique locally small and cocomplete well-pointed topos (hence the unique locally small and cocomplete model of ETCS), and the unique locally small and complete well-pointed topos (hence the unique locally small and complete model of ETCS).

\end{ucor}
\begin{proof}
Since the category of sets in some Grothendieck universe does not admit all small coproducts (for instance, not those of the size of the universe itself), if any of the equivalent statements the theorem hold for some cocomplete topos, that topos must be all of Set.

\end{proof}
A more direct proof of the corollary is possible.

\begin{proof}
We show as in the theorem that $\Gamma$ is a full inclusion. Cocompleteness of $S$ then shows that it has a left adjoint given by $X\mapsto \coprod_X 1$, so it suffices to show that the unit $X\to S(1,\coprod_X 1)$ of this adjunction is a bijection.

For injectivity, we need to show that if $j_x=j_y$, then $x=y$. If $x\neq y$, then since coproducts in a topos are [[disjoint coproduct|disjoint]], the pullback of $j_x$ and $j_y$ is the initial object $0$. But since $j_x=j_y$, their pullback is also $1$. By well-pointedness, $0$ is not isomorphic to $1$, so by contradiction, $x=y$.

For surjectivity, we need to show that any map $k\colon 1\to \coprod_X 1$ is equal to $j_x$ for some $x$. Now for each $x$, the pullback of $k$ and $j_x$ is a [[subterminal object|subobject of 1]], call it $U_x$. Since a well-pointed topos is [[two-valued topos|two-valued]], every $U_x$ must be $0$ unless some $U_x$ is $1$. Since coproducts in a topos are [[pullback stability|stable under pullback]], $1 = \coprod_X U_x$. But then if $U_x=0$ for every $x$, we would have $1 = \coprod_X 0 = 0$, contradicting well-pointedness. Thus there must be an $x$ with $U_x=1$, which implies that $k=j_x$.

\end{proof}
\hypertarget{in_constructiveintuitionistic_mathematics}{}\subsection*{{In Constructive/Intuitionistic Mathematics}}\label{in_constructiveintuitionistic_mathematics}

In [[constructive mathematics]], $Set$ is not a model of $ETCS$, but it is a model of the [[IETCS|intuitionistic version]] thereof -- that is, it is a (constructively) well-pointed topos with a NNO. It is also locally small, complete and cocomplete.

However, the above theorem and corollary both fail intuitionistically, at least as stated above. The proof of the theorem goes through up to the point where we identify $S$ with a full subcategory of $Set$. The next paragraph, however, proves only that $S$ is closed under indexed unions and [[detachable subsets]] (more precisely, under subsets whose [[characteristic function]] lands in the set of truth values belonging to $S$ --- whereas for arbitrary $S$, the only truth values we can be sure belong to $S$ are ``true'' and ``false'').

Depending on how we choose to define ``Grothendieck universe'' intuitionistically, this may imply that if $S$ is essentially small then it is a Grothendieck universe. However, it definitely does \emph{not} follow intuitionistically that if $S$ is large, it must be all of $Set$; the argument for this in the classical case implicitly uses the [[axiom of choice]] in the guise of the [[well-ordering]] (or at least [[total ordering]]) of [[cardinal numbers]].

In particular, the corollary fails to hold intuitionistically. A concrete [[weak counterexample]] (which can be made into a strong counterexample by working internally to some topos) is given by the following.

Let $\mathcal{U}$ be a truth value (identified with the subset $\{\star \;|\; \mathcal{U}\} \subseteq \{\star\} = 1$) such that $\not\not\mathcal{U}$ is valid and $\mathcal{U}$ is [[indecomposable object|indecomposable]] and [[projective object|projective]], and let $S$ be the topos $Set/\mathcal{U}$. Then $S$ is a [[Grothendieck topos]], hence cocomplete and locally small, and the assumptions on $\mathcal{U}$ ensure that it is well-pointed, but in an intuitionistic theory they don't imply that $\mathcal{U} = \top$.

Note that in this example, the ``global sections'' functor $S\to Set$ is \emph{not} the forgetful functor $Set/\mathcal{U} \to Set$ (which doesn't even preserve the terminal object), but the [[exponential]] functor $\Pi_U = Hom(U,-)$. This is the [[direct image functor]] in the [[geometric morphism]] $Set/\mathcal{U} \to Set$, whereas the obvious forgetful functor is the left adjoint to the inverse image functor that exhibits $S$ as a [[locally connected topos]].



\end{document}