Re: are fibrations evil?

Re: are fibrations evil?

[Fred E.J. Linton]

Those of us whom the use (or misuse) of the term "evil" displeases
should be aware that some of that term's proponents are using it, 
in part, only because -- like the DaDa-ists of a certain intellectual 
period in France -- they enjoy seeing how predictably that term is
able to "épater (or "épouvanter") les bourgeois".

Why continue to feed that enjoyment?

Cheers, -- Fred



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Toby Bartels]

Eduardo J. Dubuc wrote at first:

>Dear Toby, your choice of example is very unfortunate. Mac Lane wrote
>that category theory was invented to define functor, and that functor was
>invented to define "natural" transformation.

Yes, I know; that was quite deliberate.

I'm afraid that I no longer have any idea
how to communicate with you on this matter.
I'm sure that you don't understand my opinion,
and it's clear that I must not understand yours,
but beyond that I have no idea what upsets you,
and I'm not going to worry about it any more.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Eduardo J. Dubuc]

Toby Bartels wrote:

>
> Shall we stop saying "natural" and say "invariant under composition"?
> Or is that term allowed under the grandfather clause,
> since it was being used imprecisely before category theory defined it?

Dear Toby, your choice of example is very unfortunate. Mac Lane wrote that
category theory was invented to define functor, and that functor was invented
to define "natural" transformation.

How do you compare the importance of the concepts "invariant under
composition" (assuming that is the definition of "natural") and "invariant
under equivalence".

The discovery of the property underneath many important mathematical
developments (property not clearly evident or identified at the time) (like
Stone duality just one example) was an extraordinary accomplishment.

Invariant under equivalence is obviously used, is a concept already there
(whether true or false). The introduction of a new name for it can only be
justified by a frequent use, which is not clear at the moment.


> If I can find a citation where John Baez used the term "evil"
> before he knew how to define it, will that make it OK?
> Or is that irrelevant because John was already working in the ghetto?

?????????????

   > You may continue to write down strict definitions,
> and we will continue to weaken them as we need.
> Different styles of mathematics are not at war.

Sorry, I never said that i will only write strict definitions (as a matter of
fact I have already written several non strict ones when I need them and they
were naturally the correct ones over the strict version).

If I run into a concept (or definition) non invariant under equivalence, I
will just say so. No need to introduce a name for it, and much worse to call
it "evil". Understand ?

> I understand that "evil" is grating; other terms have been suggested.
> But no, *any* short term to replace "not invariant under equivalence"
> is forbidden by your decree: it relegates us to the ghetto.
> Well, that is your interpretation, but it doesn't affect my mathematics.

Your mathematics will not change a bit whether you use the term "evil", or any
other term "x", or simply "not invariant under equivalence".

e.d.



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Toby Bartels]

Eduardo J. Dubuc wrote:

>Furthermore, the introduction of new terminology (specially if this
>terminology refers directly to a meaning in everyday life) with no real
>need and/or to change established terminology, is an habit that harm the
>credibility of any school of research.

Shall we stop saying "natural" and say "invariant under composition"?
Or is that term allowed under the grandfather clause,
since it was being used imprecisely before category theory defined it?
If I can find a citation where John Baez used the term "evil"
before he knew how to define it, will that make it OK?
Or is that irrelevant because John was already working in the ghetto?

>In the present case we are discussing a particular single word "x" to
>replace the compound "not invariant under equivalence". This seems
>justified by its frequent use, but its frequent use is due precisely
>because we are discussing its use !!!.

As a proud citizen of the Ghetto of Category Land,
I've used that term in other contexts than this discussion.
If you do not wish to join us, what does that matter?
You may continue to write down strict definitions,
and we will continue to weaken them as we need.
Different styles of mathematics are not at war.

I understand that "evil" is grating; other terms have been suggested.
But no, *any* short term to replace "not invariant under equivalence"
is forbidden by your decree: it relegates us to the ghetto.
Well, that is your interpretation, but it doesn't affect my mathematics.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Eduardo J. Dubuc]

Andre is very polite, I call such a subculture "ghetto", and Benabou 
calls it "Category land".

Joyal wrote:
> Dear David,
> 
> I appreciate your view.
> I would love to have the dictatorial power to reform 
> the mathematical vocabulary.
> I dream of kicking out long words like diffeomorphism and homeomorphism.
> I guess that if they have persisted in mathematics, it is because
> everybody understand them.
> 
> It is very difficult to impose a new terminology.
> There is a social aspect to the problem.
> Even if small group of peoples agree in using
> a new terminology, this may have little influence on the larger community.
> The new word may become a tag for identifying the members of a group.
> It may enclose its user into a sub-culture.
> 
> Best,
> andré
> 

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Eduardo J. Dubuc]

