\input phomework
\def\fcc{{\bf Fcc}}
\def\U{{\sans U}}
\def\V{{\sans V}}
\def\comp{{\sans comp}}
\def\C{{\bf C}}
\def\D{{\bf D}}
\def\E{{\bf E}}
\def\F{{\bf F}}
\def\G{{\bf G}}
\def\int{{\sans Int}}
\def\ext{{\sans Ext}}
\def\fst{{\rm fst}}
\def\snd{{\rm snd}}
\def\pfst{{\sans L}}
\def\psnd{{\sans R}}
{\it January 2, 2001}

\diagramstyle[PostScript=dvips]

Choose a universe $\V$.
and a universe $\U$ such that $\V\in\U$.
Let $\fcc$ be the category of finitely complete $\U$-small categories
with functors preserving finite limits as arrows.
An {\it internal category} in a finitely complete category $\C$
is an object $H$ of $\C$ and arrows $d_0,d_1\colon H\to H$ and $\comp\colon H\times_H H \to H$ --- where
$H\times_H H$ is the pullback 
\diagram
H\times_H H\SEpbk&\rTo^{\snd}&H\cr
\dTo<{\fst}&&\dTo>{d_0}\cr
H&\rTo_{d_1}&H\cr
\enddiagram
of $d_1$ and $d_0$ --- such that the following diagrams commute:
\diagram
    && H                     &&& H                      &&    \cr
(C1)&& \uTo<{d_0}&\rdTo>{d_1} && \uTo<{d_1}&\rdTo>{d_0} &&(C2)\cr
    && H&\rTo_{d_0}&H          & H&\rTo_{d_1}&H         &&    \cr
\enddiagram
\diagram
    && H&\rTo^{\pair{\id_H}{d_1}_H}&H\times_H H&\lTo^{\pair{d_0}{\id_H}_H}&H\cr
(C3)&& &\rdCong&\dTo~{\comp}&\ldCong\cr
    && &&H\cr
\enddiagram
\diagram
    && H&\lTo^{\fst}&H\times_H H&\rTo^{\snd}&H\cr
(C4)&& \dTo<{d_0}&&\dTo~{\comp}&&\dTo>{d_1}\cr
    && H&\lTo_{d_0}&H&\rTo_{d_1}&H\cr
\enddiagram
\diagram
(C5)&& H\times_H H\times_H H&\rTo^{\id_H\times_H \comp}&H\times_H H\cr
    && \dTo<{\comp\times_H\id_H}&&\dTo>\comp\cr
    && H\times_H H&\rTo_\comp&H\cr
