Re: Computing with Category Theory

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