Re: Not invariant but good

[Michael Shulman <mshulman@ucsd.edu>]

On Sun, Sep 26, 2010 at 10:36 PM, John Baez <baez@math.ucr.edu> wrote:
> Can every property of categories that is invariant under equivalence be
> expressed in some language that doesn't include equations between objects?
> Or conversely? Or what precise conditions are needed to get theorems along
> these lines?

The converse is very easy, and it's something that I and others have
frequently mentioned in these discussions: if we write category theory
in dependent type theory with arrows dependent on their source and
target and no equality predicate on objects, then all formulas and
constructions in this language are easily proven to be invariant under
equivalence and isomorphism.

The forward direction is trickier, but essentially the answer is yes:
I believe theorems along these lines can be found in:

1) Peter Freyd, "Properties invariant within equivalence types of
categories", 1976

2) Georges Blanc, "Équivalence naturelle et formules logiques en
théorie des catégories",  1979

3) Michael Makkai, "First-order logic with dependent sorts, with
applications to category theory,"
http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf

(and perhaps others that I'm unaware of).

Mike


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