\enddiagram
An {\it internal functor} from an internal category
$(H,d_0,d_1,\comp)$ in $\C$ to an internal category
$(H',d_0',d_1',\comp')$ in $\C$ is an arrow
$F\colon H\to H'$ in $\C$ such that the following diagrams commute:
\diagram
    && H&\rTo~F&H'\cr
    && \uTo<{d_0}&&\uTo>{d_0'}\cr
(F1)&& H&\rTo~F&H'\cr
    && \dTo<{d_1}&&\dTo>{d_1'}\cr
    && H&\rTo~F&H'\cr
\enddiagram
\diagram
    && H\times_H H&\rTo^{\pair{F\circ \fst}{F\circ \snd}_{H'}}&H'\times_{H'} H'\cr
(F2)&& \dTo<\comp&&\dTo>{\comp'}\cr
    && H&\rTo_F&H'\cr
\enddiagram
\shout{Proposition:} Internal categories and internal functors in a
finitely complete $\U$-small category $\C$ form a $\U$-small category, $\int(\C)$.
\proc{Proof:} It clearly follows from the fact that $\C$ is $\U$-small that the collections
of internal categories in $\C$ and internal functors are respectively $\U$-small. We define composition
of internal functors in $\C$ by composition of the corresponding arrows in $\C$.
\part{Composition is well-defined:}
If we have internal functors $F\colon H\to H'$ and $G\colon H'\to H''$ in $\C$, then certainly
$G\circ F$ is an arrow of $\C$, but we must check that it is an internal functor $H\to H''$.
Preservation of `domain' and `codomain' is an easy diagram-chase:
\diagram
H&\rTo~F&H'&\rTo~G&H''\cr
\uTo<{d_0}&&\uTo>{d_0'}&&\uTo>{d_0''}\cr
H&\rTo~F&H'&\rTo~G&H''\cr
\dTo<{d_1}&&\dTo>{d_1'}&&\dTo>{d_1''}\cr
H&\rTo~F&H'&\rTo~G&H''\cr
\enddiagram
To see that `composition' is preserved for the composite we must establish the commutativity of
\diagram
 H\times_H H&\rTo^{\pair{GF\fst}{GF \snd}_{H''}}&H''\times_{H''} H''\cr
 \dTo<\comp&&\dTo>{\comp''}\cr
 H&\rTo_{GF}&H''\cr
\enddiagram
given the commutativity of
\diagram
 H\times_H H&\rTo^{\pair{F\fst}{F \snd}_{H'}}&H'\times_{H'} H'&\rTo^{\pair{G\fst'}{G \snd'}_{H''}}&H''\times_{H''} H''\cr
 \dTo<\comp&&\dTo>{\comp'}&&\dTo>{\comp''}\cr
 H&\rTo_F&H'&\rTo_G&H''\cr
\enddiagram
so it suffices to show that $\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} =  \pair{GF\fst}{GF \snd}_{H''}$.
But observe that we have
$$\fst''\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} = G\fst' \pair{F\fst}{F \snd}_{H'}
= GF\fst$$ and 
$$\snd''\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'} = G\snd' \pair{F\fst}{F \snd}_{H'}
= GF\snd$$
so that $\pair{G\fst'}{G \snd'}_{H''}\pair{F\fst}{F \snd}_{H'}$ has the property
which uniquely characterizes $\pair{GF\fst}{GF \snd}_{H''}$, namely that it fits into the pullback diagram
\diagram
H\times_H H\cr
&\rdTo(2,4)_{GF\fst}\rdDotsto\rdTo(4,2)^{GF\snd}&\cr
&&H''\times_{H''} H''&\rTo_{\snd''}&H''\cr
&&\dTo>{\fst''}&&\dTo>{d_0''}\cr
&&H''&\rTo_{d_1''}&H''\cr
\enddiagram
\part{Identities exist:}
The identity internal functor for an internal category $(H,d_0,d_1,\comp)$ is just the identity
arrow on $H$. We need to check that $\id_H$ is an internal functor; preservation of `domain' and
`codomain' is trivial, and preservation of `composition' again follows from the universal property
of the pullback. That is, we have that $\pair{\id_H\fst}{\id_H\snd}_H = \id_{H\times_H H}$, so that (F2) commutes
for $H' = H$ and $F = \id_H$.
That these identites behave correctly under composition follows directly from the behavior of
identity arrows in $\C$.
\part{Composition is associative:}
Associativity of composition in $\int(\C)$ is again a direct conseqence of associativity of
composition in $\C$. \cqed
\shout{Proposition:} Let $\C$ be a finitely complete $\U$-small category. Then $\int(\C)$ is finitely complete.
\proc{Proof:}
\part{Terminal object:}
The terminal object of $\int(\C)$ is the internal category whose
`object of homomorphisms' $H$ is the terminal object $1_\C$ of $\C$. The arrows $d_0,d_1,\comp$
are all then necessarily the unique endomorphism $!\colon 1_\C \to 1_\C$.
The universal property of the terminal object of $\int(\C)$ is satisfied precisely
because it is satisfied for the terminal object of $\C$.
\part{Pairwise products:}
Suppose $(H,d_0,d_1,\comp),(H',d_0',d_1',\comp')$ are two internal categories in $\C$.
We define the product in $\int(\C)$ `pointwise', i.e.
$(H\times H', d_0\times d_0', d_1\times d_1', \comp \times \comp')$.
There appears to be a type mismatch; the type
of $\comp\times \comp'$ is $(H\times_H H) \times (H'\times_{H'} H') \to H\times H'$,
and we want it to be $(H\times H') \times_{H\times H'} (H\times H') \to H \times H'$.
However, $(H\times H') \times_{H\times H'} (H\times H')$ and $ (H\times_H H) \times (H'\times_{H'} H')$ 
are uniquely isomorphic since $\times$ is a right adjoint and so preserves limits, in particular
pullback diagrams. That $H\times H'$ {\it et al.} is in fact an internal category follows from
further application of preservation of limits by the product. It remains to check that
the universal property of the product holds; suppose we have an internal category
$(H'',d_0'',d_1'',\comp'')$ and internal functors $F\colon H'' \to H$ and $G\colon H'' \to H'$.
Now $\pair F G$ (where pairing is in $\C$) is the unique morphism in $\C$ such that
$\pfst \pair F G = F$ and $\psnd \pair F G = G$, where $\pfst,\psnd$ are the projections
from $H\times H'$, again in $\C$. It is easy to check that these projections are
in fact internal functors, and that the pairing is an internal functor.
\part{Equalizers:}
Suppose we have two internal parallel functors
\diagram
H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\enddiagram
we can find the equalizer in $\C$ to obtain an object $H''$ 
and an arrow $E\colon H''\to H$ in $\C$:
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
%&\luDotsto&\uTo\cr
%&&H^{(3)}\cr
\enddiagram
Our first priority is to find structure to make $H''$ an internal category.
Consider the diagram
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
&&\uTo<{d_0}&&\uTo>{d_0'}\cr
H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\enddiagram
and notice that since $F,G$ are internal functors and $E$ equalizes $F,G$,
we have $F d_0 E = d_0' F E = d_0' G E = G d_0 E$.
That is, $d_0 E$ also equalizes $F,G$, which provides us an arrow $d''_0\colon H''\to H''$
such that the following diagram commutes:
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\uDotsto<{d''_0}&&\uTo<{d_0}&&\uTo>{d_0'}\cr
H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\enddiagram
Similarly, we get $d_1''$ out of the diagram
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\uDotsto<{d''_1}&&\uTo<{d_1}&&\uTo>{d_1'}\cr
H''&\rTo_E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\enddiagram
since $d_1 E$ equalizes $F,G$, and we get $\comp''$ out of the diagram
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
\uDotsto<{\comp''}&&\uTo<\comp&&\uTo>{\comp'}\cr
H''\times_{H''} H''&\rTo_{\pair{E \fst''}{E \snd''}_{H}}&H\times_H H&\pile{\rTo^{\pair{F \fst}{F\snd}_{H'}}\cr \rTo_{\pair{G \fst}{G\snd}_{H'}}\cr}&H'\times_{H'} H'\cr
\enddiagram
and observing that
$$\eqalign{
\pair{F \fst}{F\snd}_{H'} \pair{E \fst''}{E \snd''}_{H} &= \pair{FE \fst''}{FE\snd''}_H\cr
 &= \pair{GE \fst''}{GE\snd''}_H\cr
&= \pair{G \fst}{G\snd}_{H'} \pair{E \fst''}{E \snd''}_{H}\cr
}$$
Now it is easy to check that $(H'', d_0'', d_1'', \comp'')$ is an internal category;
for example, by choice $d_0''$ is the unique arrow such that $E d_0'' = d_0 E$, yet
$E d_1'' d_0'' = d_1 E d_0'' = d_1 d_0 E = d_0 E$, so it must be that
$d_1'' d_0'' = d_0''$. It falls out of the diagrams already shown that $E$
is an internal functor $H''\to H$. Now suppose we have a situation as depicted in the diagram
\diagram
H''&\rTo^E&H&\pile{\rTo^F\cr \rTo_G\cr}&H'\cr
&\luDotsto<J&\uTo>I\cr
&&H^{(3)}\cr
\enddiagram
where $H^{(3)}$ is an internal category and $I$ is an internal functor equalizing $F,G$. The universal
property of the equalizer in $\C$ guarantees a unique arrow $J$ making the diagram commute. To
see that $J$ is internal functorial, consider the following diagram:
\diagram
H''&&&\rTo^{d_0''}&&&H''\cr
\uTo<J&\rdTo(2,1)~E&H&\rTo~{d_0}&H&\ldTo(2,1)~E&\uTo>J\cr
&\ruTo~I&&&&\luTo~I&\cr
H^{(3)}&&&\rTo_{d_0^{(3)}}&&&H^{(3)}\cr
\enddiagram
the internal trapezoids commute because $E,I$ are internal functors, and the triangles commute
by choice of $J$. Hence $E d_0'' J = E J d_0^{(3)}$, and because $E$ (being an equalizer) is mono,
we know $d_0'' J = J d_0^{(3)}$. The proofs that $J$ preserves `codomain' and `composition' are similar.
Therefore we conclude that $E$ is the equalizer of $F,G$ in $\int(\C)$. \cqed
\shout{Proposition:} $\C \mapsto \int(\C)$ as defined above is the object
part of a functor $\int\colon \fcc \to \fcc$.
\proc{Proof:}
Let $\F\colon \C \to \D$ be an arrow in $\fcc$, i.e. a finite limit preserving functor from
$\C$ to $\D$. Now $\int(\F)$ also needs to be a finite limit preserving functor, but from
$\int(\C)$ to $\int(\D)$. Suppose we have an internal category $(H,d_0,d_1,\comp)$ in $\C$.
Then we define $\int(\F)(H,d_0,d_1,\comp) := (\F H, \F d_0, \F d_1, \F \comp)$. Because
$\F$ preserves composition and finite products, $(\F H, \F d_0, \F d_1, \F \comp)$ is
an internal category in $\D$. The action of $\int(\F)$ on arrows of $\int(\C)$ is the obvious
one; $\int(\F)(F) := \F F$. Now it is possible to see that $\int(\F)$ is
functorial since $\int(\F)(\id_H) = \F(\id_H) = \id_{\F H} = \id_{\int(\F)(H)}$ for any
internal category object $H$ in $\C$, and 
$\int(\F)(G \circ F) = \F(G \circ F) = \F(G) \circ \F(F) = \int(\F)(G) \circ \int(\F)(F)$
for any internal functors $F\colon H\to H'$ and $G\colon H'\to H''$ in $\C$.
Now we check that $\int(\F)$ preserves finite limits; We have first of all that
$\int(\F)(1_{\int(\C)}) = (\F 1_{\int(\C)}, \F !, \F !, \F !) = (1_{\int(\D)}, !, !, !)$
because $\F$ preserves the terminal object. Moreover, just by unrolling definitions again
we see
$$\eqalign{
\int(\F)((H,  d_0,  d_1, \comp) \times ( H',  d_0',  d_1', \comp')) &=
\int(\F)(H\times H', d_0 \times d_0', d_1 \times d_1', \comp\times \comp') \cr
&= (\F(H\times H'), \F(d_0 \times d_0'), \F(d_1 \times d_1'), \F(\comp\times \comp')) \cr
&= (\F H\times \F H', \F d_0 \times \F d_0', \F d_1 \times \F d_1', \F \comp\times \F\comp') \cr
&= (\F H, \F d_0, \F d_1, \F \comp) \times (\F H', \F d_0', \F d_1', \F\comp') \cr
&= (\F H, \F d_0, \F d_1, \F \comp) \times (\F H', \F d_0', \F d_1', \F\comp') \cr
&= \int(\F)(H,  d_0,  d_1, \comp) \times \int(\F)( H',  d_0',  d_1', \comp') \cr
}$$
and similarly $\int(\F)$ preserves equalizers because $\F$ does.
Finally, we want $\int$ itself to be functorial. Suppose we have arrows
$\F\colon \C\to \D$ and  $\G\colon \D\to \E$ in $\fcc$. Then
$$\eqalign{
\int(\G \circ \F)(H, d_0, d_1, \comp) &= ((\G\circ \F)(H), (\G\circ \F)(d_0), (\G\circ \F)(d_1), (\G\circ \F)(\comp))\cr
&= (\G(\F(H)), \G(\F(d_0)), \G(\F(d_1)), \G(\F(\comp)))\cr
&= \int(\G)(\F(H), \F(d_0), \F(d_1), \F(\comp))\cr
&= \int(\G)(\int(\F)(H, d_0, d_1, \comp))\cr
&= (\int(\G) \circ \int(\F))(H, d_0, d_1, \comp)\cr
}$$
and for any object $\C$ of $\fcc$ we know
$$\eqalign{
\int(\id_\C)(H, d_0, d_1, \comp) &= (\id_\C(H), \id_\C(d_0), \id_\C(d_1), \id_\C(\comp))\cr
&= (H, d_0, d_1, \comp)\cr
}$$
and so $\int(\id_\C) = \id_{\int(\C)}$, hence $\int\colon \fcc \to \fcc$ is functorial.\cqed
\shout{Conjecture:} There exists a functor $\ext\colon \fcc \to \fcc$ such that $\int\dashv \ext$.
\shout{Conjecture:} $\fcc$ is countably cocomplete.
\shout{Corollary:} There exists a finitely complete $U$-small category $\C$ such that
$\int(\C) \cong \C$.
\proc{Proof:}
Let $\Sets_\V$ be the ($\U$-small) category of all $\V$-small sets.
There exists a functor $F\colon \Sets_\V\to \int(\Sets_\V)$ defined by 
$$F(S) := (S, \id_S, \id_S, \id_S)$$
and $$F(f) := f$$
So we can form the diagram
\diagram
D&:=&\Sets_\V&\rTo^f&\int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}\cdots
\enddiagram
and set $\C := \dirlim\, D$ to obtain 
\diagram
\Sets_\V&\rTo^f&\int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}\cdots\cr
&\rdTo<{i_0}&\dTo~{i_1}&\ldTo~{i_2}&\cdots\cr
&&\C\cr
\enddiagram
Now $\int$, being a left adjoint, preserves colimits, so we have that
\diagram
\int(\Sets_\V)&\rTo^{\int(f)}&\int^2(\Sets_\V)&\rTo^{\int^2(f)}&\int^3(\Sets_\V)&\rTo^{\int^3(f)}\cdots\cr
&\rdTo<{\int(i_0)}&\dTo~{\int(i_1)}&\ldTo~{\int(i_2)}&\cdots\cr
&&\int(\C)\cr
\enddiagram
is also a colimit diagram. That is, $\int(\C) = \dirlim\, \int(D)$.
Now if we can show that $\C$ is the colimit of $\int(D)$, then
$\C \cong \int(\C)$. Certainly $\C$ together with $i_1,i_2,i_3,\ldots$ is
a cocone over $\int(D)$, so there exists a unique $h\colon \int(\C) \to \C$ such
that
\diagram
&\int^{n+1}(\Sets_\V)\cr
\ldTo(1,2)<{\int(i_n)}&&\rdTo(1,2)>{i_{n+1}}\cr
\int(\C)&\rTo_h&\C\cr
\enddiagram
commutes for every $n\in \N$. Also $\int(\C)$ together with $\int(i_0) \circ f, \int(i_0),\int(i_1),\int(i_2),\ldots$
is a cocone over $\D$, so there exists a unique $k\colon \C \to \int(\C)$ such
that
\diagram
&\Sets_\V\cr
\ldTo(1,2)<{\int(i_0) \circ f}&&\rdTo(1,2)>{i_{0}}\cr
\int(\C)&\lTo_k&\C\cr
\enddiagram
commutes and
\diagram
&\int^{n+1}(\Sets_\V)\cr
\ldTo(1,2)<{\int(i_n)}&&\rdTo(1,2)>{i_{n+1}}\cr
\int(\C)&\lTo_k&\C\cr
\enddiagram
commutes for every $n\in \N$. Notice that $h,k$ are morphisms
in the category of cocones over $\int(D)$, and therefore so too is $k\circ h\colon \int(\C)\to\int(\C)$.
Hence $kh = \id_{\int(\C)}$ since $\int(\C) = \dirlim\, \int(D)$.
But $h,k$ are also morphisms in the category of cocones over $D$ ($h$ is because $h\circ \int(i_0) \circ f = i_1 \circ f = i_0$)
so $hk = \id_{\C}$ since $\C = \dirlim\, D$. That is, $h,k$ are an inverse pair, and $\C\cong \int(\C)$.\cqed
\end
$$I := \pair{\pair{\pfst_{H\times H'}\fst_{H\times H'}}{\pfst_{H\times H'}\snd_{H\times H'}}_H}
{\pair{\psnd_{H\times H'}\fst_{H\times H'}}{\psnd_{H\times H'}\snd_{H\times H'}}_{H'}}$$
