categories: Re: Computing with Category Theory

[Jason C Reed <jcreed@andrew.cmu.edu>]

On Thu, 1 Nov 2001, Barry Jay wrote:

> Dear Saul,
>
> I can envisage at least two distinct ways of computing with categories.
> One is for category theorists to use computers to do their calculation
> or perhaps even provide formal proofs of theorems.

This is actually quite feasible using existing tools. For instance, that
we don't need to put the existence of exponentials in the definition of a
topos (i.e. a terminal object, subobject classifier, power objects, and
pullbacks suffice to construct exponentials) can be proved formally.
see http://functor.org/math/cd01.ps.

---Jason