On Fri, Oct 1, 2010 at 2:24 AM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
Well, but then we can work with categories with a chosen structure, e.g. chosen products; that's what is recommended in the Elephant and it looks to me as close to practice; it's very unlikely to have a nonconstructive proof of existence of products.
Unlikely, but it happens occasionally. For instance, if the morphisms of a category are equivalence classes, then a "construction" of equalizers or pullbacks might require choosing representatives; this actually happens at one point in the Elephant. The "small complete categories" in realizability topoi are also generally "weakly complete," in the sense that "every small diagram has a limit" is true in the internal logic, but not "strongly complete" in the sense that there exist internal limit-assigning (non-ana) functors. The property of "strong completeness" is also not in general preserved or reflected by weak equivalence functors. One can of course develop a theory which distinguishes between weak and strong equivalence and weak and strong completeness, but I think it's reasonable to call it "unfamiliar" to most category theorists. It feels to me like trying to do work constructively with topological spaces and therefore having to talk about [0,1] being complete and totally bounded but not compact, instead of realizing that when working constructively, one should really replace topological spaces with locales. Just as in set theory, no axiom of choice is necessary to define a function whose values are individually uniquely determined, it seems to me that no axiom of choice should be necessary in category theory to define a functor whose values are individually uniquely determined up to unique isomorphism. But obviously this is a subjective judgement. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]