I completely agree with Andre.

I add:

Furthermore, the introduction of new terminology (specially if this 
terminology refers directly to a meaning in everyday life) with no real 
need and/or to change established terminology, is an habit that harm the 
credibility of any school of research.

In the present case we are discussing a particular single word "x" to 
replace the compound "not invariant under equivalence". This seems 
justified by its frequent use, but its frequent use is due precisely 
because we are discussing its use !!!.
In the practice of category theory or mathematics, its use is not 
frequent enough to justify the introduction of new (simpler) 
terminology. What happens with readers which see "x" and do not belong 
to our group ?.
Well, most will be upset , and specially if "x is evil" (ja !).

Joyal wrote:
> Dear John,
> 
> A property is "evil" in your sense if it is
> not invariant under equivalences.
> Invariance under equivalence is a well
> established mathematical notion.
> I prefer to say that something is not
> invariant under equivalence than to say
> that it is "evil". There is no need to
> introduce a new terminology.
> 
> Best,
> André 
> 

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Joyal, André]

Dear David,

I appreciate your view.
I would love to have the dictatorial power to reform 
the mathematical vocabulary.
I dream of kicking out long words like diffeomorphism and homeomorphism.
I guess that if they have persisted in mathematics, it is because
everybody understand them.

It is very difficult to impose a new terminology.
There is a social aspect to the problem.
Even if small group of peoples agree in using
a new terminology, this may have little influence on the larger community.
The new word may become a tag for identifying the members of a group.
It may enclose its user into a sub-culture.

Best,
andré



-------- Message d'origine--------
De: David Yetter [mailto:dyetter@math.ksu.edu]
Date: dim. 19/09/2010 10:57
À: Joyal, André
Cc: John Baez; categories
Objet : Re: categories: Re: are fibrations evil?
 
Dear Andre:

Brevity is the usual reason for introducing new terminology.

And, ultimately there is a need, as mathematics would grind
to a halt if one had to write out a phrase giving the content
of each concept whenever one wanted to talk about it.

One may object to the jocular use of a word with a moral
denotation as the name for a mathematical concept, but four 
characters beats 28 characters (or 31 if one counts spaces).

It certainly seems desirable to have a brief name for either
"invariant under equivalence" or "not invariant under 
equivalence".

Best Thoughts,
David Y.


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[David Yetter]

Dear Andre:

Brevity is the usual reason for introducing new terminology.

And, ultimately there is a need, as mathematics would grind
to a halt if one had to write out a phrase giving the content
of each concept whenever one wanted to talk about it.

One may object to the jocular use of a word with a moral
denotation as the name for a mathematical concept, but four 
characters beats 28 characters (or 31 if one counts spaces).

It certainly seems desirable to have a brief name for either
"invariant under equivalence" or "not invariant under 
equivalence".

Best Thoughts,
David Y.

On 18 Sep 2010, at 08:50, Joyal, André wrote:

> Dear John,
> 
> A property is "evil" in your sense if it is
> not invariant under equivalences.
> Invariance under equivalence is a well
> established mathematical notion.
> I prefer to say that something is not
> invariant under equivalence than to say
> that it is "evil". There is no need to
> introduce a new terminology.
> 
> Best,
> André 
> 

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Joyal, André]

Dear John,

A property is "evil" in your sense if it is
not invariant under equivalences.
Invariance under equivalence is a well
established mathematical notion.
I prefer to say that something is not
invariant under equivalence than to say
that it is "evil". There is no need to
introduce a new terminology.

Best,
André 

 


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Thomas Streicher]

We seem to agree that paying attention to the non-kosher concept is at least
very convenient. But what I do not see is a correspondence between kosher and
non-kosher versions. If you start with a collection CC of 1-cells in a 2-cat
like Cat and close it under equivalences thus obtaining CC' I don't see any
way of reconstructing CC from CC' in a canonical way.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Toby Bartels]

Thomas Streicher wrote at last:

>BTW under a regime which identifies equality with being isomorphic (or weakly
>equivalent) it looks tempting to use functors from B^\op to Cat. These should
>capture the pseudo-functors since equality and isomorphism are identified. But
>writing down functoriality in type theory using \Sigma for existence amounts
>to choosing a lot of not at all canonical "canonical isomorphisms". Actually,
>one would get something even more general than pseudo-functors because one
>wouldn't write down the coherence conditions (actually one couldn't even
>since there is no honest for good equality!).

