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/ ]