are fibrations evil?

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

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

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

Is equality evil?

[Vaughan Pratt]

Theorem.  Equality if and only if the diagonal.

Corollary.  P(equality) <--> P(contraction)

(where the predicate P may be "Evil", "Nonlinear", "Sophomoric", etc)

In this context (as opposed to metric spaces, materials, and maternity
wards) contraction is the logical rule predicated on the idea that two
things with the same name are actually one.  See Kripke and others on
the topic of Naming and Necessity.

Were Rosa Parks still around she would surely not judge equality evil.


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

why it matters that fibrations are "evil"

[Thomas Streicher]

Let BB be a (base) topos. Then split fibrations over BB correspond to
categories internal to Psh(BB). (Well, in Psh(BB) = Set^{BB^op} one has to
choose Set big enough!). Thus in Psh(B) one can speak about split fibrations
over BB as categories internal to Psh(BB).
To which extent can this be extended to arbitrary fibrations P : XX -> BB
typically not split. In a recent paper by Mike Shulman this has been
exercised for the fundamental fibration P_BB : BB^2 -> BB. (Well, he was even
exploiting that P_BB is a stack w.r.t. the regular topology on BB). But it
works for every fibration P. One can speak about P in a first order
dependently typed language L(P) without equality of objects. Generalized
elements of sort "object" at stage I are objects of the fibre P(I) and
similarly for morphisms. Now this language can be given a Kripke-Joyal
interpretation in BB. If P is a JJ-stack then one thinks of BB as endowed with
the topology JJ and incorporates this into the Kripke-Joyal interpretation.
The key trick is that implicitly one quantifies over all possible reindexings.
First I was quite enthusiastic about this because I thought that it augments
the usual fibrational foundations of category theory over an arbitrary base
topos with a linguistic framework entending that of the internal language
of the base (or rather (pre)sheaves over it).

But when trying to test the viability of this approach I came across the
following problem. It is not enough to quantify over objects but one also
has to quantify over families of objects indexed objects of BB.
This leads one to consider also the family fibration Fam(P) over BB together
with the cartesian functor FFam(P) from Fam(P) to P_BB. One can now easily
cook up a language speaking about P, Fam(P) and the cartesian functor FFam(P).
The first thing one wants to show is that the proposition
"Fam(P) is a fibration" holds under the Kripke-Joyal interpretation. But
when writing this down one sees that one cannot escape equality of objects
which has been dropped to make the whole thing possible.

Thus it might be easier to replace P by an equivalent split fibration Sp(P)
and reason about this in Psh(BB). Nothing seems to be lost when one considers
everything up to isomorphism. The question rather is whether this excessive
prevention of "evil" is appropriate. I have some doubts since it prevents
us from speaking about fibrations in a natural way.

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?

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

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?