Yes, you can write the coherence conditions down
(although I agree that it would be easy to forget them).

What you need is that a functor (pseudofunctor) P: B^\op -> Cat
is not just the following data:
*  for each object x of B,
     a category P_x,
*  for each object x, object y, and morphism f: x -> y,
     a functor P_f: P_x -> P_y,
*  functoriality structure (and maybe coherence conditions);
but in fact the following data:
*  for each object x of B,
     a category P_x,
*  for each object x, object y, and morphism f: x -> y,
     a functor P_f: P_y -> P_x,
*  for each object x, object y, and equal morphisms f = g: x -> y,
     a natural isomorphism P_{f=g}: P_f => P_g,
*  functoriality structure and coherence conditions.

For example, given f: w -> x, g: x -> y, and h: y -> z in B,
we want to compare (P_f . P_g) . P_h with P_f . (P_g . P_h).
In a "kosher" treatment of category theory, these aren't equal
(that would be meaningless), but there is an associator between them.
As a coherence condition, we want to demand that this associator
is equal (and this does have meaning) to a natural isomorphism
built out of the functoriality structure isomorphisms and their inverses.
As we do this, we need to compare P_{(f;g);h} and P_{f;(g;h)}.
Again, it's not meaningful (much less true) that these are equal,
but P_{(f;g);h = f;(g;h)} is a natural isomorphism between them.
So we can write down this coherence condition after all.


--Toby


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Michael Shulman]

On Thu, Sep 16, 2010 at 2:47 AM, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
> For such a thing the key intuitions are lost as
> far as I can see (even if I and J are isomorphic the fibre over I may be
> inhabited whereas the fibre over J is inhabited).

The key necessary change to intuition is that one has to replace
"fiber" (itself a non-kosher notion) with "essential fiber".
http://ncatlab.org/nlab/show/essential+fiber
With this change, all the usual intuitions and facts about fibrations
still hold (in corresponding kosher ways).

> I doubt that category
> theory over a base (topos) can be developed this way.

The 2-category of Street fibrations over a given category (such as a
topos) is biequivalent to the 2-category of Grothendieck fibrations
over that same category, and both are biequivalent to the 2-category
of Cat-valued pseudofunctors.  (In fact, any Street fibration is
equivalent to a Grothendieck fibration, using the same construction
which shows that any functor is equivalent to an isofibration; thus
the second is a full biequivalent sub-2-category of the first.  The
second and third are actually strictly 2-equivalent.)  Thus, anything
kosher that can be done in one can equally be done in the others.

> At least it would be
> very cumbersome. Has the generalised notion of fibration been used for
> something?

Indeed it would be cumbersome, and unnecessary for most purposes.  The
only use I know of for Street fibrations is when working internally to
a bicategory.  Both Street and Grothendieck fibrations can be defined
internally to a strict 2-category, and I believe that if the
2-category has some simple strict 2-limits then every Street fibration
will be equivalent to a Grothendieck one, just as in Cat.  However,
since Grothendieck fibrations are non-kosher, their internal
definition involves equality of arrows, and hence is not really
sensible in a bicategory rather than a strict 2-category.  This was
Street's original application.

I didn't mean to say that Street's kosher fibrations *should* be used
in any place where Grothendieck non-kosher ones suffice, or that the
latter aren't easier, simpler, more common, and better to use in
practice when possible.  This is often the case with kosher and
non-kosher things, like weak and strict 2-categories, or bilimits and
pseudolimits.  But in almost all cases where we use non-kosher things,
there *exists* an equivalent kosher notion, and occasionally it
happens that the equivalence breaks and in that case we have to use
the kosher notion instead.  The only thing I was objecting to was your
conclusion that equality of objects is sometimes "absolutely
necessary" -- in this case, as in many others, it's just very
convenient.

