\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*{pretopos}

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

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{regular_and_exact_categories}{}\paragraph*{{Regular and Exact categories}}\label{regular_and_exact_categories}

[[!include regular and exact categories - contents]]

\hypertarget{category_theory}{}\paragraph*{{Category Theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{pretopos}{}\section*{{Pretopos}}\label{pretopos}

\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{infinitary}{Infinitary pretoposes}\dotfill \pageref*{infinitary} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{internal_logic_and_mathematics_in_pretopoi}{Internal logic and mathematics in pretopoi}\dotfill \pageref*{internal_logic_and_mathematics_in_pretopoi} \linebreak
\noindent\hyperlink{colimits}{Colimits}\dotfill \pageref*{colimits} \linebreak
\noindent\hyperlink{the_precanonical_topology}{The precanonical topology}\dotfill \pageref*{the_precanonical_topology} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

A \textbf{pretopos} is a [[category]] which is both [[exact category|exact]] and [[extensive category|extensive]]. (See [[familial regularity and exactness]] for why extensivity and exactness deserve to be considered together.) This implies that it is a [[coherent category]].

Frequently one is especially interested in pretoposes having additional properties, such as:

\begin{itemize}%
\item A \textbf{Heyting pretopos} is a pretopos which is also a [[Heyting category]]; a \textbf{Boolean pretopos} is a pretopos which is also a [[Boolean category]]. These are suitable as frameworks for [[finite mathematics|finitist]] [[predicative mathematics]], respectively with [[intuitionistic logic|intuitionistic]] or [[classical logic|classical]] logic.


\item A \textbf{[[Π-pretopos]]} is a pretopos which is also a [[locally cartesian closed category]]. (A $\Pi$-pretopos is automatically a Heyting pretopos.) These are suitable as frameworks for finitist [[constructive mathematics]] which is `weakly predicative'.


\item A \textbf{$W$-pretopos} is a pretopos which has (locally) [[W-types]] ([[initial algebra|initial]] [[algebra for an endofunctor|algebras]] for [[polynomial endofunctors]]), most famously a [[natural numbers object]]. (Here, we take any [[exponentiable morphism]] to define a polynomial endofunctor. This paragraph is original to this page and not in the literature; it may not be the best definition.) Heyting $W$-pretoposes and Boolean $W$-pretoposes are suitable as frameworks for non-finitist but strongly predicative mathematics (with intuitionistic and classical logic, respectively).


\item A \textbf{[[ΠW-pretopos]]} is a topos that is both a $\Pi$-pretopos and a $W$-pretopos. (Now every morphism defines a polynomial endofunctor, since every morphism is exponentiable.) These are suitable as frameworks for weakly predicative constructive mathematics that is not finitist.


\item A \textbf{[[predicative topos]]} is a [[ΠW-pretopos]] that satisfies the [[axiom of multiple choice]]. (This now differs from a $W$-[[topos]] below mainly in still lacking [[power objects]], hence still a context for weakly predicative constructive mathematics.)


\item A \textbf{[[topos]]} is a pretopos that has [[power objects]]. A topos is automatically a $\Pi$-pretopos; conversely, a $\Pi$-pretopos is a topos iff it has a [[subobject classifier]], and a Boolean $\Pi$-pretopos is always a topos. Toposes and [[Boolean toposes]] are suitable as frameworks for finitist (but otherwise impredicative) mathematics, with intuitionistic and classical logic respectively.


\item A \textbf{$W$-topos} is of course a topos that is a $W$-pretopos; it is sufficient that the topos have a [[natural numbers object]] (see van den Berg \& Moerdijk), so this is often called a \textbf{topos with NNO}. These are suitable as frameworks for (non-predicative, non-finitist) [[constructive mathematics]], while Boolean $W$-toposes are suitable as a framework for [[classical mathematics]] without the [[axiom of choice]].


\item A \textbf{topos with choice} is a topos that satisfies the [[axiom of choice]] (that every [[epimorphism]] is [[split epic|split]]). Every topos with choice is automatically boolean, so $W$-toposes with choice are suitable as a framework for full classical mathematics. (In fact, a [[well-pointed category|well-pointed]] $W$-topos with choice is precisely a model of [[ETCS]].)



\end{itemize}
\hypertarget{infinitary}{}\subsubsection*{{Infinitary pretoposes}}\label{infinitary}

An \textbf{infinitary pretopos} is an [[infinitary coherent category]] which is both [[infinitary extensive category|infinitary extensive]] and [[exact category|exact]]. Giraud's theorem says that infinitary pretoposes with small generating sets are the same as [[Grothendieck toposes]], and in particular are [[toposes]] (although this last result is not valid in [[predicative mathematics]]).

An infinitary pretopos (perhaps with [[well-powered category|well-poweredness]] included) is sometimes called an ``$\infty$-pretopos'' (e.g. in the [[Elephant]]), but we avoid that term because of potential confusion with the notion of [[(∞,1)-pretopos]].

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

\hypertarget{internal_logic_and_mathematics_in_pretopoi}{}\subsubsection*{{Internal logic and mathematics in pretopoi}}\label{internal_logic_and_mathematics_in_pretopoi}

Like any coherent (or Heyting) category, a (Heyting) pretopos has an [[internal logic]]. Extensivity and exactness make a Heyting pretopos a very set-like category. One can say imprecisely that it has ``all the good first-order properties of a [[topos]]'', meaning not that it has those properties that can be expressed in elementary terms (which is false) but that it has those properties that (unlike exponential and power objects) correspond to first-order reasoning in ordinary mathematics. Therefore, pretoposes (especially Heyting, $\Pi$, and/or $W$ ones) are related to predicative constructive mathematics in a way similar to how toposes are related to non-predicative constructive mathematics.

\hypertarget{colimits}{}\subsubsection*{{Colimits}}\label{colimits}

A pretopos is necessarily [[balanced category|balanced]], but while it has coproducts and coequalizers of equivalence relations, it need not have all finite colimits. However, if it has countable pullback-stable unions of subobjects, then any internal binary relation generates an equivalence relation and therefore has a quotient, so we can construct arbitrary coequalizers and thus arbitrary finite colimits. And we can perform an ``internal'' version of this argument in a $\Pi$-pretopos with a [[natural numbers object|NNO]], such as a $\Pi$-$W$-pretopos.

\hypertarget{the_precanonical_topology}{}\subsubsection*{{The precanonical topology}}\label{the_precanonical_topology}

A pretopos, being a [[coherent category]], admits a [[subcanonical site|subcanonical]] [[Grothendieck topology]] called the [[coherent topology]]. In a pretopos, this topology is generated by finite jointly epimorphic families. Since the [[canonical topology]] on a [[Grothendieck topos]] consists of all jointly epimorphic families, the coherent topology on a pretopos is sometimes called the \textbf{precanonical topology}.

The [[codomain fibration]] of a pretopos is always a [[stack]] for its precanonical topology. Being a pretopos is stronger than necessary for this condition to hold in a coherent category, however; see [[coherent category]] for the necessary and sufficient conditions.

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

\begin{itemize}%
\item [[Π-pretopos]], [[ΠW-pretopos]], [[list-arithmetic pretopos]]


\item [[2-pretopos]]


\item [[(∞,1)-pretopos]]


\item [[conceptual completeness]]



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

\begin{itemize}%
\item [[Benno van den Berg]], [[Ieke Moerdijk]] (2008-09-25); \emph{$W$-types in sheaves}; \href{http://www.phil.cmu.edu/projects/ast/Papers/}{vdBM\_Wtypes.ps/pdf}

\end{itemize}
[[!redirects pretopos]] [[!redirects pretoposes]] [[!redirects pretopoi]]

[[!redirects Heyting pretopos]] [[!redirects Heyting pretoposes]] [[!redirects Heyting pretopoi]]

[[!redirects Boolean pretopos]] [[!redirects Boolean pretoposes]] [[!redirects Boolean pretopoi]]

[[!redirects W-pretopos]] [[!redirects W-pretoposes]] [[!redirects W-pretopoi]]

[[!redirects infinitary pretopos]] [[!redirects infinitary pretoposes]] [[!redirects infinitary pretopoi]]

[[!redirects precanonical topology]] [[!redirects precanonical topologies]]



\end{document}