On 15 Sep 2010, at 08:43, Thomas Streicher wrote:
On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows
if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ...
I don't see how to avoid reference to equality of objects in this formulation.
If one tries to define fibrationhood as a property of functors, "P : XX --> BB is a fibration", then indeed talking about equality of objects seems unavoidable. The problem is exactly turning the object part F : ob XX ---> ob BB into a function ob BB ---> Sets. But if instead we define a set of "fibrations over BB", then we can do it: a fibration over BB is a function ob BB ---> Sets, together with etc. etc. (I gave more details in a post on June 2, answering a similar question.) Now, in classical foundations, this is (1-)equivalent to the usual definition. Within a dependent type theory foundation, they are only rather more weakly equivalent; and in that case I'd hazard that something along these lines is a more natural/fruitful definition. Digressing a little further, a similar situation arises for many other classes of maps that are viewed as "fibrations" or some sort: in a dependently-typed foundation, it's often more natural to consider a type of "fibrations over B", which then have "total spaces" that are maps into B, rather than defining "f is a fibration" as a property of maps. The most fundamental case is just in Sets, with (classically) "all maps are fibrations": in a dependent system, a "fibration over B" is a function B --> Sets, which may not be quite the same as a map E --> B. -p. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]