(There are a few situations where equality of objects -- or, in Toby's
language, the use of "strict categories" -- does seem to be
conceptually fundamental, such as Peter May's Galois theory example.
But I don't think fibrations is one of them.)

Why should we distinguish between "absolutely necessary" and "very
convenient"?  For the "working mathematician" perhaps there is no
reason to.  But I think that for a category theorist developing new
categorical concepts, it is a useful heuristic guide -- if a
non-kosher concept is not equivalent to some kosher one, then that is
a reason to be suspicious of it, if nothing more.

Mike


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[John Baez]

Thomas wrote, of fibrations:

Sure, they are "evil" but it seems to be beneficial to be "evil" sometimes.
>

Of course!  Anybody who thinks that concepts should be avoided merely
because they're "evil" in the technical sense must also think that odd
numbers are peculiar and perfect groups are the best groups to study.  I'm
finding it quite amusing how people are getting worked up over the concept
just because its name has moral overtones.

An excellent example of an evil but useful concept is the concept of
"skeletal category".  Every category is equivalent to a skeletal one
(assuming choice), but not every category is skeletal.  So, this concept is
evil.  But it's sometimes nice to prove a theorem for all categories by
proving it for skeletal categories.

We can formalize this a bit.

Remember, a property P of objects in an n-category is "evil" if there's an
object with that property that is equivalent to an object without that
property.  It's "non-evil" if whenever x has property P and x is equivalent
to y, y also has that property.

(I'm using classical logic here.  If we're using intuitionistic logic, the
really useful concept is the concept that I'm calling "non-evil".  We should
probably call it "good": evil is just the absence of good.  But "non-evil"
is less likely to cause confusion.)

Every property P can be made non-evil by defining a new property P' that
means "equivalent to something with property P".  Sometimes it's more
convenient to work with objects with property P than objects with property
P'.  And note: if the property Q is non-evil, the theorem

all objects with property P have property Q

automatically implies

all objects with property P' have property Q

So, for example, if Q is a non-evil property of categories, to prove Q holds
for all categories it suffices to prove it for skeletal categories.

Or - with a bit more work to fill in the details - if Q is a non-evil
property of functors, to prove Q holds for all Street fibrations it suffices
to prove it for fibrations.

Best,
jb

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[David Roberts]

Mike wrote:

>If one defined the identity types and pullbacks using limits in Gpd in the
>kosher 2-categorical sense, then it seems to me that one should be
>able to define an equivalent model using arbitrary functors between
>groupoids to represent the dependent types, rather than merely the
>fibrations.

This seems (to me) to be analogous to extending one's notion of
covering space to allow for empty fibres - indeed, the
characterisation of covering spaces as representations of Pi_1 needs
this.

David

PS +1 for using 'kosher' :)


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Thomas Streicher]

Sure, they are "evil" but it seems to be beneficial to be "evil" sometimes.
If the equivalence closed version would have been the original one I doubt
that it would have been recognized how useful they are for category theory
over fairly general bases. Or, rather, people would have quickly shifted to
the "evil" version.

BTW under a regime which identifies equality with being isomorphic (or weakly
equivalent) it looks tempting to use functors from B^\op to Cat. These should
capture the pseudo-functors since equality and isomorphism are identified. But
writing down functoriality in type theory using \Sigma for existence amounts
to choosing a lot of not at all canonical "canonical isomorphisms". Actually,
one would get something even more general than pseudo-functors because one
wouldn't write down the coherence conditions (actually one couldn't even
since there is no honest for good equality!).

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Prof. Peter Johnstone]

Yes, fibrations in the original sense of Grothendieck are "evil"
(sorry, Jean!), as is shown by the fact that an equivalence of
categories is not in general a fibration. There is a weaker notion
of fibration in which one replaces the equality "P\phi = u" by a
(specified) isomorphism PY -> J making the obvious triangle
commute. But every fibration in this sense factors as an equivalence
followed by a fibration in Grothendieck's sense, so it's not
such an important notion.

Peter Johnstone

On Wed, 15 Sep 2010, 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.
>
> This already happens if XX and BB are groupoids where P : XX -> BB is a
> fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X
> with P\phi = u.
>
> Ironically the category of groupoids and fibrations of groupoids as families
> of types was the first example of a model of type theory where equality may
> be interpreted as being isomorphic.
>
> So my conclusion is that equality of objects is sometimes absolutely
> necessary. Avoiding reference to equality is also not a question of using
> dependent types as some people implicitly seem to say. Even in intensional
> type theory there is a notion of equality. But it is sometimes inconvenient
> to use. As pointed out by Ahrens one can and should use extensional type theory
> whenever convenient.
> Intensional type theory allows one to interpret equality as being isomorphic,
> a kind of reward for the inconvenience of using intensional identity types.
>
> Thomas
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Thomas Streicher]

Dear Michael,

Street's notion of fibration is a weakening not a strengthening of
Grothendieck fibrations. For such a thing the key intuitions are lost as
far as I can see (even if I and J are isomorphic the fibre over I may be
inhabited whereas the fibre over J is inhabited). I doubt that category
theory over a base (topos) can be deloped this way. At least it would be
very cumbersome. Has the generalised notion of fibration been used for
something?

