Suppose we have a category C. We can partition the objects of C into equivalence classes each populated by the objects that are isomorphic to each other. If we assert the Univalence Axiom, then each equivalence class collapses to one element and the Axiom of Choice becomrd vacuous. I am sure I am using the Univalence Axiom naively, yes? If so, why and how? Thx, Vasily Gal'chin [For admin and other information see: http://www.mta.ca/~cat-dist/ ]