[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?

[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: Is equality evil?

[Toby Bartels]

Thomas Streicher wrote in small part (in a post about fibrations):

>Even in intensional type theory there is a notion of equality.

Elsewhere in the same thread, Vaughan Pratt wrote:

>Theorem.  Equality if and only if the diagonal.

and concluded that equality is no more or less evil than contraction.


This depends on what kind of type theory you are using!

In the intentional type theory of Martin-Loef, for example,
there is a notion of equality (or identity) at each type.
Heck, there's even a notion of identity of types!
However, one can certainly consider type theory without identity types.
I would suggest the internal language of a Heyting 2-pretopos
(although that depends on what one takes this language to be).

Logic should be the servant of intuition, not the master.
If some category theorists have the intuition (and we do)
that it is meaningless to speak of equality of objects,
then it's the job of the logician to find a formal language
which expresses only what these category theorists find meaningful.
If they haven't done so, then this is something to work on,
not an argument that the motivating intuitions are invalid.

There is something else that logic can do, however:
it can show that identity follows from something else.
Vaughn's theorem (cited above) purports to do this,
but it is based on the assumption that every operation between types
(in this case, the diagonal Delta_X: X -> X x X)
has (as "image" or "range") a predicate on the target type
(in this case, the identity predicate on X x X).
So if our intuition suggests that operations have ranges,
then we must accept that we have identity predicates too
(assuming that we can construct the diagonal operation using contraction).

But my intution suggests no such thing for arbitrary types
(such as might be suitable as the type of objects of a category);
naively, given an operation f: X -> Y, the range predicate (ran f) on Y
would hold at those objects of Y with the form f(a) for some object a of X.
But given an object b of Y, how do you determine if it has this form?
If we already had an identity predicate =_Y on Y, then we could do this:
(ran f)(b) if and only if (for some x: A) (b =_Y f(a)).
But in general, I don't see any meaning for the range of an operation.

In fact, since I'm happy to use contraction in general mathematics,
I would phrase Vaughn's theorem as follows:

>Theorem.  Equality if and only if ranges.

and conclude that equality is no more or less evil than ranges.
But I don't believe in either of these, in general;
that is, I believe in the usefulness of types that lack these.

(Quiz:  Given two arbitrary sets, say the set of natural numbers
and the set of positive integers, how do you decide if they are equal?
Similarly, given a set and an arbitrary operation on sets,
say the set of rational numbers and the operation of cartesian square,
how do you decide if the set belongs to the range of the operation?
Or more relevantly, given the diagonal operation on sets,
how do you decide if a pair of sets belongs to its range?)


--Toby


[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: Is equality evil?

[Thomas Streicher]

It's no problem to come up with logics without equality predicates. Just
omit the equality predicate and its associated axioms. For ideological reasons
most logic texts give equality a distinguished status for historical reasons.
In case of extensional theories it suffices to have equality on base type and
lift it `a la logical relations. But then there might be operations which
don't respect this kind of equality. In other words identity types are not
necessary for doing constructive mathematics.
Intensional Id-types arise from putting the idea to an extreme that all logical
concepts are "inductively defined", i.e. are given by constructors and
eliminators.
The notion of equality of types you refer to is a different one. Namely
judgemental equality which cannot be used as an ingredient for forming
propositions.

It seems to me t that the point simply is that use of equality in premisses
can be avoided by declaring varibales appropriately. That trick goes a long
way in basic category theory.

Using Id-types is a different thing. Extensional Id-types together with sums
correspond to "cartesian logic" which suffices for declaring a lot of
categorical concepts.

Intensional Id-types might be convenient for providing a logic where equality
gets identified with isomorphism or even weak equivalence. But that's not
avoiding equality it's rather `liberal'ising it.

Thomas


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

Re: Is equality evil?

[Erik Palmgren]

Thanks Thomas for bringing up the intensional type theory perspective. Here
equality of objects in categories is a serious problem already for sets,
or rather for their type theoretic counterpart, setoids (types with
equivalence classes). The so-called identity types give a minimal
equality on each type A: Id(A,a,b) are the proofs that a and b
are equal in A. But the fact that these proofs are in general not
unique and induces a groupoid structure makes it difficult to apply
when e.g. A is a universe of types. Some remarks are contained in
in this preprint

http://www.mittag-leffler.se/preprints/files/IML-0910f-36.pdf


If one tries to use the Id-types to define equality on (small) setoids
one ends up with a groupoid of objects rather than a setoid objects.
I think the situation can be described as follows for a general category K,
which we think of as a category without equality of objects. We now
want to induce an equality of objects on (a part of) K. Take a
groupoid G and a functor F:G -> K. We define the groupoids of
objects C_0, arrows C_1 and composable arrows C_2 in a natural
way. C_0 is G and C_1 has for objects triples (a,b,f) where a,b in G
and f:F(a) -> F(b), and a morphism (a,b,f) -> (a',b',f') is a pair of
G morphisms r:a -> a' and s:b -> b' with F(s) f = f' F(r). C_2 has for
objects pairs of morphisms composable with an mediating map m from G,
i.e. ((a,b,f),(c,d,g),m). The composition is g F(m)f. The morphisms of
C_2 are then pairs of C_1 morphisms

((r,s), (t,u)): ((a,b,f),(c,d,g),m) -> ((a',b',f'),(c',d',g'),m')

with m's= t m.

When G is a discrete groupoid this becomes a standard category. When G is
a groupoid it becomes almost a category. Notions of limits can be
formulated in a natural fashion. At least when K=Setoids, C inherits
limits from K. Perhaps some general results are known about this
construction of C from functor F:G -> K on a groupoid G?


Erik


> It's no problem to come up with logics without equality predicates. Just
> omit the equality predicate and its associated axioms. For ideological reasons
> most logic texts give equality a distinguished status for historical reasons.
> In case of extensional theories it suffices to have equality on base type and
> lift it `a la logical relations. But then there might be operations which
> don't respect this kind of equality. In other words identity types are not
> necessary for doing constructive mathematics.
> Intensional Id-types arise from putting the idea to an extreme that all logical
> concepts are "inductively defined", i.e. are given by constructors and
> eliminators.
> The notion of equality of types you refer to is a different one. Namely
> judgemental equality which cannot be used as an ingredient for forming
> propositions.
>

......

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

Re: Re: are fibrations evil?

[Michael Shulman]

On Sat, Sep 18, 2010 at 6:48 AM, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
> 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.

I didn't mean to imply that there was.  In general, a given kosher
concept may correspond to more than one non-kosher concept.  For
instance, the notion of "weak n-category" is believed to be
"semi-strictifiable" in multiple incompatible ways.  It's known for
n=3 that one can either make associativity and units strict but keep
interchange weak, or make associativity and interchange strict but
keep units weak, but one cannot make everything strict.  However, if
we choose a particular corresponding non-kosher concept, then we can
talk about (semi)strictification of individual objects.

Mike


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

Re: Is equality evil?

[Toby Bartels]

Thomas Streicher wrote in part:

>Intensional Id-types might be convenient for providing a logic where equality
>gets identified with isomorphism or even weak equivalence. But that's not
>avoiding equality it's rather `liberal'ising it.

Right.  I would prefer to use no identity types at all.
If there is a particular predicate (on some particular type)
that you would like to think of as equality (on that type),
then write down its definition and introduce a symbol for it.
But I would not write any particular predicate into the language,
even with intensional behaviour, if I don't need it.

However, it is interesting that intentional identity types/predicates
satisfy weaker axioms than the extensional equality of first-order logic,
enough so that we are still driven away from using strict concepts.

>identity types are not necessary for doing constructive mathematics.

Nor for nonconstructive mathematics; excluded middle is a red herring.
Type theory naturally lends itself to constructive interpretation,
but one can add rules for excluded middle, even the axiom of choice,
if one wants to do classical mathematics.

However, questions of predicativity ARE important.
(Some type theories become impredicative when excluded middle is added,
  as Martin-Loef's do, but not all do; impredicativity is what matters.)
In sufficiently impredicative mathematics, identity can be defined:
  Given a type A and elements x and y of A, x is _identical_ to y
  if, for every predicate p on A, p holds for x iff p holds for y.
(This definition is usually attributed to Gottfried Leibniz.)
So you get an identity predicate by quantifying over all predicates,
in a theory that allows this.

It would be interesting to hear from people who want to keep kosher,
but also want to reason impredicatively, how to interpret this definition.
(For my part, I want to be both kosher *and* predicative by default,
  only abandoning predicativity when this seems to be needed.
  Very little basic category theory relies on impredicative reasoning.)

>The notion of equality of types you refer to is a different one. Namely
>judgemental equality which cannot be used as an ingredient for forming
>propositions.

Quite right; I really should not have mentioned that at all.
So everyone, delete this line from your memory of my previous post:
>>Heck, there's even a notion of identity of types!

Identity judgements are less problematic than identity types.
And some form of identity judgement seems to be necessary
to fully develop foundational-strength dependent type theory.
Actually, I don't so much seem to need identity judgements
as beta-convertibility (although you can define beta-equivalence
in terms of beta-convertibility, and call that identity).
I started to write this up once, but I never finished it.

The point is that one can recognise that two syntactic expressions,
such as x and x, are the same, or even that one reduces to another,
such as fst(x,y) and x (where fst: A x B -> A is the usual projection),
but this is different from taking two completely different expressions,
such as x and y, and considering the hypothesis that they are the same.


--Toby


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

Re: Is equality evil?

[Thomas Streicher]

I suspected already that you want to use no identity types at all.
Well, in category theory one needs at least equality on morphisms.

What I meant was that when one just considers finite types over a base type
(typically N) one can use an equality defined by recursion on the type
structure. But that's an ontology good for analysis and not for category
theory. Moreover, there will be maps between these types which don't respect
the inductively defined equality.

Alternatively, one coud work with setoids as suggested by Palmgren. But
that has also its intricacies since the binary predicates forming part of
setoids are proof-relevant in general (see Palmgren's posting).

As to Leibniz equality. If x and y are Leibniz equal, i.e.
\forall P : A -> Prop. P(x) -> P(y), then this doesn't allow one to
construct a map B(x) -> B(y) in case B : A -> Set (simply because Set is not
Prop).

Of course, dropping impredicativity you loose the theory of toposes. But
maybe that's not so bad since van den Berg and Moerdijk have developed
predicative algebraic set theroy in a sequence of papers available on the
arXiv. Predicative topos theory is less well developed. But notice that they
work with extensional equality (expressed by the reqirement that regular monos
are small).

I must say I remain unconvinced about working without equality as long as
I haven't seen a convincing account of (presheaf) toposes and fibered
categories in such a restricted setting. But presumably, people have other
application areas in mind. It would be interesting to identify those.

Thomas


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

Re: Is equality evil?

[Bas Spitters]

> Intensional Id-types might be convenient for providing a logic where equality
> gets identified with isomorphism or even weak equivalence. But that's not
> avoiding equality it's rather `liberal'ising it.

Vladimir Voevodsky just posted a draft manuscript about these issues:
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html

Bas


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

Re: Is equality evil?

[Michael Shulman]

On Tue, Sep 21, 2010 at 9:00 PM, Toby Bartels
<toby+categories@ugcs.caltech.edu> wrote:
> In sufficiently impredicative mathematics, identity can be defined:
>  Given a type A and elements x and y of A, x is _identical_ to y
>  if, for every predicate p on A, p holds for x iff p holds for y.
> ...
> It would be interesting to hear from people who want to keep kosher,
> but also want to reason impredicatively, how to interpret this definition.

Well, if "for every predicate" is to be interpreted as ranging only
over kosher predicates, then x and y are Leibniz identical as soon as
they are isomorphic (or equivalent, or whatever is appropriate).  Note
that in order for the notion of "keeping kosher" to even be
meaningful, you need the type A to "come with" some sort of notion of
equivalence between its elements; assigning it after the fact isn't
good enough.  But if A does have such a notion, then it seems that
Leibniz identity is provably equivalent to "there exists an
equivalence between x and y," by applying the definition of Leibniz
identity to the property p(z) = "there exists an equivalence between x
and z".

> As to Leibniz equality. If x and y are Leibniz equal, i.e.  \forall
> P : A -> Prop. P(x) -> P(y), then this doesn't allow one to
> construct a map B(x) -> B(y) in case B : A -> Set (simply because
> Set is not Prop).

Of course, this makes sense from the perspective above, since there's
no reason to expect that simply knowing that there *exists* an
equivalence between x and y would determine a map B(x) -> B(y); you
need to first pick a particular such equivalence.  I find this to be a
good reason for (intensional) identity types, whose elimination rule
provides a map (indeed, an equivalence) B(x) -> B(y) for any
inhabitant of Id(x,y).  In fact, the inductive notion of identity
types, as used in Voevodsky's foundations:

Inductive paths (T:Type)(t:T): T -> Type := idpath: paths T t t.

seems to me to essentially define it by strengthening Leibniz identity
to allow elimination into Set/Type as well.

Mike


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