equivalence terminology

["Paul Taylor" <pt10@PaulTaylor.EU>]

Colin McLarty said,

> It is an interesting impulse in higher category theory to avoid
> identity in favor of isomorphism on the level of objects, and to avoid
> isomorphism in favor of equivalence on the level of categories.   But
> so far as I know no one has yet articulated a way to avoid ever using
> identity of objects and identity of categories.

I am not going to get involved in higher category theory, but one
setting in which (essentially) the question of identity of objects
arises is in the interpretation of type theories in categories,
where one needs to "choose" binary products, to give the simplest case.

Any type theory has its category of contexts and substitutions
(or classifying category).  This has the categorical structure
that is analogous to the type theoretic connectives, for example
it's a CCC if we started with lambda calculus.

Conversely, any category has its proper language, consisting of names
for its objects and morphisms and various axioms.

Without even having the structure, let alone a choice of it,
the category is embedded in the category of contexts and substitutions
of its proper language.

If the category has choices for the structure then this embedding
is a strong equivalence, ie with a pseudo-inverse,

If it has the structure but not choices for it then it is a weak
embedding - full, faithful and essentially surjective.

The upshot of this is that, by replacing the category with a weakly
equivalent one, you become able to talk about equality of objects,
choices of product, etc.

In other words, using the principle of interchangeability at a
higher categorical level, we get the convenience of working with
equality in the original structure.

This is all explored in my book, "Practical Foundations of Mathematics".

Paul


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