In reply to David Roberts's message. Of course, category theorists do study weaker notions than equivalence in the 2-categorical sense and that's worthwhile to do. But it only makes sense when you still have a notion of equality of objects, i.e. a category in the ordinary sense of the word. If equality and (weak) equivalence were the same then one would not need to study model categories and/or related structures. Now it is certainly a fascinating extremist thought experiment to investigate logical systems where part of the structure they speak about is made invisible. This Martin Hofmann and I suggested when studying the groupoid model of type theory. There are nonstandard logical systems (intensional type theory) with a treatment of equality very different from the usual one. The main deviating feature is that ordinary replacement of equals is not valid anymore. Instead one always has to specify along which proof of equality one replaces. That's not convenient but necessary for keeping type checking decidable. But this inconvenience allows one to interpret this nonstandard equality as isomorphism in a category which does have equality of objects!. It is just that the formal system cannot speak about it. But ordinary equality is still required for interpreting judgemental equality! I don't know of any way to interpret type theory directly in a weak higher dimensional. It's always interpreted in a representing model category with its equality of objects. As the name says HoTT seems to be a fine ambience for doing synthetic homotopy theory. It is less clear for me how useful it is as a setting for developing category theory. I have made some experiments with the cases of indexed categories and monoidal categories which were disappointing. One might expect that you get coheence conditions for free or are at least forced to impose them. But this is not the case you just get a further level of generality not witnessed by interesting examples. I would be glad to see some positive uses of identifying equality and isomorphism when doing or at least formalizing category theory. According to my understanding what Jean wanted to say was that for getting enough equivalences you need choice for classes in order to find "quasi-inverses" to weak equivalences. This certainly is the situation when you reason about categories in ZF with a couple of Grothendieck universes. You need choice to identify strong and weak equivalence. It is presumably better (at least sometimes) to distinguish these notions. The situation is quite different when you use type theory with Univalence Axiom (UA) for speaking about categories. As always in type theory you have a kind of AC available because you interpret existential quantification as dependent sums. So one might think that everything's fine. But actually, since equality is interpreted in a deviating way if you write down isomorphism of types it turns out to mean weak equivalence (e.g. in the simplicial sets model). This means that what looks strong is actually very weak. But this is not a contradiction since existence and equality have very different meanings in these two settings. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]