I agree with you that Kan fibrations in simplicial sets are an alternative
and certainly the right thing if one want's to get "weak". After all that's
what I suggested in 2006 in a talk in Uppsala.
I personally am interested in the possibility of having type theories where
equality coincides with being isomorphic or even weakly equivalent (as recently
suggested by Voevodsky).
But this is an extremal point of view which shouldn't be taken absolute since
otherwise important parts of category theory get lost.

I suspect that when doing fibered categories in a type theory validating
Voevodsky's equivalence axiom one comes up with something like Street's
generalisation of fibrations. But that doesn't mean that we arrive at something
easy to work with.

What Martin Hofmann and I thought when bringing up the idea was that use of
intensional Id-types amounts to imposing a brutal bureaucracy which FORCES
you to check all the coherence conditions often swept under the carpet.

I think when interpreting type theory in the topos SSet of simplicial sets
one can have both extensional Id-types and the intensional ones. In the first
case a family of types is simply a map of SSet, in the second case it is a
Kan fibration. Luckily both system of display maps are closed under \Sigma and
\Pi. Thus the intensional model sits within the extensional one. It is the
restriction to "kosher" types, i.e. Kan complexes.

Thomas





[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: are fibrations evil?

[Peter LeFanu Lumsdaine]

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

Re: are fibrations evil?

[Michael Shulman]

The usual notion of (Grothendieck) fibration is indeed non-kosher, but
there is a variant due to Ross Street which is not.  This variant is
reproduced at

http://ncatlab.org/nlab/show/Grothendieck+fibration#StreetFibration

As remarked there, almost any fibration which arises in practice
indeed satisfies the stronger non-kosher condition, and a functor is a
Street fibration iff it factors as an equivalence of categories
followed by a Grothendieck fibration.  However, when working
internally to a bicategory where the non-kosher version doesn't even
make sense, Street's version is essential.

Regarding groupoids, it's easy to see that every functor between
groupoids is a Street fibration.  Grothendieck fibrations between
groupoids can be identified with "isofibrations," which are the
fibrations in the canonical model structure on Gpd.  It seems to me
that the use of groupoid fibrations in the groupoid model of type
theory is really an artifact of the desire to describe that model
treating Gpd as a 1-category, rather than a 2-category.  If one
defined the identity types and pullbacks using limits in Gpd in the
kosher 2-categorical sense, then it seems to me that one should be
able to define an equivalent model using arbitrary functors between
groupoids to represent the dependent types, rather than merely the
fibrations.

Similarly, in homotopical models of type theory where the dependent
types are represented by the fibrations in some model structure, it
seems that one should equivalently be able to work with the
oo-category presented by that model structure and use arbitrary maps,
but with all the structure defined using kosher oo-categorical limits.
  The non-kosher version using a model structure on a 1-category and
fibrations may certainly be *easier* to describe and work with, and
there is no reason not to do so in practice -- but just as is usually
the case in homotopy theory, it seems to me that one should regard
this as merely a convenient way to "present" the "real" underlying
structure, which is higher-categorical and kosher.

Mike

On Wed, Sep 15, 2010 at 4:43 AM, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> 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.
>
> This already happens if XX and BB are groupoids where P : XX -> BB is a
> fibration iff for all u : J -> I in BB and PX = I there is a map \phi :  Y -> X
> with P\phi = u.
>
> Ironically the category of groupoids and fibrations of groupoids as families
> of types was the first example of a model of type theory where equality may
> be interpreted as being isomorphic.
>
> So my conclusion is that equality of objects is sometimes absolutely
> necessary. Avoiding reference to equality is also not a question of using
> dependent types as some people implicitly seem to say. Even in intensional
> type theory there is a notion of equality. But it is sometimes inconvenient
> to use. As pointed out by Ahrens one can and should use extensional type theory
> whenever convenient.
> Intensional type theory allows one to interpret equality as being isomorphic,
> a kind of reward for the inconvenience of using intensional identity types.
>
> Thomas
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

are fibrations evil?

[Thomas Streicher]

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.

This already happens if XX and BB are groupoids where P : XX -> BB is a
fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X
with P\phi = u.

Ironically the category of groupoids and fibrations of groupoids as families
of types was the first example of a model of type theory where equality may
be interpreted as being isomorphic.

So my conclusion is that equality of objects is sometimes absolutely
necessary. Avoiding reference to equality is also not a question of using
dependent types as some people implicitly seem to say. Even in intensional
type theory there is a notion of equality. But it is sometimes inconvenient
to use. As pointed out by Ahrens one can and should use extensional type theory
whenever convenient.
Intensional type theory allows one to interpret equality as being isomorphic,
a kind of reward for the inconvenience of using intensional identity types.

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]