Re: terminology

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

Thorsten Altenkirch wrote in part:

>A setoid is the intensional representation of a quotient (ie
>coequalizer) and any construction involving it should respect this
>structure. To use the underlying set of a setoid to construct another
>set seems fundamentally flawed.

I would rather not say "underlying set" here, but "underlying type".
The category of types can do what it likes, but the category of sets
should already have coequalisers.  (Some type theorists do say "set" here;
I just think that it is liable to confuse category theorists.)
It is the setoids which behave like the sets that we know.

But what is flawed about using the underlying type of a set(oid)?
Group theorists who found group theory on set theory
are allowed to use the underlying set of a group.
So set theorists who found set theory (as setoid theory) on type theory
should be able to speak of the underlying type of a set(oid),
and category theorists who found category theory on type theory
should be able to speak of the underlying type of their structures.

>My understanding of an arrow category is that it's objects are the
>morphisms of  the underlying category and since this is a setoid objects
>should be represented as a setoid too.

I'm not sure what you mean by "this is a setoid".
If you mean that, given a category C (as formalised in type theory),
the morphisms of C form a setoid, then this is not true.
Given a category C and two objects x and y of C,
then the morphisms of C from x to y form a setoid, nothing more.

Even if they did form a setoid, what of that?
In Peter May's example of the category of intermediate fields
in a given field extension, the objects do form a setoid.
I call such a category a "strict category":
  http://ncatlab.org/nlab/show/strict+category
Any poset defines a strict category in which isomorphic objects are equal.
More generally, any category in which any two parallel morphisms are equal
may be made into such a strict category by defining equality as isomorphism.
Assuming an appropriate version of the axiom of choice,
any category whatsoever may be made into a strict category
by defining equality as isomorphism and making some choices
to match up hom-sets.

The fact that strict categories exist does not invalidate
the perspective from which categories are not inherently strict,
any more than the existence of monoidal categories
invalidates ordinary category theory.
Even assuming the axiom of choice,
that we can make any category into a strict category is like
our ability to make any monoidal category into a strict monoidal category;
the theory of weak categories and weak monoidal categories stands.
(Incidentally, any strict monoidal category must be a strict category,
while a weak monoidal category need not be.)

>You may say that we are only interested in objects upto isomorphism. But
>what does this mean precisely?

What it means is that, whenever anyone refers to equality of objects,
I interpret it as being a statement in strict category theory,
with all other statements being in ordinary (weak) category theory.
It is an empirical claim that the basic results of category theory
as it is normally understood do not refer to equality of objects.
It is conjecture in metamathematics that any such statement,
if a theorem, has a proof that never refers to equality of objects.
(Whether this conjecture is true or false can depend
on exactly what your foundations of mathematics are.
You also have to take care to identify defined concepts
that implicitly make reference to equality of objects.)


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]