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

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

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

[[!include category theory - contents]]

\hypertarget{additive_and_abelian_categories}{}\paragraph*{{Additive and abelian categories}}\label{additive_and_abelian_categories}

[[!include additive and abelian categories - contents]]

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

[[!include topos theory - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{basic_consequences_of_the_at_axioms}{Basic consequences of the AT axioms}\dotfill \pageref*{basic_consequences_of_the_at_axioms} \linebreak
\noindent\hyperlink{category_of_type_a_objects_is_abelian}{Category of type A objects is abelian}\dotfill \pageref*{category_of_type_a_objects_is_abelian} \linebreak
\noindent\hyperlink{category_of_type_t_objects_is_a_pretopos}{Category of type T objects is a pretopos}\dotfill \pageref*{category_of_type_t_objects_is_a_pretopos} \linebreak
\noindent\hyperlink{splitting_into_type_a_and_type_t_objects}{Splitting into type A and type T objects}\dotfill \pageref*{splitting_into_type_a_and_type_t_objects} \linebreak
\noindent\hyperlink{topostheoretic_considerations}{Topos-theoretic considerations}\dotfill \pageref*{topostheoretic_considerations} \linebreak


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

In a \href{http://www.mta.ca/~cat-dist/catlist/1999/atcat}{discussion} with [[Vaughan Pratt]] on the categories mailing list, [[Peter Freyd]] gave a sharp and clever description of the commonalities and differences between [[abelian categories]] and [[topos]]es (or, in the first place, between abelian categories and [[pretopos]]es), by introducing a finitely axiomatized theory of ``AT categories''. Thus abelian categories and pretoposes are examples of AT categories; underscoring how much these structures have in common, Freyd's theory hews so closely to both of these two basic examples that in fact every AT category splits cleanly as a [[product]] of a pretopos part and an abelian part.

Here, the properties held in common between abelian categories and pretoposes are all exactness conditions; in the AT set-up, the decisive difference between abelian categories and pretoposes is concentrated solely in the behavior of the [[initial object]] with respect to [[cartesian product]] (being in one case the cartesian monoidal unit, i.e. an element that is universally absorbed into any other, and in the other an absorbing element, i.e. an element that absorbs any other element into itself, aka a zero element or annihilating element).

There is no research we know of on AT categories. One might say that they were invented by Freyd really for the sole theoretical purpose of demonstrating the commonalities and differences between abelian categories and pretopos categories, not because AT categories are found in nature. Indeed, a ``typical'' AT category is something of a mythological creature with the head of an abelian lion and the body of a pretopos dragon, and serves no purpose as such, even though pure lions and pure dragons themselves serve a purpose. Some of the axioms, particular axiom ``AE'' below, seem expressly designed to fuse them together in ad hoc fashion.

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

Freyd introduces some baseline assumptions on the categories in question:

\begin{itemize}%
\item [[finitely complete category|Finite completeness]],


\item Presence of an [[initial object]],


\item Presence of [[pushout|pushouts]] for pairs of [[morphism|arrows]] one of which is [[monomorphism|monic]],


\item Presence of pushouts for [[kernel pair]]s



\end{itemize}
Each of these assumptions obviously holds in any [[abelian category]] and in any [[pretopos]].

\begin{remark}
\label{}\hypertarget{}{}
If we introduce predicates to express these four baseline assumptions, such as a predicate formula $P(p, q; f, g)$ whose meaning is ``$(p, q)$ is a pushout pair for pairs of arrows $(f, g)$'', then the remaining AT axioms given below all have a simple logical structure: they can be expressed as [[Horn theory|Horn clauses]] in the language generated by the baseline predicates. The first 8 axioms are in fact universal Horn clauses in these predicates.

This might look like a side comment for logicians, but it might also signal that Freyd intends to invoke, if pressed for details of proofs, one of a battery of representation theorems, such as the representation theorem for regular categories whose precise formulation is in terms of Horn theories -- see [[Categories, Allegories]] for examples.

Furthermore, by choosing a \emph{specific} initial object, a specific pullback for each pair of arrows with common target, etc., an AT category can be cast as a model for a certain [[essentially algebraic theory]]. In other words, such ``algebraic AT categories'' can be internalized in any finitely complete category.

\end{remark}
The crucial difference between ``abelianness'' and ``toposness'' is concentrated in the following definition:

\begin{defn}
\label{}\hypertarget{}{}
Let $0$ be the initial object, and let $\pi_1: 0 \times X \to 0$, $\pi_2: 0 \times X \to X$ be the two product projections. We say $X$ is of \textbf{type T} if $\pi_1$ is an isomorphism, and \textbf{type A} if $\pi_2$ is an isomorphism.

\end{defn}
A pretopos will turn out to be precisely an AT category in which every object is of type T, and an abelian category will turn out to be an AT category where every object is of type A.

Here then are the AT exactness axioms. Again, each of them is satisfied in every abelian category and in every pretopos, and according to Freyd's thesis, any exactness condition satisfied in both classes of categories is a logical consequence of this set of axioms. Some of Freyd's remarks in his original posting are included in parentheses.

\begin{defn}
\label{}\hypertarget{}{}
A category meeting the baseline assumptions above is an \textbf{AT category} if the following 8 axioms plus axiom ``AE'' are satisfied.

\begin{enumerate}%
\item The category is an effective [[regular category]]. (``Yes this can be stated as universal Horn conditions on pullbacks and the special pushouts mentioned above.'')


\item The arrow $0 \to 1$ is monic. (``Note that it follows that all maps from $0$ are monic.'')


\item If $i\colon A \to C$ is monic, then any pushout square

\begin{displaymath}
\itexarray{
A & \stackrel{i}{\to} & C \\
\downarrow & & \downarrow \\
B & \stackrel{j}{\to} & D
}
\end{displaymath}
is also a pullback, and $j$ is monic.


\item The functor $0 \times -$ preserves pushouts of kernel pairs, and pushouts of pairs of arrows one of which is monic.


\item If $f\colon B \to 0 \times C$ is epic and

\begin{displaymath}
\itexarray{
A & \to & B \\
\downarrow & & \downarrow f \\
0 & \to & 0 \times C
}
\end{displaymath}
is a pullback, then it's also a pushout.


\item In the full subcategory of type T objects, pushouts of pairs of morphisms, one of which is monic, are universal (i.e., stable under pullback).


\item Define a functor $T$ by the pushout diagram

\begin{displaymath}
\itexarray{
0 \times X & \stackrel{\pi_1}{\to} & 0 \\
\pi_2 \downarrow & & \downarrow \\
X & \to & T X
}
\end{displaymath}
Then $T$ preserves pullbacks.


\item Given a morphism $f\colon X \to Y$, if $T f$ and $0 \times f$ are isomorphisms, then so is $f$.



\end{enumerate}
\end{defn}
This is the basic list of exactness assumptions which permit a sharp comparison between pretoposes and abelian categories. From this list alone one can prove that every AT category embeds faithfully in a product of a pretopos and an abelian category. To show that every AT category is \emph{equivalent} to such a product, Freyd appends the following axiom involving an existential Horn condition:

\begin{defn}
\label{AxiomAE}\hypertarget{AxiomAE}{}
\textbf{axiom (AE)}

For every object $X$, there is a map $\xi\colon T X \to X$ such that

\begin{displaymath}
0 \times X \stackrel{\pi_1}{\to} X \stackrel{\xi}{\leftarrow} T X
\end{displaymath}
is a coproduct diagram, and the canonical map $X \to T X$ is a retraction of $\xi$.

\end{defn}
To bring actual toposes into the picture, Freyd adds some more axioms, but let's first take stock and see what this gives us so far.

\hypertarget{basic_consequences_of_the_at_axioms}{}\subsection*{{Basic consequences of the AT axioms}}\label{basic_consequences_of_the_at_axioms}

\begin{prop}
\label{}\hypertarget{}{}
For any $X$ the unique map $0 \to X$ is monic.

\end{prop}
\begin{proof}
By axiom 2, the map $0 \to 1$ is monic. The pullback-preserving functor $- \times X$ preserves monos, so

\begin{displaymath}
0 \times X \stackrel{! \times 1_X}{\to} 1 \times X \cong X
\end{displaymath}
(which is just the second projection $\pi_2: 0 \times X \to X$) is monic. The unique map $0 \to 0 \times X$ is monic since it has a retraction $\pi_1: 0 \times X \to0$. The result follows.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
Binary coproducts exist.

\end{prop}
\begin{proof}
Because we can take the pushout of a pair of monos $0 \to X$, $0 \to Y$.

\end{proof}
\begin{prop}
\label{}\hypertarget{}{}
Coproducts are disjoint.

\end{prop}
\begin{proof}
By axiom 3, the two coprojections $i_X \colon X \to X + Y$, $i_Y \colon Y \to X + Y$ are monic, and their pullback is initial.

\end{proof}
\hypertarget{category_of_type_a_objects_is_abelian}{}\subsection*{{Category of type A objects is abelian}}\label{category_of_type_a_objects_is_abelian}

In this section we show that the full subcategory of type A objects forms an abelian category.

\begin{lemma}
\label{tozero}\hypertarget{tozero}{}
An object is of type A if and only if there exists a map to $0$.

\end{lemma}
\begin{proof}
If $X$ is of type A, then we clearly have $X \cong 0 \times X \stackrel{\pi_1}{\to} 0$. Conversely, suppose there exists $p: X \to 0$. Note that since $0 \to 1$ is monic, there is at most one map $Y \to 0$ for any object $Y$. It follows quickly that maps $Y \to X$ are in natural bijective correspondence with maps $Y \to X \times 0$ by composition with $\pi_1: X \times 0 \to X$, so that $\pi_1$ is an isomorphism by the Yoneda lemma.

\end{proof}
\begin{prop}
\label{coreflective}\hypertarget{coreflective}{}
The full subcategory of type A objects is coreflective.

\end{prop}
\begin{proof}
By Lemma \ref{tozero}, the subcategory of type A objects in an AT category $C$ is equivalent to the subcategory $C/0 \hookrightarrow C/1 \simeq C$, which is the category of coalgebras for the functor $A(X) = 0 \times X$. Thus the category of type A objects is comonadic.

\end{proof}
\begin{lemma}
\label{}\hypertarget{}{}
Objects of type A are closed under binary products, finite coproducts, subobjects, and quotient objects (= cokernels of kernel pairs).

\end{lemma}
\begin{proof}
This follows from the fact that the category of type A objects is the slice category $C/0$.

\end{proof}
Before we prove the next lemma, recall that in a category with zero objects, a \textbf{kernel} of an arrow $f: A \to B$ is an equalizer of the pair $f, 0: A \stackrel{\to}{\to} B$. This is the same as a pullback

\begin{displaymath}
\itexarray{
K & \to & A \\
\downarrow & & \downarrow f \\
0 & \to & B
}
\end{displaymath}
Cokernels are defined dually, and can be formulated dually as certain pushouts. Since pushouts along monos exist, we can take the cokernel of any mono, and in particular the cokernel of any kernel.

\begin{lemma}
\label{}\hypertarget{}{}
In the category of type A objects, every mono is the kernel of its cokernel, and every epi is the cokernel of its kernel.

\end{lemma}
\begin{proof}
Of course, $0$ is a zero object in the category of type A objects. If $i\colon A \to B$ is a mono in the category of type A objects, then the pushout

\begin{displaymath}
\itexarray{
A & \stackrel{i}{\to} & B \\
\downarrow & & \downarrow \\
0 & \to & coker(i)
}
\end{displaymath}
exists and is also a pullback, by axiom 3, and hence $i$ is the kernel of its cokernel. Now suppose $f: A \to C$ is an epi in the category of type A objects. Since $0 \times C \cong C$, we have an epi $f\colon A \to 0 \times C$. Then, by axiom 5, the pullback

\begin{displaymath}
\itexarray{
ker(f) & \to & A \\
\downarrow & & \downarrow f \\
0 & \to & 0 \times C
}
\end{displaymath}
is also a pushout, so $f$ is the cokernel of its kernel.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
The category of type A objects is an abelian category.

\end{theorem}
\begin{proof}
Any category with zero objects, binary products and coproducts, and in which every mono is the kernel of its cokernel and every epi is the cokernel of its kernel, is in fact an abelian category. See Freyd-Scedrov, \emph{Categories, Allegories}, 1.598 (p. 95).

\end{proof}
\hypertarget{category_of_type_t_objects_is_a_pretopos}{}\subsection*{{Category of type T objects is a pretopos}}\label{category_of_type_t_objects_is_a_pretopos}

Now we show that the full subcategory of type T objects is a pretopos. It is clear that $0 \times 0 \cong 0$ (since $0 \to 1$ is monic), so $0$ is a type T object.

\begin{lemma}
\label{exactlyone}\hypertarget{exactlyone}{}
If $A$ is type A and $T$ is type T, then there exists exactly one map $A \to T$. Type T objects are characterized by this property.

\end{lemma}
\begin{proof}
There is exactly one morphism $A \to 0$. Hence morphisms $A \to T$ are in bijection with maps $A \to 0 \times T \cong 0$, of which there is exactly one. For the second statement, suppose that $X$ has the property that there is exactly one map $A \to X$ for each type A object. Such objects $X$ are closed under products, and $0$ is such an object; therefore $0 \times X$ is such an object. On the other hand, $0 \times X$ is of type A since it projects to $0$. Hence there is at most one morphism $0 \times X \to 0 \times X$, and it follows that $0 \times X \to 0 \to 0 \times X$ is the identity, so that $0 \times X \cong 0$. Thus $X$ is of type T.

\end{proof}
\begin{cor}
\label{strict}\hypertarget{strict}{}
The initial object $0$ is [[strict initial object|strict]] in the category of type T objects.

\end{cor}
\begin{proof}
Given $T$ of type T and $T \to 0$, we know $T$ is type A, and therefore by Lemma \ref{exactlyone} there is exactly one map $T \to T$. Hence $T \to 0 \to T$ is the identity, and of course so is $0 \to T \to 0$. So $T$ is initial.

\end{proof}
\begin{cor}
\label{closed}\hypertarget{closed}{}
The full subcategory of objects of type T is closed under products, coproducts, subobjects, and quotient objects.

\end{cor}
\begin{proof}
Closure under products and subobjects is immediate from Lemma \ref{exactlyone}. Closure under quotients and coproducts follows from axiom 4.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
The full subcategory of objects of type T is a pretopos.

\end{theorem}
\begin{proof}
Corollary \ref{closed} gives finite completeness, coproducts, and quotients of kernel pairs. Axiom 6 gives that in the full subcategory of $T$ objects, pushouts along monos are stable under pullback, and the initial object is stable under pullback in the category of T objects, because it is strict by Corollary \ref{strict}. It follows that coproducts are universal in the category of T objects. They are also disjoint by an earlier result, so the category of T objects is extensive. It is also effective regular by axiom 1, hence a pretopos.

\end{proof}
\hypertarget{splitting_into_type_a_and_type_t_objects}{}\subsection*{{Splitting into type A and type T objects}}\label{splitting_into_type_a_and_type_t_objects}

In this section we show that every AT category $C$ is the product of the abelian category $C_A$ of type A objects and the pretopos $C_T$ of type T objects.

Let us first observe that the coreflector (see Proposition \ref{coreflective})

\begin{displaymath}
0 \times {-}\colon C \to C_A
\end{displaymath}
is left exact (as all coreflectors are), and

\begin{itemize}%
\item Preserves the initial object (by axiom 2),


\item Preserves pushouts of kernel pairs, and pushouts of pairs of arrows one of which is monic (axiom 4),


\item And therefore also preserves coproducts.



\end{itemize}
A functor between AT categories which is left exact and which preserves such classes of finite colimits may be called a \textbf{morphism of AT categories}. Hence the coreflector is a morphism of AT categories.

Next let us observe that the subcategory $C_T \hookrightarrow C$ is \emph{reflective}; the reflector is the functor $T$ defined above by means of a suitable pushout. The reflector clearly preserves any colimits that exist, and preserves pullbacks (by axiom 7), so

\begin{displaymath}
T\colon C \to C_T
\end{displaymath}
is also a morphism of AT categories. Therefore we have a morphism of AT categories

\begin{displaymath}
F = \langle 0 \times {-}, T \rangle\colon C \to C_A \times C_T
\end{displaymath}
and now we wish to prove, under a suitable additional axiom (also satisfied by every abelian category and every pretopos), that this is an equivalence.

\begin{lemma}
\label{}\hypertarget{}{}
The functor $F$ is faithful.

\end{lemma}
\begin{proof}
The functor $F$ is left exact and therefore preserves kernels. By axiom 8, $F$ reflects isomorphisms. It follows immediately from these two facts that $F$ is faithful.

\end{proof}
\begin{remark}
\label{}\hypertarget{}{}
With this result, Freyd's ``first task'' is complete: any AT category may be faithfully represented in a product of a pretopos and an abelian category.

\end{remark}
At this point we bring in axiom \textbf{AE}, def. \ref{AxiomAE}, for its debut appearance. It may be helpful to consider that $T X$ is by definition the [[cokernel]] appearing in the exact sequence

\begin{displaymath}
0 \times X \stackrel{\pi_2}{\to} X \to coker(\pi_2)
\end{displaymath}
and that axiom AE asserts that this exact sequence splits (with splitting $\xi: coker(\pi_2) \to X$), in such a way that $X$ is the coproduct of the end terms.

\begin{prop}
\label{}\hypertarget{}{}
The functor $F$ is full.

\end{prop}
\begin{proof}
\begin{displaymath}
\itexarray{
0 \times X & \stackrel{\pi_2}{\to} & X & \to & T X \\
f \downarrow & & & & \downarrow g \\
0 \times Y & \underset{\pi_2}{\to} & Y & \stackrel{\overset{\xi}{\leftarrow}}{\to} & T Y
}
\end{displaymath}
Since $X = (0 \times X) + T X$, the two obvious arrows $0 \times X \to Y$, $T X \to Y$ combine to give an arrow $(f, g): X \to Y$. It is straightforward to check that $0 \times (f, g) = f$ (because the functor $0 \times -$ kills the type T summands) and that $T(f, g) = g$.

\end{proof}
\begin{theorem}
\label{}\hypertarget{}{}
The functor $F$ is an equivalence.

\end{theorem}
\begin{proof}
All that is left to check is that $F$ is essentially surjective, but this is clear because given a type A object $X$ and a type T object $Y$, we have $0 \times (X + Y) \cong X$ (use axiom 4 plus the fact that $0 \times Y \cong 0$), and

\begin{displaymath}
T(X + Y) \cong T X + T Y \cong 0 + T Y \cong Y
\end{displaymath}
which completes the proof.

\end{proof}
This completes Freyd's ``second task''.

\hypertarget{topostheoretic_considerations}{}\subsection*{{Topos-theoretic considerations}}\label{topostheoretic_considerations}

In order to beef up the type T objects to a topos, Freyd imposes some extra structure on top of the AT axioms. Since it is now the topos axioms that are in the ascendant, I will christen these categories \emph{TA categories}.

Thus, a \textbf{TA category} is an AT category $C$ together with

\begin{itemize}%
\item Functions $P, E\colon Ob(C) \to Ob(C)$,


\item Functions $l, r\colon Ob(C) \to Mor(C)$, of the form $l X\colon E X \to P X$, $r X\colon E X \to X$,


\item An operation $\Lambda$ which assigns to each pair of morphisms $f\colon R \to Y$, $g\colon R \to X$ (where $R$ and $Y$ are assumed to be type T), a morphism $\Lambda(f, g)\colon Y \to P X$.



\end{itemize}
This data is to satisfy the following axioms:

\begin{enumerate}%
\item $\langle l X, r X \rangle: E X \to P X \times X$ is monic and $P X$, $E X$ are of type T,


\item The composite of relations

\begin{displaymath}
Y \stackrel{\Lambda(f, g)}{\to} P X \stackrel{(l X)^{op}}{\to} E X \stackrel{r X}{\to} X
\end{displaymath}
is equal to

\begin{displaymath}
Y \stackrel{f^{op}}{\to} R \stackrel{g}{\to} X,
\end{displaymath}

\item If

\begin{displaymath}
\itexarray{
R & \stackrel{g}{\to} & E X \\
f \downarrow & & \downarrow l X \\
Y & \underset{h}{\to} & T X
}
\end{displaymath}
is a pullback and $R$ is of type T, then $\Lambda(f, (r X) \circ g) = h$.



\end{enumerate}
Freyd: ``Note that in the full category of type-T objects, $P$ yields power-objects with $E$, $l$, $r$ naming the universal relations. (The third axiom provides the uniqueness condition.)''

And: ``In any abelian category the only type T object is the zero object, which forces $P = E = 0$ for abelian categories.''

And finally: ``It's routine that both $0 \times {-}$ and $T$ preserve the new structure. We can now remove the existential from AE. Define $\xi\colon T X \to X$ as the image of $r X$. The third task is finished with:

\begin{enumerate}%
\item For every $X$, $0 \times X \to X \stackrel{\xi}{\leftarrow} T X$ is a coproduct diagram.``

\end{enumerate}
\emph{This section is likely to be rewritten and cleaned up.}

[[!redirects AT category]] [[!redirects AT categories]] [[!redirects AT-category]] [[!redirects AT-categories]]

[[!redirects TA category]] [[!redirects TA categories]] [[!redirects TA-category]] [[!redirects TA-categories]]



\end{document}