[FOM] When is it appropriate to treat isomorphism as identity?

[Andrej Bauer]

On Sun, May 24, 2009 at 4:53 AM, Vaughan Pratt <pratt at cs.stanford.edu> wrote:
> First, as a picky point, the rationals are not the initial field (there
> are no ring homomorphisms from Q to GF(4) for example).  Q *is* the
> initial ordered field however, but now you need to bring in order earlier.

Oops, thank you for pointing that out. (The problem seems to be with
the characteristic. Is Q the initial field with characteristic 0? That
would be an alternative to bringing in order.)

> Second, I don't understand in what sense the elements of an initial
> algebra aren't thereby being represented.

You _can_ represent an initial algebra, it might even be smart to do
so, but you don't have to (and your initial claim was that one _must_
think about representations in constructive mathematics). Instead, you
can just adopt an axiom which says that such-and-such functor (or
monad) has an initial algebra, and prove all properties from the
axiom, without ever wondering how to think about the initial algebra
concretely. Isn't that what category theorists do?

Andrej