the definition of "evil"

the definition of "evil"

[Peter Selinger]

Dear all,

sorry for sending yet another message on the topic of "evil"
structures on categories. After some interesting private replies, as
well as Dusko's latest message (which should have appeared on the list
by the time you read this), I noticed that not everyone is agreeing on
the technical meaning of the term "evil". I will therefore attempt to
state a more precise technical definition of the term as I have used
it. Perhaps 2-category theorists already have another name for this.

The information definition I had used is that a structure is "evil" if
it does not "transport along equivalences of categories". I thought it
was reasonably obvious what was meant by "transport along", but there
is actually a lot of variation in what people understand this phrase
to mean.

John Baez gave a pointer to a website containing a technical
definition of "evil": http://ncatlab.org/nlab/show/evil.
Unfortunately, this site only speaks of properties, not structures. It
is easy to state what it means for a property of categories to be
transported along equivalences: namely, if C has the property, and C
and C' are equivalent, then C' has the property. Structures are more
tricky.

Certainly, it should not just mean that if C admits such a structure,
and C' is a category equivalent to C, then C' admits such a structure.
(Then "admitting a structure" would merely be a property).  This seems
to be the definition Dusko has used. If we used this definition, there
would be almost no evil structures; in particular, the original
(strict) notion of dagger category is not evil in this sense.  Dagger
structure is reflected by full and faithful functors, and therefore by
one half of an equivalence. The point is that the other half won't
respect it.

At least to me, "transported" suggests that the given equivalence
respects the structure in some sense. So here is my attempt at a
definition.

 DEFINITION. Let X be some structure on categories. By this, I mean
 that there is a given 2-category called X-Cat, whose objects are
 called X-categories, whose morphisms are called X-functors, and whose
 2-cells are called X-transformations, and for which there is a given
 2-functor U to Cat, called the forgetful functor.

 We say that X is "transported along equivalences of categories" if the
 following holds. Given an X-category D', with underlying category D =
 U(D'), and a category C, and an equivalence (F,G,e,h) of categories D
 and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D,
 it is then possible to find:

 (1) an X-category C' whose underlying category U(C') is isomorphic
     [not equivalent!] to C. Let c : U(C') -> C be the isomorphism
     (i.e., an invertible functor in Cat) with inverse c': C -> U(C');

 (2) an X-equivalence of X-categories (F',G',e',h'), where
     F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D'
     [the concept of equivalence makes sense in any 2-category];

 such that

 (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h).

 Here, cF and Gc' denotes composition of functors, and cec' denotes
 whiskering.

 The structure X is called "evil" iff it is not transported along
 equivalences of categories.

 This finishes the definition.

More informally, "transported along equivalences" therefore means that
if D and C are equivalent, and D has an X-structure, then there is a
way to equip C with an X-structure and to lift the original equivalence
to an X-equivalence.

There was a need for the isomorphism c in the definition, because the
forgetful functor U : X-Cat -> Cat may not be strictly speaking
surjective onto 0-cells in some real-life examples (and in any case,
this forgetful functor may sometimes only be well-defined up to
isomorphism). It is important that c is an isomorphism, rather than an
equivalence, because else the definition becomes vacuous (and we are
precisely interested in notions that are not well-defined up to
equivalence).

Also note that I didn't require the data (C',F',G',e',h') to be
unique, not even up to equivalence in X-Cat. Although in practice, it
will often be unique in this sense. So my definition allows for a
given structure to be transported "in essentially more than one way"
along a given equivalence. I am open to strengthening the definition
to forbid this.

It is clear that the definition generalizes to any 2-category instead
of Cat, so one might for example speak of structures on monoidal
categories, or on categories-with-a-distinguished-subcategory, or even
on dagger categories, as being evil or not.

Here are some examples of structures:

* monoidal structure on categories is non-evil (for concreteness,
  taken with strong monoidal functors and monoidal natural
  transformations).

* strict monoidal structure is evil, when taken with strict monoidal
  functors. With strong monoidal functors, I think it is still evil,
  but I am not sure at this late hour.

* dagger structure is evil. More generally, any structure X with which
  one can equip FHilb (the category of finite dimensional Hilbert
  spaces), and which allows a definition of unitary map that includes
  all identities and that coincides with the usual one on FHilb, and
  for which the full and faithful X-functors preserve and reflect
  unitary maps, is evil. Here is the technical argument again, as it
  seems to have been misunderstood. The forgetful functor
  F : FHilb -> FVect induces an equivalence, whose other half
  G : FVect -> FHilb requires a choice of inner product on each finite
  dimensional vector space. Define such a G in some way. Fix some
  X-structure on FVect. Let V be some non-trivial vector space, and
  let i and j be two different inner products on V. Then (V,i) and
  (V,j) are Hilbert spaces, so different objects of FHilb.  Consider
  the morphism (in FHilb) f:(V,i) -> (V,j) given by f(v) = v. It is
  evidently not unitary. However, we have F(f) = id_V: V -> V, which
  is unitary, no matter the X structure that was chosen on FVect.
  So F does not reflect unitary maps. QED.

  Note that it is F, not G, that is causing problems. As remarked
  above, since G is full and faithful, it is possible to successfully
  reflect the dagger structure along G to FVect. This amounts to
  arbitrarily choosing some inner product on each vector space. But it
  won't be compatible with F.

  Also note that this argument is independent of the definition of the
  2-cells of X-Cat. So it is even valid for some weaker definitions of
  "evil", for example, if one only requires F and G to lift to
  X-functors, rather than to an X-equivalence.

  I will argue that any structure X that claims to be a "weak" version
  of dagger structure should at least satisfy the conditions I listed
  as preconditions for the argument above. This is the basis for my
  claim that no construction such as Toby's or Dusko's can succeed in
  producing a non-evil equivalent of dagger structure.

* the structure of "being equipped with a chosen Frobenius structure
  on each object" is evil, relative to monoidal categories.

* the structure of "being equipped with an identity-on-objects
  covariant functor" is evil.

* more generally, the structure of "being equipped with a chosen
  subcategory" is evil, unless the subcategory is required, as part of
  the structure, to contain all isomorphisms (in which case it is not
  evil).

* poset-enrichment (with composition f o g monotone in f and g) is
  non-evil.

* The following structure is evil: equip a category with a partial
  order on each hom-set, so that composition f o g is monotone in g,
  but not necessarily in f. Proof: Given such a structure on any
  category, define g:A->B to be "monotone" if (X,g) : (X,A) -> (X,B)
  is monotone for all X.  Consider the category whose objects are
  partially-ordered sets, and whose morphisms are *all* functions
  (thanks to Fred Linton for this example). It can be equipped with
  the aforementioned structure, by giving the pointwise ordering to
  the functions in each hom-set.  As a category, it is equivalent to
  Set. The rest of the argument proceeds as above for Hilbert spaces,
  with "monotone" instead of "unitary": take some non-trivial set with
  two different partial orders, then the identity is non-monotone,
  etc.

The last example is almost an enrichment in Poset, but instead of the
usual cartesian product on Poset, we have used another bifunctor on
Poset, given by cartesian product P x Q of the underlying sets, with
the non-standard order defined by (p,q) <= (p',q') iff p=p' and
q<=q'. This operation is bifunctorial and associative, but not quite
monoidal, because it lacks a right unit. More generally, taking
"enrichments" in such almost-monoidal categories often yields evil
structures. An analogous example works for the category of finite
abelian groups and all set-theoretic functions.

Happy new year to all, -- Peter


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

re: the definition of "evil"

[Claudio Hermida]

Peter Selinger wrote:

 DEFINITION. Let X be some structure on categories. By this, I mean
 that there is a given 2-category called X-Cat, whose objects are
 called X-categories, whose morphisms are called X-functors, and whose
 2-cells are called X-transformations, and for which there is a given
 2-functor U to Cat, called the forgetful functor.

 We say that X is "transported along equivalences of categories" if the
 following holds. Given an X-category D', with underlying category D =
 U(D'), and a category C, and an equivalence (F,G,e,h) of categories D
 and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D,
 it is then possible to find:

 (1) an X-category C' whose underlying category U(C') is isomorphic
     [not equivalent!] to C. Let c : U(C') -> C be the isomorphism
     (i.e., an invertible functor in Cat) with inverse c': C -> U(C');

 (2) an X-equivalence of X-categories (F',G',e',h'), where
     F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D'
     [the concept of equivalence makes sense in any 2-category];

 such that

 (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h).

 Here, cF and Gc' denotes composition of functors, and cec' denotes
 whiskering.

 The structure X is called "evil" iff it is not transported along
 equivalences of categories.

 This finishes the definition.

More informally, "transported along equivalences" therefore means that
if D and C are equivalent, and D has an X-structure, then there is a
way to equip C with an X-structure and to lift the original equivalence
to an X-equivalence.

There was a need for the isomorphism c in the definition, because the
forgetful functor U : X-Cat -> Cat may not be strictly speaking
surjective onto 0-cells in some real-life examples (and in any case,
this forgetful functor may sometimes only be well-defined up to
isomorphism). It is important that c is an isomorphism, rather than an
equivalence, because else the definition becomes vacuous (and we are
precisely interested in notions that are not well-defined up to
equivalence).

Also note that I didn't require the data (C',F',G',e',h') to be
unique, not even up to equivalence in X-Cat. Although in practice, it
will often be unique in this sense. So my definition allows for a
given structure to be transported "in essentially more than one way"
along a given equivalence. I am open to strengthening the definition
to forbid this.



Dear all,

A quick pointer to a variation on this matter, which has already been around
(I presented it at CT07).
The nature of 2-categorical structures that transport along equivalences is
nicely captured by the notion of Equ-iso-fibration:

DEFINITION
A 2-functor F:E → B is an Equ-iso-fibration if:

 - it admits cartesian liftings of (adjoint) equivalences and

 - every hom F(X,Y):E(X,Y) → B(FX,FY) admits cartesian lifitings of
isomorphism 2-cells, and such liftings are preserved by precomposition
(pointwise).

Notice that a cartesian lifting of an adjoint equivalence is another such.
The notions of cartesian liftings used here are those for 2-fibrations (as
in the references below); they involve the expected 2-dimensional property
for 1-cells.
The liftings are strict.

The most interesting example of such a structure is the forgetful functor of
a 2-cateogory of pseudo-algebras
V: Ps-T-Alg → K, for a 2-monad T on a 2-category K (or a pseudo-monad on a
bicategory). They include all the known interesting examples of
pseudo-structures, the classical such being monoidal categories. The
morphisms in Ps-T-Alg are strong ones, preserving structure up to coherent
isomorphism. The observation that pseudo-algebras do transport along
equivalences is credited to Max Kelly in Power´s article below.

I used this notion to capture the following universality of coherence:
coherence for such pseudo-algebras (meaning that we can strictify every
pseudo-algebra into a equivalent strict T-algebra) is equivalent to the
statement

THM: The inclusion 2-functor J: T-alg → Ps-T-alg makes V: Ps-T-alg → K the
FREE Equ-iso-fibration over
U:T-alg → K

In other words, the passage from strict algebras (with their strict
morphisms) to pseudo-algebras (and strong morphisms) is the universal way of
achieving transportability along equivalences.

Claudio

References

- C.Hermida, Some properties of Fib as a fibred 2-category, JPAA, *134 (1),
83-109, 1999*

- C.Hermida, Descent on 2-fibrations and 2-regular 2-categories, Applied Cat
Str, *12(5-6), 427--459, 2004*

- A.J.Power, A general coherence result,


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

re: the definition of "evil"

[John Baez]

Dear Categorists -

I'm glad Peter is trying to formulate a definition of structures that can be
transported along equivalences, and I like the spirit of his definition,
namely in terms of a "lifting property" where one has a 2-functor

U: XCat -> Cat

and one is trying to lift equivalences from Cat to XCat.

But it makes me nervous when he says "isomorphic [not equivalent!]".  Just
as evil in category theory typically arises from definitions that impose
equations between objects instead of specifying isomorphisms, evil in
2-category theory typically arises when we specify isomorphisms between
objects instead of specifying equivalences.

It would be sad, or at least intriguing, if the definition of "evil" was
itself evil.

Best,
jb

  DEFINITION. Let X be some structure on categories. By this, I mean
>  that there is a given 2-category called X-Cat, whose objects are
>  called X-categories, whose morphisms are called X-functors, and whose
>  2-cells are called X-transformations, and for which there is a given
>  2-functor U to Cat, called the forgetful functor.
>
>  We say that X is "transported along equivalences of categories" if the
>  following holds. Given an X-category D', with underlying category D =
>  U(D'), and a category C, and an equivalence (F,G,e,h) of categories D
>  and C, where F: D -> C, G: C -> D, and e: FG -> id_C, h: GF -> id_D,
>  it is then possible to find:
>
>  (1) an X-category C' whose underlying category U(C') is isomorphic
>     [not equivalent!] to C. Let c : U(C') -> C be the isomorphism
>     (i.e., an invertible functor in Cat) with inverse c': C -> U(C');
>
>  (2) an X-equivalence of X-categories (F',G',e',h'), where
>     F': D' -> C', G': C' -> D', e': F'G' -> id_C', and h': G'F' -> id_D'
>     [the concept of equivalence makes sense in any 2-category];
>
>  such that
>
>  (3) (U(F'), U(G'), U(e'), U(h')) = (cF, Gc', cec', h).
>
>  Here, cF and Gc' denotes composition of functors, and cec' denotes
>  whiskering.
>
>  The structure X is called "evil" iff it is not transported along
>  equivalences of categories.
>
>  This finishes the definition.
>
>


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

Re: the definition of "evil"

[Urs Schreiber]

On Sun, Jan 3, 2010 at 8:23 AM, Peter Selinger <selinger@mathstat.dal.ca> wrote:

> John Baez gave a pointer to a website containing a technical
> definition of "evil": http://ncatlab.org/nlab/show/evil.
> Unfortunately, this site only speaks of properties,
> not structures.

Fortunately, though, everybody can and is invited add to this site! So
eventually it may speak also of structures --  and much more.

This site was created for exactly the kind of situation we have here:
we have an intersting technical discussion on a mailing list or
similar forum. After a while it will end and a bunch of scattered
messages will remain in the archives of the mailing list. The
important insight gained or exhibited in the discussion will be
non-trivial to find and deduce from the archived discussion threads.
It'll be a shame if all the valuable insight of various participants,
all the energy they invested into composing these messages, find no
more focused and polished incarnation than that.

The above site is meant to provide a place where results of such
discussion is collected in a more useful form. I am hoping that
eventually the upshot of the discussion on "evil" had here on the list
will eventually find a nice incarnation on that site. Everyone can
help to make that come true. Just hit the "edit" button at the bottom
of the page:

http://ncatlab.org/nlab/edit/evil

Best,
Urs


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

re: the definition of "evil"

[Michael Shulman]

It looks to me like there are (at least) two different ideas of "evil"
floating around.


1. A property or structure (on objects of a 2-category) is "non-evil" if
it can be transported along equivalences.

This is clearly a property of a forgetful 2-functor, which I agree that
it makes the most sense to formulated as a lifting property for entire
(adjoint) equivalences, including both functors and the unit and counit.
 (I'm surprised that Peter didn't require (F,G,e,h) and (F',G',e',h') to
be *adjoint* equivalences in his definition; that seems to me likely to
be the more correct notion.)  Thus, whether a given structure is "evil"
in this sense depends on what you are forgetting down to.  Dagger
structure is evil as structure on a category, but it is not evil as
structure on a "category equipped with a distinguished subgroupoid."
(Of course, a distinguished subgroupoid is evil as structure on a category.)

I also think that this notion must necessarily be "2-evil" in the way
that makes John sad, for anything at all is always "transportable along
an equivalence up to equivalence"!  In other words, if we are serious
about avoiding evil, even at a higher-categorical level, then we
shouldn't even be talking about evil in the first place.  (-:

(Of course, that also suggests that we probably can't construct, by
purely non-2-evil (e.g. bicategorical) means, the 2-category of dagger
categories from the 2-category of categories.  But we can construct
something pretty close, e.g. if we weaken "distinguished subgroupoid" to
"faithful functor with groupoidal domain.")


2. A categorical structure is "evil" if it involves talking about
equality of objects.

For this sense, one has to be careful, because lots of notions in
category theory involve equality of objects.  In order to compose two
morphisms f:A-->B and g:B-->C one has to know that the target of f is
*equal* to the source of g.  Likewise, to say that f:A-->B is an
isomorphism, one has to say that there is an inverse g:B-->A whose
source and target are *equal* to the target and source of f,
respectively.  However, as Toby says, there is a precise way to say that
something is "not evil" in this sense while still admitting all of these
"natural" constructions.  Namely, we work in a dependent type theory
with a type Ob of objects, and for each pair of objects x,y a dependent
type Hom(x,y) of arrows, and stipulate that our theory contains an
equality predicate only for the types Hom(x,y) and not for Ob.
(Makkai's FOLDS, which Toby mentioned, is a generalization of this
appropriate for higher-categorical structures.)

The point is that specifying the source and target of an arrow should
not be thought of as "talking about equality of objects," but rather as
a *typing assertion*.  What is forbidden is rather asking whether two
already *given* objects are equal, not introducing an arrow whose source
and target are ("equal to") some pair of already given objects.  The
notion of "dagger category" can be formulated in this dependently-typed
language, as Toby has said, so it is *not* evil in this sense.  This is
related to the observation that dagger-categories are still
"implementation-independent" relative to membership-based set theory,
e.g. for the dagger-structure on Hilb it doesn't matter whether you
define the real numbers as Cauchy sequences or Dedekind cuts.


The relationship between these two notions is not immediately obvious to
me.  Clearly evil (1) does not imply evil (2), because of the example of
dagger-categories.  Does evil (2) imply evil (1)?

Best,
Mike

John Baez wrote:
> Dear Categorists -
>
> I'm glad Peter is trying to formulate a definition of structures that can be
> transported along equivalences, and I like the spirit of his definition,
> namely in terms of a "lifting property" where one has a 2-functor
>
> U: XCat -> Cat
>
> and one is trying to lift equivalences from Cat to XCat.
>
> But it makes me nervous when he says "isomorphic [not equivalent!]".  Just
> as evil in category theory typically arises from definitions that impose
> equations between objects instead of specifying isomorphisms, evil in
> 2-category theory typically arises when we specify isomorphisms between
> objects instead of specifying equivalences.
>
> It would be sad, or at least intriguing, if the definition of "evil" was
> itself evil.
>
> Best,
> jb
>

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

dagger not evil

[Joyal, André]

Dear Peter and all,

I cannot resist adding my grain of salt to the ongoing 
discussion on dagger categories.

I will take the point of view of a homotopy theorist.
Recall that the category of small categories Cat admits a
"natural" model structure (called the "folk" model structure
for the wrong reason by the folks). 

The category of small dagger categories DCat also admits 
a "natural" model structure. A dagger functor f:A-->B
is a weak equivalence iff it is fully faithful and 
unitary surjective (this last condition means that every object of B
is unitary isomorphic to an object in the image of the functor f).
The cofibrations and the trivial fibrations are as in Cat.
A fibrations is a unitary isofibration (a map having the lifting
property for unitary isomorphisms).

The forgetful functor DCat ---> Cat is a right adjoint
but it is not a right Quillen functor with respect to the
natural model structures on these categories.
In other words the forgetful functor DCat ---> Cat is wrong.
This may explains why a dagger category cannot be
regarded as a category equipped a homotopy invariant structure.
But I claim that the notion of dagger category is perfectly reasonable
from an homotopy theoretic point of view.
This is because the model category DCat is combinatorial.
It follows, by a general result, that the notion of
of dagger category is homotopy essentially algebraic
There a homotopy limit sketch whose category of models (in spaces)
is Quillen equivalent to the model category DCat.
This is true also for the model category Cat.

There should be a notion of dagger quasi-category.
A dagger simplicial set can be defined to be a simplicial set X
equipped with an involutive isomorphism dag:X-->X^o  
which is the identity on 0-cells.
The category of dagger simplicial sets (and dagger preserving maps)
is the category of presheaves on the category whose objects are the ordinals [n]
but where the maps [m]-->[n] are order reversing or preserving.

Finally, the (homotopy) trace of a category (resp. quasi-category) has
the structure of a cyclic set in the sense of Connes.
I conjecture that the (homotopy) trace of a dagger category (resp. dagger quasi-category)
has the structure of a dihedral set in the sense
of Fiedorowicz and Loday.

Happy New Year to all!
andré

PS: I will be quiet during the next few weeks.


-------- Message d'origine--------
De: categories@mta.ca de la part de Peter Selinger
Date: dim. 03/01/2010 02:23
À: Categories List
Objet : categories: the definition of "evil"
 
Dear all,

sorry for sending yet another message on the topic of "evil"
structures on categories. After some interesting private replies, as
well as Dusko's latest message (which should have appeared on the list
by the time you read this), I noticed that not everyone is agreeing on
the technical meaning of the term "evil". I will therefore attempt to
state a more precise technical definition of the term as I have used
it. Perhaps 2-category theorists already have another name for this.

The information definition I had used is that a structure is "evil" if
it does not "transport along equivalences of categories". I thought it
was reasonably obvious what was meant by "transport along", but there
is actually a lot of variation in what people understand this phrase
to mean.

John Baez gave a pointer to a website containing a technical
definition of "evil": http://ncatlab.org/nlab/show/evil.
Unfortunately, this site only speaks of properties, not structures. It
is easy to state what it means for a property of categories to be
transported along equivalences: namely, if C has the property, and C
and C' are equivalent, then C' has the property. Structures are more
tricky.

....

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

Re: dagger not evil

[Toby Bartels]

André Joyal wrote in small part:

>In other words the forgetful functor DCat ---> Cat is wrong.

This reminds me of the fact that the obvious forgetful functor
Ban -> Set or Hilb -> Set (where now Hilb is just a category,
with short linear maps as morphisms, not a dagger category) is wrong.
That is, the wrong forgetful functor takes the set of points,
whereas the right one takes the set of points in the closed unit ball.
(Of course, both functors exist, but the right one is representable.)

While the obvious forgetful functor DCat -> Cat is wrong,
is there a right one?  In particular, we have a functor
Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms
and the functor DCat -> Grpd that takes the LS of unitary morphisms;
is there a functor DCat -> Cat that completes a commutative triangle?

Less rigorously but more concretely, can we start with Hilb+
(the dagger category with all bounded linear maps as morphisms)
and systematically derive the class of short linear maps,
much as we can systematically derive the class of unitary maps?
Offhand, I don't see how to do this.

(Note: "short" = "Lipschitz with Lipschitz constant at most 1",
so "short linear" = "bounded linear with norm at most 1".)


--Toby


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

dagger not evil (2)

[Joyal, André]

Dear Peter and all,

In my last message, I wrote that the forgetful functor DCat ---> Cat 
is wrong because it is not a right Quillen functor. 
The argument is not good enough.

I believe that a forgetful functor XStruc--->Cat should reflect 
weak equivalences in addition to preserving them.  

The forgetful functor DCat ---> Cat preserves weak equivalences
but it does not reflect them. 
Because two objects in a dagger category can be isomorphic
without been unitary isomorphic.

Best,
aj

-------- Message d'origine--------
De: Joyal, André
Date: mar. 05/01/2010 15:04
À: Peter Selinger; Categories List
Objet : dagger not evil
 
Dear Peter and all,

I cannot resist adding my grain of salt to the ongoing 
discussion on dagger categories.

I will take the point of view of a homotopy theorist.
Recall that the category of small categories Cat admits a
"natural" model structure (called the "folk" model structure
for the wrong reason by the folks). 

The category of small dagger categories DCat also admits 
a "natural" model structure. A dagger functor f:A-->B
is a weak equivalence iff it is fully faithful and 
unitary surjective (this last condition means that every object of B
is unitary isomorphic to an object in the image of the functor f).
The cofibrations and the trivial fibrations are as in Cat.
A fibrations is a unitary isofibration (a map having the lifting
property for unitary isomorphisms).


....


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

Re: dagger not evil

[Peter Selinger]

Toby Bartels wrote:
>
> Andr=E9 Joyal wrote in small part:
>
> >In other words the forgetful functor DCat ---> Cat is wrong.
>
> This reminds me of the fact that the obvious forgetful functor
> Ban -> Set or Hilb -> Set (where now Hilb is just a category,
> with short linear maps as morphisms, not a dagger category) is wrong.
> That is, the wrong forgetful functor takes the set of points,
> whereas the right one takes the set of points in the closed unit ball.
> (Of course, both functors exist, but the right one is representable.)
>
> While the obvious forgetful functor DCat -> Cat is wrong,
> is there a right one?  In particular, we have a functor
> Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms
> and the functor DCat -> Grpd that takes the LS of unitary morphisms;
> is there a functor DCat -> Cat that completes a commutative triangle?

There is, because Cat -> Grpd is right invertible, but that is
probably not the functor you had in mind.

> Less rigorously but more concretely, can we start with Hilb+
> (the dagger category with all bounded linear maps as morphisms)
> and systematically derive the class of short linear maps,
> much as we can systematically derive the class of unitary maps?
> Offhand, I don't see how to do this.
>
> (Note: "short" = "Lipschitz with Lipschitz constant at most 1",
> so "short linear" = "bounded linear with norm at most 1".)
>
> --Toby

As far as I know, you can't do this with a dagger structure alone;
however, if you regard Hilb+ as a dagger category with dagger
biproducts, then the short linear maps are definable as those maps
f: A -> B satisfying

(1)  there exists some g: A -> C such that
               (f^dagger o f) + (g^dagger o g) = id,

or equivalently,

(2)  there exists some h: D -> B such that
               (f o f^dagger) + (h o h^dagger) = id.

In Hilb+, conditions (1) and (2) are equivalent for a given f.  In a
general dagger category with dagger biproducts, they are not
equivalent (as the example Rel shows), and one should in general
define a "short linear" morphism to be an f that satisfies both (1)
and (2). The always form a dagger subcategory.

In general, invertible + short linear, in this sense, does not imply
unitary. A counterexample is chosen-basis vector spaces over Z_2 (with
dot product as inner product), where all maps are short linear, but
not all invertible maps are unitary.

However, if one further assumes that the category satisfies the
following strictness condition:

(3)      1 + (g o g^dagger)  = 1     implies    g = 0,

then invertible + short linear implies unitary. So something like your
"right" forgetful functor DCat' -> Cat can be defined, where DCat' is
DCat equipped with these additional hypotheses. I don't know whether
there is a more organic definition that works in greater generality.

-- Peter



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

Re: dagger not evil

[Joyal, André]

Dear Toby

You wrote:

>While the obvious forgetful functor DCat -> Cat is wrong,
>is there a right one?  In particular, we have a functor
>Cat -> Grpd that takes the lluf subcategory (LS) of invertible morphisms
>and the functor DCat -> Grpd that takes the LS of unitary morphisms;
>is there a functor DCat -> Cat that completes a commutative triangle?

I will try answer your question, but my answer is wonkish.

First, a category can be regarded as a (simplicial) diagram of groupoids.
More precisely, every category C has a "Rezk nerve" RN(C)
which is a simplicial object in the category of groupoids.
By definition, we have

RN(C)_n=IsoNat([n],C)

for every non-negative integer n,
where IsoNat([n],C) denotes the groupoid of natural isomorphisms
in the category of functors [n]-->C.
The nerve RN(C) was first introduced by Charles Rezk in
http://arxiv.org/abs/math/9811037
The functor RN has very nice properties. 
It embeds the category Cat in the category
of simplicial groupoids Simp(Grpd). 
The embedding respects (ie preserves and reflects)
the equivalences defined on both sides,
where a map of simplicial groupoids f:X-->Y  
is defined to be an equivalence if it is an equivalence levelwise.
It can be proved that RN is a right Quillen functor
with respect to the natural model structure on Cat
and with respect to the Reedy model structure on Simp(Grpd).

A dagger category can also be regarded as a (dagger simplicial) diagram of groupoids.
More precisely, every dagger category C has a "unitary nerve" UN(C)
which is a dagger simplicial object in the category of groupoids.
By definition, we have

UN(C)_n=UIsoNat([n],C)

for every non-negative integer n,
where UIsoNat([n],C) denotes the groupoid of unitary natural isomorphisms
in the category of functors [n]-->C.
The functor UN embeds the category DCat in the category
of dagger simplicial groupoids DSimp(Grpd). 
The embedding respects the equivalences defined on both sides,
where a map of dagger simplicial groupoids f:X-->Y  
is defined to be an equivalence if it is an equivalence levelwise.

You wrote:

>Less rigorously but more concretely, can we start with Hilb+
>(the dagger category with all bounded linear maps as morphisms)
>and systematically derive the class of short linear maps,
>much as we can systematically derive the class of unitary maps?
>Offhand, I don't see how to do this.


I am afraid I dont have an answer to this question. 
But I will think about the problem.


Best,
André




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

equality is beautiful

[Joyal, André]

Dear All

Many people seem to distrust the equality 
relation between the objects of a (large) category.
Is this a philosophical conundrum or a mathematical problem?

Can we define a notion of (large) category without supposing 
that its (large) set of objects has a diagonal?


Best,
André



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

Re: equality is beautiful

[Steve Vickers]

On 9 Jan 2010, at 03:29, Joyal, André wrote:

> Dear All
>
> Many people seem to distrust the equality
> relation between the objects of a (large) category.
> Is this a philosophical conundrum or a mathematical problem?
>
> Can we define a notion of (large) category without supposing
> that its (large) set of objects has a diagonal

Dear Andre,

Can I explore this with regard to topologies?

Suppose we compare FinSet with Set, defining FinSet very small with N  
for its object space. The object diagonal N -> NxN is an open inclusion.

Now look at Set. The natural topology on the class of sets, as the  
Ind-completion of FinSet, is the one whose sheaves are given by the  
object classifier. Thus continuous maps from it are functorial and  
preserve filtered colimits (the categorical analogue of Scott  
continuity).

(This introduces a confusing issue. Functors from the category Set  
are already determined by their object maps. But it is a special  
category in which the morphism space is the comma object got from two  
copies of the identity map on the object space - we are using the  
fact that the category of spaces is actually a 2-category, using the  
specialization morphisms. FinSet was certainly not of this kind.)

Now the object diagonal is not even an inclusion, since it is not  
full. I would speculate, by analogy with what I know for ideal  
completions, that it is essential but not locally connected.

I don't really know what to make of this, but it does seem that there  
are topological distinctions to be made between the two categories  
based on object equality.

Now let me wonder about classifying toposes.

I love using them (as I did above), but they always seem slightly  
fuzzy because they are really defined only up to equivalence. So I  
certainly would distrust the object equality. I think the discussion  
becomes slightly sharper in terms of arithmetic universes (as  
mentioned by Paul Taylor) instead of toposes.

Given a base AU A0, there are two obvious places to look for an  
object classifier (representing the class of sets) a la Grothendieck  
topos theory. First, there is A0[U], the AU freely generated over A0  
by an object U. This can be constructed by universal algebra, and  
then is a classifying A0-AU (for the theory with one sort and no  
predicates, functions or axioms) characterized up to isomorphism with  
respect to strict A0-AU homomorphisms. However, its object equality  
depends rather delicately on the precise structure used to  
characterized AUs. For example, I suspect it will differ according as  
AUs are taken to have canonical pullbacks or canonical binary  
products and equalizers.

On the other hand, sheaf theory would suggest using the category Presh 
(FinSet^op) of internal diagrams over the internal FinSet in A0. I  
conjecture that this (is an AU and) is equivalent but not isomorphic  
to A0[U]. Hence there are issues of object equality when one compares  
them. (Milly Maietti and I are looking at "subspaces" in this AU  
setting, and again are having to be rather careful about equality and  
the distinction between strict and non-strict AU homomorphisms.)

A further issue, seen in AUs but not toposes, is that A0[U] can be  
internalized in A0, as the internal AU in A0 freely generated by one  
object. The comparison with the external A0[U] will presumably raise  
truth v. proof issues similar to those that you have already  
investigated for the initial AU and Goedel's Theorem.

To summarize:

(1) Granted the existence of the object diagonals, they may still  
have different topological characteristics for different kinds of  
categories.
(2) A universal characterization (such as for classifying toposes)  
that is only up to equivalence will make it difficult to rely on  
object equality.
(3) In arithmetic universes we can perhaps (allowing for the fact  
that the theory is not fully developed yet) see situations where the  
object equality definitely exists, but is sensitive to inessential  
differences.

Best regards,

Steve Vickers.




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

Re: equality is beautiful

[Vaughan Pratt]

Joyal wrote:
> Many people seem to distrust the equality
> relation between the objects of a (large) category.
> Is this a philosophical conundrum or a mathematical problem?

I don't even trust it for the *-autonomous category with two objects and
three morphisms.  This is the basis for the classical notion of truth as
normally understood when not trying to parse the sentences of
constructive mathematicians.

Some dark night someone could sneak into the basement where the
foundations of mathematics are stored and switch true and false around,
and in the morning we'd all wake up talking Doublespeak without even
realizing it.

Are you suggesting we should trust the equality relation between the
objects of that category?  Useful categories don't come much smaller.

It can't be a question of size because the free Heyting algebra on one
generator is infinite yet it doesn't have this structural ambiguity of
classical logic: we can trust its equality relation because we can tell
which element is the generator even if the arrows are accidentally
flipped---it's a sort of error-detection feature of that Heyting algebra
not possessed by any Boolean algebra.  This is a reason to prefer
intuitionistic logic over classical (not one I'd use myself mind you).

Best,
Vaughan


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

Re: equality is beautiful

[Richard Garner]

Dear André

> Many people seem to distrust the equality
> relation between the objects of a (large) category.
> Is this a philosophical conundrum or a mathematical problem?
>
> Can we define a notion of (large) category without supposing
> that its (large) set of objects has a diagonal?

Yes, this is precisely what one does in formalising category 
theory in an (intensional) dependent type theory. (Mike 
Shulman has alluded to this in a previous message to this 
list.)

Since in such a type theory one does not have quotients of 
equivalence relations, one typically works not with raw types 
but with setoids (=types equipped with an equivalence 
relation in the internal logic).

The category of such setoids is well behaved---at least an 
LCC pretopos---but the notion of internal category in this 
pretopos is generally not what one is interested in.

Instead one takes a category internal to the type theory to 
be given by a type of objects O, together with an OxO indexed 
family of hom-setoids O(x,y), composition and identities 
which are maps of setoids, and associativity and unitality 
witnessed by elements of the hom-setoid equality. In this 
setting, we may not talk of equality of objects (since O is 
not a setoid but only a type) but may talk of the equality of 
any pair of parallel arrows.

This notion is due to Peter Aczel and there is a fairly 
extensive development of it in the proof assistant Coq by 
Gérard Huet and Amokrane Saïbi. Some consequences of the 
definition are, e.g., that the collection of all small 
categories does no longer forms a category, but only a 
bicategory (since one cannot speak of equality of functors, 
since this would require equality of objects in the 
codomain). Some work on this has been done by Olov Wilander.

Since the category of sets is a model of extensional, and so 
also intensional, type theory, one may interpret what the 
above means in this context to obtain, within a classical (or 
at least impredicative) metatheory, a notion of category 
meeting your requirements. In fact such non-standard 
categories may be seen as special kinds of tricategory (in 
the usual sense).

Indeed, in the set-based model of type theory, a setoid is 
given by a set X; for each pair of elements x,y in X, a 
further set X(x,y); and arrows of composition X(y,z) x 
X(x,y)-->X(x,z), inverse X(x,y)-->X(y,x) and identity 
1-->X(x,x) subject to no axioms. But this is precisely to 
give a bigroupoid which is locally chaotic, in the sense that 
between any two parallel 1-cells, there is a unique 2-cell. 
[From a constructive perspective, not every such bigroupoid 
would be "OK". The constructively valid ones would be the 
cofibrant ones, since these may be inductively generated.]

From this it follows without difficulty that a category in 
the constructive sense is precisely a tricategory (in the 
sense of Gordon-Power-Street) whose every hom-bicategory is a 
locally chaotic bigroupoid.

The use of these non-standard categories is pertinent with 
regard to Bill Lawvere's comments on the distinction between 
presentations and the things (theories) that they present. 
There is a model structure on the category FPCat of small 
categories with chosen finite products and strict 
product-preserving maps whose cofibrant objects are, up to 
retracts, the (many-sorted) Lawvere theories. One may define, 
in a similar way, a category FPCat' whose objects are 
non-standard categories with finite products, and whose 
morphisms are strict structure-preserving maps: and on this 
there is a model structure (or at least the 
cofibration-trivial fibration half of a model structure) 
whose cofibrant objects are "equational presentations of 
Lawvere theories": one has not only the sorts, and the 
generating operations, but also the generating equalities 
between composite operations. There is an adjunction between 
FPCat and FPCat' which is the left-hand of the two 
adjunctions described by Bill.

Richard



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

Re: A challenge to all

[Steve Vickers]

Dear Andre,

How would you deal with composition?

The standard account of composability - defined by equality between a
domain and a codomain - does seem to presuppose a notion of object equality.

Normally for categories internal in C one therefore takes C to have
pullbacks. Are there obvious ways to generalize that to monoidal C?

Or are you thinking you might want to relax that standard account,
perhaps even losing the well defined domain and codomain? I'm getting a
picture of things like "categories" of smooth curves, where two curves
are composable only if the end of one has an open overlap with the start
of the other. But then "objects" are more nebulous.

Regards,

Steve Vickers.

Joyal wrote:
> ...
> I cannot imagine a category without an equality relation between the objects.
> ...
>
> I would like to propose a test for verifying if the
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on a set S is
> defined by the diagonal map S-->S times S.
> The diagonal gives a set the structure of a cocommutative coalgebra,
> where the tensor product is the cartesian product.
> The objects of a general symmetric monoidal category have no
> coalgebra structure in general.
>
> The test: Is it possible to define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?


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

A challenge to all

[Joyal, André]

Dear All,

I cannot imagine a category without an equality relation between the objects of this category.
Ok, I may have been brainwashed by my training in mathematics at an early age.
But more seriously, I think that the equality relation is inseparable 
from the idea of a set. I do not understand what a preset is:

http://ncatlab.org/nlab/show/preset

Two things are equal if they are the same, if they coincide (whatever that mean!).
Without this notion, an element of a set has no identity, no individuality.
Of course, a set is often constructed from other sets, 
as in arithmetic with congruence classes. 
I am fully aware that the equality relation between the objects of a 
category is not preserved by equivalences in general.
But the art of category theory consists partly in knowing
which construction on the objects and arrows of
a category is invariant under equivalences. 

I would like to propose a test for verifying if the 
notion of category can be freed from the equality relation
on its set of objects. The equality relation on an ordinary 
set S is defined by the diagonal S-->S times S.
The objects of a symmetric monoidal category have no diagonal in general,
ie no coalgebra structure.

The test: Can we define a notion of category internal to
a symmetric monoidal category without using a coalgebra structure
on the object of objects?


Best, André 



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

Re: A challenge to all

[David Roberts]

Dear Andre,

> The test: Can we define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?

the quickest reference I can find is the very incomplete page

http://ncatlab.org/nlab/show/internal+category+in+a+monoidal+category

but more importantly, the thesis referenced there. As I remark at the
above page, Ross Street would know something about this.

As to the other idea, someone (Toby Bartels perhaps) once said that
explicitly equipping 'sets' with a notion of when elements are equal
goes back to Cantor. I find thinking of the undergraduate (or high
school) definition of equality of functions |R --> |R as a pale shadow
of the idea of preset. Consider the collection of expressions denoting
functions (even restricting to polynomials), this is a preset with the
equality relation given by when one algebraic expression gives the
same function as another algebraic expression.

Best,

David Roberts

2010/1/13 Joyal, André <joyal.andre@uqam.ca>:
> Dear All,
>
> I cannot imagine a category without an equality relation between the objects of this category.
> Ok, I may have been brainwashed by my training in mathematics at an early age.
> But more seriously, I think that the equality relation is inseparable
> from the idea of a set. I do not understand what a preset is:
>
> http://ncatlab.org/nlab/show/preset
>
> Two things are equal if they are the same, if they coincide (whatever that mean!).
> Without this notion, an element of a set has no identity, no individuality.
> Of course, a set is often constructed from other sets,
> as in arithmetic with congruence classes.
> I am fully aware that the equality relation between the objects of a
> category is not preserved by equivalences in general.
> But the art of category theory consists partly in knowing
> which construction on the objects and arrows of
> a category is invariant under equivalences.
>
> I would like to propose a test for verifying if the
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on an ordinary
> set S is defined by the diagonal S-->S times S.
> The objects of a symmetric monoidal category have no diagonal in general,
> ie no coalgebra structure.
>
> The test: Can we define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?
>
>
> Best, André
>

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

Re: A challenge to all

[burroni]

Dear André,

> The test: Can we define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?

This is possible with this conception :
A "monoid" in a monoidal category is what Benabou call *monad* in his  
paper on bicatégories. The more general notion of "category", in the  
same vein, is the notion of *polyad* (in the same paper of Benabou ---  
apologize me : I have not the reference whith me): the objets are  
given externally.

I don't know if my remark you satisfie, I think not (you have had  
certainly yourself this idea), but, for me, the moral of this fact  
seems to say that the equality of objets have something of  
intrinsically very different of morphisms.
(This meets perhaps the ideas of Bob Paré on index categories)

I am convided of this (If I have the occasion, I will explain this).
Best,
Albert

"Joyal, André" <joyal.andre@uqam.ca> a écrit :

> Dear All,
>
> I cannot imagine a category without an equality relation between the  
>  objects of this category.
> Ok, I may have been brainwashed by my training in mathematics at an   
> early age.
> But more seriously, I think that the equality relation is inseparable
> from the idea of a set. I do not understand what a preset is:
>
> http://ncatlab.org/nlab/show/preset
>
> Two things are equal if they are the same, if they coincide   
> (whatever that mean!).
> Without this notion, an element of a set has no identity, no individuality.

...

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

Re: A challenge to all

[Jeff Egger]

Dear André,

I do not understand the point of your "test".  

What Bob Paré said, and which I agree with, is that equality 
is "okay" for small categories.  And as Paul Taylor wrote, 
by "small" what one really means is "internal".  

So, of course, it makes sense that V-internal categories 
(where V is a not-necessarily-braided monoidal category with 
distributive coreflexive equalisers) should have a comonoid 
of objects.  

But this in no way contradicts the assertion that _large_ 
categories should not have an equality relation between 
objects---internal categories are tautologously small!  

Not being as familiar with indexed categories/fibrations as
I ought to be, I tend to think of large categories in terms 
of enriched category theory.  Here, we see very clearly that 
the collection of objects has nothing whatsoever to do with 
the enriching category V, and this is as it should be.

In fact, I suppose that it probably would make sense to 
generalise enriched categories by taking a (large) groupoid 
of objects (and _canonical_ isos, in the spirit of Paré and 
Schumacher) instead of a mere class.  I don't know if this 
has ever been done.  

My main point is that you are right in asserting that a set 
without an equality relation is not a set.  But the exact 
meaning of large category is one whose objects do not 
necessarily form a set!  

Morally speaking, "set" does mean "collection that has an 
equality predicate", but this leaves open the possibility 
that there are collections which do not have such a 
predicate, and which are therefore not sets.  These suffice 
for the purpose of large category theory---for example, they 
suffice for the purpose of enriched categories; moreover, 
FOLDS is explicitly based on these principles. 

Cheers,
Jeff.

----- Original Message ----
> From: "Joyal, André" <joyal.andre@uqam.ca>
> To: categories@mta.ca
> Sent: Tue, January 12, 2010 4:24:39 PM
> Subject: categories: A challenge to all
> 
> Dear All,
> 
> I cannot imagine a category without an equality relation between the objects of 
> this category.
> Ok, I may have been brainwashed by my training in mathematics at an early age.
> But more seriously, I think that the equality relation is inseparable 
> from the idea of a set. I do not understand what a preset is:
> 
> http://ncatlab.org/nlab/show/preset
> 
> Two things are equal if they are the same, if they coincide (whatever that 
> mean!).
> Without this notion, an element of a set has no identity, no individuality.
> Of course, a set is often constructed from other sets, 
> as in arithmetic with congruence classes. 
> I am fully aware that the equality relation between the objects of a 
> category is not preserved by equivalences in general.
> But the art of category theory consists partly in knowing
> which construction on the objects and arrows of
> a category is invariant under equivalences. 
> 
> I would like to propose a test for verifying if the 
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on an ordinary 
> set S is defined by the diagonal S-->S times S.
> The objects of a symmetric monoidal category have no diagonal in general,
> ie no coalgebra structure.
> 
> The test: Can we define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?
> 
> 
> Best, André 
> 
> 
> 
>

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

Re: A challenge to all

[Michael Shulman]

Dear Andre,

You are absolutely right that the equality relation is inseparable from
the idea of a set.  What is being proposed, however, is that a category
doesn't need to have a *set* of objects.  In fact, the objects of a
category don't need to form an object of any category at all, so I think
your proposed test is misguided.  The formulation of category theory in
dependent type theory which Richard, Toby, I, and others are proposing
makes perfect sense without any equality predicate for the objects.

Best,
Mike

Joyal wrote:
> Dear All,
> 
> I cannot imagine a category without an equality relation between the objects of this category.
> Ok, I may have been brainwashed by my training in mathematics at an early age.
> But more seriously, I think that the equality relation is inseparable 
> from the idea of a set. I do not understand what a preset is:
> 
> http://ncatlab.org/nlab/show/preset
> 
> Two things are equal if they are the same, if they coincide (whatever that mean!).
> Without this notion, an element of a set has no identity, no individuality.
> Of course, a set is often constructed from other sets, 
> as in arithmetic with congruence classes. 
> I am fully aware that the equality relation between the objects of a 
> category is not preserved by equivalences in general.
> But the art of category theory consists partly in knowing
> which construction on the objects and arrows of
> a category is invariant under equivalences. 
> 
> I would like to propose a test for verifying if the 
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on an ordinary 
> set S is defined by the diagonal S-->S times S.
> The objects of a symmetric monoidal category have no diagonal in general,
> ie no coalgebra structure.
> 
> The test: Can we define a notion of category internal to
> a symmetric monoidal category without using a coalgebra structure
> on the object of objects?
> 
> 
> Best, André 

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

Re: equality is beautiful

[lamarche]

I have been thinking on how to get this post right for a few days,  
taking my time, but André's recent post

> Can we define a notion of (large) category without supposing
> that its (large) set of objects has a diagonal?


prompted me to send this... perhaps prematurely.

One can do a lot of mathematics without using the equality predicate.  
The necessary technology  (dependent types) has been around for a long  
time, and the foundations of category theory is a natural domain of  
application for it. Richard Gardner has already said something to that  
effect, but I want to stress that point and try to sell it to the less  
syntactically inclined among us.

In dependent types you still need a very limited form of equality, to  
be able to compare syntactic objects. After all, if you make a complex  
syntactic construction A, you have to be able to make copies of it and  
reuse it elsewhere at several places, and you want your theory to take  
account of this. And, more importantly, if you start with A and  
elaborate on it twice, getting two syntactic objects  S(A), T(A), it  
is natural to be able to assert that the two results are equal,  
because some times they will. The standard example of this is beta- 
reduction in the lambda calculus.

But as I said this is a very limited form of equality, since a true  
equality predicate would allow you to assert if two *arbitrary*  
objects are equal.

The syntax of dependent types is rather heavy, but once you know how  
to interpret it in a category C it is very intuitive. To get started  
all you need is a class of maps in C which is stable under pullbacks.  
and then you interpret such a special map

A:  \bar A ---->  X

as a dependent type   x: X  |-  A(x)

I.e., if types in say, simple lamda calculus can be interpreted as  
sets (or spaces), then dependent types can be interpreted as an  
indexed family of sets, depending on another set. The operation of  
pullback is substitution of a term in a type.

That is, if an aribtrary map    B  ---->  A  in C  is thought of as a  
term, in the usual Lawvere-Lambek sense

b:B  |-  f(b)

then the pullbakck of A by f represents the type

b:B |-  A(f(b))

Most of the people on this list are already very familiar with this  
*intuition*, which has been used countless times since the mid-fifties  
starting in algebraic topology, then algebraic geometry, then  
categorical foundations (I mention in particular the idea of using  
such a class of pullback-stable maps in a topos-like category as a  
notion of smallness,  introduced (i think) by Bénabou and used  
extensively by Joyal-Moerdijk in a monograph, and lots of other people  
who are reading this list.

But the point of this post is that I think there is still the need to  
stress that there is a *formal syntax* which corresponds to this  
intuition, although many people on this list are already aware of  
this. We have learned to "reason intuititionisticallty" in a topos,  
and intuitionistic predicate theory was a real help in doing so... the  
same goes here: we can learn to reason in situations where the  
equality predicate is limited to special types, the *discrete* ones.   
And this point it is easy to illustrate.

Let us go back to our category C. People have known for a long time  
that all you need to do to define internal categories in C is to  
require that C have pullbacks. But actually the natural requirements  
are even weaker:  all you need is that C have a special class of maps  
closed under pullbacks (and that includes all isos). For simplicity  
today I will also require a terminal object. As I already said you  
think of these maps as indexed families. So suppose X is chosen to be  
the object of objects of an internal category.  You want a family of  
morphisms. I.e., given the usual span

d_0 :  X <-----  H  ----->  X  d_1

it is now required that  X ---> 1 be one of these special maps (so  
that "X is an independent type") and both  H ----> X are required to  
be special maps too. It is easy to see then that  <d_0, d_1> :  H ----- 
 >  X x X   is also a special map. We can now say that these two maps  
define an indexed family:

x: X,  y: X  |-  Hom(x,y)

Now look at how composition is presented:

x,y,z : X ,  h:  Hom(x,y), k: Hom(y,z)  |-  k o h  :  Hom(x,z)

This is intepreted in C via very mechanical constructions, which will  
give the interpretation of composition as the usual map, with the  
usual pullback as source and which obeys the usual commutation  
requirements. Notice that the syntax we used *does not need an  
equality predicate to assert that dom(k) = cod(h)*

The same goes with the identity map

x: X  |-  Id(x) : Hom(x,x)

But now look at associativity:

x,y,z,w: X, h: Hom(x,y), k: Hom(y,z), g: Hom(z,w)  |-   g o (k o h) =   
(g o k ) o h

Here you need a real equality predicate. That means that the sets in  
the indexed family (Hom(x,y))_x,y   are required to be *discrete  
sets*, i.e., that the diagonal is required to be a predicate. There is  
some leeway on how to define predicates, but a natural way to do it is  
to say that predicates are (represented by) special maps that are monos.

Thus, to be back to the "small is beautiful" track, a first  
approximation of Large/Small goes (very roughly)  space/discrete space.

Several years ago i circulated a manuscript where I was trying to  
formalize foundations of category theory by specializing the space/ 
discrete space duality above to groupoid/discrete groupoid. I was  
using fibrations of groupoids over a base category (potentially a  
topos) as a reference model. In other words, I was trying to find the  
kind of elementary toposes you would get if you subsituted fibrations  
(and stacks) of groupoids for presheaves (and sheaves). I made some  
very interesting observations, but one problem I hit was that these  
categories are only bi-cartesian closed, not cartesian closed, and  
that really stretched the available syntactic technology. It seems  
that you can't avoid going in higher dimension whenever you tackle  
such issues. I was using groupoid-enriched categories as the basic  
language of my axiomatization. In other words, a class comes  
*indissociably equipped* with a notion of isomorphism between its  
objects, and only discrete classes have the true equality predicate.  
The point is that the classes that you first meet in real life are  
classes of sets-with-structure, and that *if you have properly defined  
a structure, you should know what the isomorphisms are*. Moreover,  
whatever you do to a mathematical object, you should be able to  
transport along an isomorphism. Naturally I got the idea from André's  
theory of combinatorial species. This is perfectly in accordance with  
dependent type theory: you don't have to know when two structures are  
equal; what really matters is having an iso between them, because then  
they are interchangeable. So I was working on the principle that all  
the constructions usually done on sets should be lifted to groupoids,  
which then always allow you to use transport on whatever you've  
constructed. But another problem I hit was that the powerset  
construction is very much weakened, because given a groupoid X, the  
only natural notion of PX is the (discrete) class of all subgroupoids  
that are isomorphism-closed ("replete"). This weakens the logic very  
much and you cannot use higher-order logic to do things like  
constructing sums, as in elementary toposes. But you sitll can  
interpret a form of predicate logic in there. Naturally a predicate in  
general is interpreted as a replete subobject, which is quite natural.  
A property only makes sense only if it is invariant under iso. The use  
of subobjects as predicates show that his approach is more aligned  
with Church-style intuitionism than Martin-Löf-style constructive  
foundations.

One of these interesting observation that I made is that there is a  
special version of the axiom of choice in that context, which is  
perfectly suited for category theory, but does not clash with  
constructivism. And it is valid in fibrations and stacks. Presented in  
ordinary categorical language, it goes: given a class/groupoid G and a  
family of classes that depend on it (a fibration of groupoids  over G  
in the ordinary sense) such that every class/fiber of the family is  
inhabited (which is surjective as a fibration) and such that all  
theses fibers are *equivalent to discrete sets* (in other words such  
that hom-sets are never bigger than singletons, Bénabou has a name for  
these) then the fibration has a splitting. This is the axiom of choice  
that categorists use all the time:  universal constructions give rise  
to exactly such fibrations---existence up to uniqueisomorphism---and  
they are the cases when the axiom of choice is needed.

Richard mentions some foundational work that I was not aware of, where  
the higher-order categories go all the way up to tri. It seems that  
this particular case of dimension-climbing is a formal consequence of  
the base axiomatics, while mine came from semantics. But I think we  
should seize the bull by the horns and base foundations on higher- 
dimension groupoids (i know that other people on this list agree, and  
I should mention Makkai's opetopes). Because naturally after you've  
consider classes of sets-with structure, you cannot avoid getting  
(meta?)classes of classes-with-structure, where isomorphism has become  
equivalence, und so weiter.

To go back to André's original question:  you can build foundational  
universes whose inhabitants are groupoids and ordinary not sets/ 
classes in general. The diagonal in these will exist *but it will not  
be a predicate*.

Hope this isn't too ponderous,

François









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

Re: equality

[Dusko Pavlovic]

hi.

several people suggest dependent type theory as a foundation to
formalize categories. maybe it is worth mentioning that per martin-
loef (the originatory of dependent types) worked this out, prolly in
the 70s. that was one of his early examples. many people who
implemented basic category theory in the 80s (burstall-rydeheard,
NuPRL team etc) followed this design. i am sure that there are people
on the list who know much more about this than i do.

while martin-loef's construction is quite natural and easy to
reconstruct, one idea that still seems to be missing here, and leads
to some confusion: the distinction between the extensional equality,
ie term conversion, and the intentional equality, ie equality types.

without going into any details, let me suggest that this formalization
may clarify some confusion.

in martin loef's formalization, the composition operation does not
involve equality: no equality expressions occur in the expression
Hom(A,B) # Hom(B,C) ---> Hom(A,C). what does occur are two copies of
B. but ***being able to copy B is not the same thing as being able to
decide the equality predicate***. mapping things along the diagonal is
not the same thing as being able to decide whether something lies in
the image or not.

in practice, if i give you an object (say a group B) you will have no
problem to make two identical copies of that group, in whichever form
it may be given. but if i give you two big complicated groups, and you
want to know whether they are equal on the nose, then you need to see
how they are represented. in other words, you need to open the black
boxes, and see what exactly are the elements of these groups etc. and
this is not very categorical. as we all know, the whole point of eg
the universal properties is that you describe things without opening
any black boxes.

one more thing, also apparent from any formalization: the reason why
the object equality is no problem for small (internal) categories is
that their objects can be viewed as arrows of the base category (and
the arrows are, of course, in the business of being equal or not).

-- dusko


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

Re: equality is beautiful

[Michael Shulman]

This whole discussion has been very instructive to me, especially by
showing that the same fundamental ideas have occurred to many people
over and over again, but seemingly never quite made it out into the
general mathematical consciousness.  (Either that, or else I've
completely missed them.)

lamarche wrote:
> Several years ago i circulated a manuscript where I was trying to
> formalize foundations of category theory by specializing the
> space/discrete space duality above to groupoid/discrete groupoid. I was
> using fibrations of groupoids over a base category (potentially a topos)
> as a reference model. In other words, I was trying to find the kind of
> elementary toposes you would get if you subsituted fibrations (and
> stacks) of groupoids for presheaves (and sheaves). I made some very
> interesting observations, but one problem I hit was that these
> categories are only bi-cartesian closed, not cartesian closed, and that
> really stretched the available syntactic technology.

I would be interested in seeing this manuscript, because it sounds like
exactly the same direction that some people have recently been trying to
work on "higher-dimensional type theory" and 2-topos theory.  For
instance, Richard Garner's paper on "two-dimensional type theory"
(http://www.dpmms.cam.ac.uk/~rhgg2/2-LCCC/2-LCCC.html) sounds almost
exactly like the type theory you are describing, with categories for
which Hom(x,y) is a "discrete set", i.e. has a diagonal that "is a
predicate" (i.e. is "extensional").  He also deals with an
"intermediately weak" form of cartesian closure for 2-categories.

A number of people have also recently been thinking about 2-dimensional
analogues of elementary toposes.  On the one hand, there is Mark Weber's
work on "2-toposes" which of course uses "strict" cartesian closure.  I
have been thinking from a different direction, starting from Street's
characterization of "Grothendieck 2-toposes" with Giraud-like exactness
axioms, using those exactness axioms to describe an internal logic/type
theory for a "2-pretopos" which contains "hom-objects" that are
"discrete"---whereas not every object is discrete.  (A very preliminary
version of this can be found here:
http://ncatlab.org/michaelshulman/show/2-categorical+logic .)  It
generally seems to me that most "first-order" properties of elementary
toposes generalize quite well, whereas those that use power objects are
touchier.

> One of these interesting observation that I made is that there is a
> special version of the axiom of choice in that context, which is
> perfectly suited for category theory, but does not clash with
> constructivism. And it is valid in fibrations and stacks. Presented in
> ordinary categorical language, it goes: given a class/groupoid G and a
> family of classes that depend on it (a fibration of groupoids  over G in
> the ordinary sense) such that every class/fiber of the family is
> inhabited (which is surjective as a fibration) and such that all theses
> fibers are *equivalent to discrete sets* (in other words such that
> hom-sets are never bigger than singletons, Bénabou has a name for these)
> then the fibration has a splitting. This is the axiom of choice that
> categorists use all the time:  universal constructions give rise to
> exactly such fibrations---existence up to uniqueisomorphism---and they
> are the cases when the axiom of choice is needed.

I agree entirely.  In fact, I would argue that this is not really a
version of the axiom of choice at all, but rather a principle of
*functor comprehension*.  In ordinary set theory, the axiom of choice is
not necessary in order to make choices that are uniquely determined.
This is sometimes called the "axiom of unique choice" or "axiom of
non-choice" or the "function comprehension principle."  In categorical
language, it corresponds to the fact that any morphism which is both
monic and strong epic must be an isomorphism (in a pretopos, of course
every epic is strong).  This makes the most sense to think about in a
regular category, which has stable (strong epi, mono) factorizations,
and the function comprehension principle is true in the internal logic
of any such category.

Likewise, in category theory, the axiom of choice "should" not be
necessary in order to make choices that are uniquely determined up to
unique specified isomorphism.  The fact that an axiom of choice *is*
required for such "choices" in standard set-theoretic foundations of
category theory I would regard as merely a defect of those foundations.
 (This defect can, however, be worked around by using "anafunctors"
instead of ordinary functors.)

Another way of stating the "functor comprehension principle" is that any
fully faithful functor (between groupoids, or even between categories)
which is surjective on objects must have a section, or equivalently that
any functor which is fully faithful and essentially surjective must be a
(strong) equivalence.  In 2-categorical language, this corresponds again
to saying that any map which is both "monic" and "strong epic" must be
an equivalence.  Here we define a morphism in a 2-category (or
bicategory) to be "monic" if it is "fully faithful" in the representable
sense (perhaps this should be called "1-monic" for disambiguation with
morphisms that are merely "faithful"), and "strong epic" (or "strong
1-epic") if it is left orthogonal to monics (in the bicategorical
sense).  In Cat, the monics are the fully faithful functors, and the
strong epics are those that are essentially surjective on objects.

In his paper "A characterization of bicategories of stacks," Street
observed that Cat is a regular 2-category, i.e. it has good stable
(strong epi, mono) factorizations.  The functor comprehension principle
is of course true, for the same tautologous reasons, in the "internal
logic" of any regular 2-category, suitably defined.  However, the fact
that Cat is a regular 2-category (and in fact, the characterization of
strong epics in Cat as e.s.o. functors) depends on the axiom of choice.
 But surely AC "should" not be necessary for Cat to be a regular
2-category, just as AC is not necessary for Set to be a regular
category.  This can be remedied with anafunctors: the bicategory of
categories and anafunctors is always regular, whether or not we assume
AC.  Alternately, however, we could assume in our foundational axioms
"Cat is a regular 2-category" or better a "2-topos," instead of a
set-theoretic axiom system about Set, and get the functor comprehension
principle automatically (and without implying any form of AC).

Best,
Mike


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

Re: A challenge to all

[Peter LeFanu Lumsdaine]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1861 bytes --]

On 12 Jan 2010, at 11:24, André Joyal wrote:
> 
> I would like to propose a test for verifying if the 
> notion of category can be freed from the equality relation
> on its set of objects. The equality relation on an ordinary 
> set S is defined by the diagonal S-->S times S.

Your test is addressed in more detail in other replies, but to pull out one idea that comes up in several:

--- the diagonal embedding is not always the equality relation.

I don't think I've seen anyone propose how to define a notion of category in the absence of some kind of diagonal embedding, but Francois Larmarche and others nicely describe various situations (topological spaces, higher categories, intensional type theories...) where the diagonal embedding isn't a well-behaved equality relation, and certainly isn't the one we want.

For example, one such situation is explored by Gambino and Garner in "The identity type weak factorisation system".  Roughly: you can have logical categories where a predicate S ---> A on an object means not a monic, but rather a _fibration_, for some wfs (or similar structure).  The diagonal embedding A >--> AxA may fail to be a fibration; then the equality predicate E comes from the factorisation of this map as a left map (think "cofibrant weak equivalence") followed by a fibration:

A >--> E ---> AxA.

The groupoid case is a nice example of this situation, as described in that paper.

So the notions of "diagonal embedding" and "equality relation" can certainly diverge (even in situations where both exist); and I think the insight of Mike Shulman and co. here is that "diagonal embedding" is the one which (if either) is wanted in the definition of a category.

-p.


-- 
Peter LeFanu Lumsdaine
Carnegie Mellon University



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

Re: equality

[Colin McLarty]

2010/1/13 Dusko Pavlovic <dusko@kestrel.edu>:
> hi.
>
> several people suggest dependent type theory as a foundation to
> formalize categories. maybe it is worth mentioning that per martin-
> loef (the originatory of dependent types) worked this out, prolly in
> the 70s.

Is there a published account of this, preferably on the web?


Colin


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

Re: A challenge to all

[Joyal, André]

Dear All, 

Many people have expressed their view on the problem posed
by the equality relation.
I warmly thank everyone for that.
I would like to make some general observations.
I apologise for not answering individually.
First, I have a litte story to tell.

[A tale of giants, small and large.

I remember when I first encountered the big sets obtained 
from the set of natural numbers by iterating the power set 
operation a finite number of times.
I was scared and amazed by their size but I was reassured
by my teacher who told me they were good.
I often thought about them because I was studying real numbers 
and analysis. We eventually became close friends and I was happy to 
accept the whole family in my mathematical house.
But once living in my house, they received the visit of their relatives,
first the brothers, then the cousins, and later some higher degree cousins.
The relatives were bigger, stokier, but they were all very kind.
I had no objection in making them a place in my house if they wanted to live with me.
But eventually, the relatives were arriving endlessy and
I began to worry that my house may collapse. 
I could not find a fair rule to bar the newcomers from my house.
I was apparently losing control. 
This is why I felt some relief when I learned from a high priest 
that my home giants were actually dwarfs compared to a race of mega-giants, 
the larges. The giants were so much bigger than me and bigger than
anything I could see directly. But the priest, a distant relative of Bertrand Russel,  
also told me that I should be very wary of the mega-giants, because

"the equality relation may not be well defined on a large set".  

The truth is that I could not perceive a real difference between the large giants
and the biggests among the small giants. There was only a vague difference of scale, 
not really of shape. After taking some vacation in which I did some meditation, 
I decided to be fair with all creatures, small and large, 
and behave as if they were all good. I ignored the advice 
of the priest and welcomed the large giants in my house.
My house did not collapse and I am enjoying mathematics even more.]

The notion of equality is raising a lot of questions, 
running from the theory of classes to constructive mathematics, 
from categorical logic to higher category theory and homotopy theory.
It has also ramifications in philosophy.
I will only discuss a limited numbers of aspects.

The main character in the arena of constructive mathematics
is represented by Martin-Lof intensional types theory.
Let me give a few references, since category theorists 
are not always familiar with type theory:

http://en.wikipedia.org/wiki/Intuitionistic_type_theory

[B. Nordstöm, K. Petersson, and J. M. Smith 
Martin-Löf ’s Type Theory 
Handbook of Logic in Computer Science, Vol. 5 
Oxford University Press, 2001] 


For an introduction to dependant type theory, see

http://www.math.unipa.it/~ngambino/dtt.html

A salient feature of the system is the formation rule
which associates to two terms a and b of type A 
another type Id_A(a,b). A term c of type Id_A(a,b) is
a proof of the equality a=b. It can also
be interpreted as an isomorphism c:a-->b. 
A semantic using isomorphisms and groupoids 
was proposed by Curien in 1993 and constructed by 
Hoffman and Streicher in 1994:

[Hofmann, M. and Streicher, T. (1994) 
A groupoid model refutes uniqueness of identity proofs. 
Proceedings of the 9th Symposium on Logic in Computer Science 
(LICS), Paris, France] 
 
A semantic based on paths and spaces was later proposed by
Steve Awodey and Michael Warren in 2007:

http://arxiv.org/abs/0709.0248

A semantic based on weak omega-groupoids was proposed
by Beno van den Berg and Richard Garner in 2008,
and also by Lumsdaine:

http://arxiv.org/abs/0812.0298
http://arxiv.org/abs/0812.0409

In these models, a dependant type type A(x), 
with x a variable of type B, is interpreted 
as a fibration A(x)--->B.
Nicola Gambino and Richard Garner have introduced
a notion of fibration in the classifying category 
of type theory:

http://arxiv.org/abs/0803.4349

These developements illustrate the fact that there is a tantalising 
connection between type theory, higher category theory and homotopy theory
(see the paper of Awodey and Warren above). 
Classical first order intuitionistic logic has a natural
semantic in toposes. It is natural to conjecture that 
intensional type theory has a natural semantic in infty-toposes.
One problem is that an infty-topos is not an ordinary category,
it is an (infty,1)-category. There are many *brands*
of (infty,1)-categories and they are all equivalent:

http://arxiv.org/abs/math/0610239
http://arxiv.org/abs/math/0504334
http://arxiv.org/abs/math/0607820

It is not clear which *brand* of (infty,1)-categories
is best for the semantic of type theory.
At first, the simplicial category *brand* appears to 
be the simplest because a simplicial category is just
a category enriched over simplicial sets.
But homotopy theoretic constructions in simplicial categories 
are notoriously complex. For example, 
we have to use homotopy coherent diagrams
instead of plain commutative diagrams,

http://www.ams.org/tran/1997-349-01/S0002-9947-97-01752-2/home.html

The corresponding constructions in quasi-categories are much simpler.
This is why Jacob Lurie is using quasi-categories instead
of simplicial categories (his thesis on infinity-toposes
was originally written with categories enriched over spaces).

http://arxiv.org/abs/math/0610239

This leads to the general problem of representing
(infty,1)-categories by various kind of categorical structures.
One can use *homotopical categories* for that

http://www.ams.org/bookpages/surv-113/

A homotopical category is a category C 
equipped with a class W of "weak equivalences".
Every homotopical category (C,W) has a *quasi-localisation* C[W(-1)]
which is a quasi-category. The simplicial set C[W(-1)] is 
obtained from the nerve of C by freely gluing a homotopy inverse to 
each arrow in W, and then, by adding simplicies to turn it into 
a quasi-category (this last step is called a fibrant completion).
The quasi-category C[W(-1)] is equivalent to the Dwyer-Kan localisation 
of C with respect to W, via the equivalence between quasi-categories
and simplicial categories,

http://arxiv.org/abs/0910.0814
http://arxiv.org/abs/0911.0469

Conversely, every quasi-category is equivalent to
the quasi-localisation of a homotopical category.
This gives a representation of all (infty,1)-categories
in terms of homotopical categories.
It follows that many aspects of the theory of (infty,1)-categories
can be expressed in terms of category theory.

When the homotopical category (C,W) is obtained from a Quillen 
model structure (by forgetting the cofibrations and the fibrations)
the quasi-category C[W^(-1)] has finite limits and colimits.
Conversely, I conjecture that every quasi-category
with finite limits and colimits is equivalent to the quasi-localisation
of a model category. In fact, every locally presentable quasi-category 
is a quasi-localisation of a combinatorial model by a result of Lurie.
More can be said: the underlying category can taken to be
a category of presheaves by a result of Daniel Dugger.

http://arxiv.org/abs/math/0007070

Denis-Charles Cisinski has studied the model structures 
on a Grothendieck toposes in which the cofibrations are the monomorphisms. 

[Théorie Homotopique dans les topos, JPAA, Vol 174 (2002), pp 43-82]

It should be very interesting to know which combinatorial model structures 
on a Grothendick topos are giving rise to infty-toposes after quasi-localisation.
These "model topos" could possibly serve as a semantic for intensional type theory.  

This leads to the more general problem of "modelling" higher categories.
All higher categories can be represented as fibrant objects in
a model category. Charles Rezk has recently proposed a model structure
for n-quasi-category:

http://arxiv.org/abs/0901.3602

Finally, let me return to the equality problem.
I agree that the meaning of the equality relation 
between the objects of a large category is unclear.
The is because the set theoretic incarnation or representation 
of a mathematical structure depends on arbitrary choices. 
For example, the real euclidian space could be construct as 

(R times R) times R

or as  

R times (R times R).

where R is the real line.
They are different sets, but as far as geometry goes, it does not matter.
I like to use it in a course for an example of a monoidal category which is not strict.
Not every monoidal category is strict, since the the category of sets is not!
I am reluctant to accept the notion of preset, a set
without an equality, because I do not understand what it means.
I am also reluctant to base category theory on type theory because
constructive mathematics tends to be much more complicated than 
ordinary mathematics. I doubt that constructive mathematics will be adopted 
by the mathematical community any time soon, probably not before 
the collapse of human civilisation due to climate warming! 
(I hope it will not collapse, but we should be wary).
But type theory could become important in computer science in the short term:

[B. Nordström, K. Petersson, and J. M. Smith 
Programming in Martin-Löf ’s Type Theory 
Oxford University Press, 1990] 

Classical set theory is our best friend. It should not be throwned 
away because of philosophical doubts about the equality relation. 
It should be used (and perfected) until we have a better alternative
or until it breaks. The theory of sets is axiomatic and we 
may choose the axioms quite freely for their simplicity, beauty and 
practical values. This is why I am ready to use large sets whenever 
possible when they seem useful.  

Category theory based on classical set theory works very well. 
The category of large sets is a pretopos equipped with a notion 
of small maps (algebraic set theory).
It has many other properties that should be investigated.
For example, I suspect that its category of internal categories 
has a natural Quillen model structure.
I conjecture that this is true also for many other
categories of internal structures.
For example, there should be a model structure 
for internal n-quasi-categories for any n.

I believe that the encoding of higher category theory 
in terms of ordinary category theory and set theory is not artificial.
It depends on deep mathematical structures and ideas.
It is using Quillen model structures and combinatorics.
 
Many people have suggested using indexed categories
and stacks to handle large categories.
The notion of stack is extending that of sheaf.
The category of all sheaves on a site is a Grothendieck topos
and the category of all stacks may be called a Grothendieck cosmoi 
(I apologise to Ross Street for perverting his terminology). 
The quasi-category of Rezk categories internal to a 1-topos 
is an another example of cosmoi, but not every cosmoi 
is of this form. The theory of cosmoi can be developed by 
using model structures.


Best, 
André


PS: My "challenge to all" was met with a deafening silence as far as
producing a counter-example is concerned. 

Ross Street and Brian Day have a notion of quantum category,
but as Ross pointed out, its object of objects has a coalgebra structure.

[Quantum categories, star autonomy, and quantum groupoids, in 
"Galois Theory, Hopf Algebras, and Semiabelian Categories", 
Fields Institute Communications 43 (American Math. Soc. 2004) 187-226]

Ross wrote: 

> Take V to be the monoidal category of vector spaces (say). 
> Write Comod(V) for the monoidal bicategory whose objects are 
> comonoids C in V and whose morphisms C --> D are left C-, right D-comodules; 
> composition of these morphisms involves an equalizer. 
> Actually Comod(V) is an autonomous monoidal bicategory with the dual 
> C^o of C obtained by following the diagonal by a switch 
> (symmetry or braiding would do for more general V). 
> Notice that C^o (tensor) C becomes a pseudomonoid in Comod(V).
> A quantum category in V consists of a comonoid C in V together 
> with a monoidal comonad on C^o(tensor) C.




 



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

Re: A challenge to all

[Thomas Streicher]

It is, of course, not impossible that big categories come with an equality of
objects, e.g. if one works relative to a base category Set which is a model
of ZFC with sufficiently many Grothendieck universes. A very strong such
extension is by the axiom that every set appears as element of some
Grothendieck universe. For most purposes 2 or 3 nested Grothendieck universes
suffice. This may seem strong but is weaker than some of the large cardinal
axioms considered by set theorists.

As I understand big categories without equality show up necessarily when
one works relative to bases much weaker then Set like elementary toposes or
"predicative" versions thereof. The reason is that when fibring the base BB
over itself via the fundamental (or codomain) fibration P_BB : BP^2 -> BB
this fibration is not split. A possibility is to extend BB to the category
Idl(BB) (as done in work on Algebraic Set Theory by Awodey et.al. following
an advice of Joyal) which provides a model for an intuitionistic theory of
classes. One may describe Idl(BB) as the full subcategory of Sh(BB) (sheaves
over BB w.r.t. the finite cover topology) such that equality is definable in
the sense of Benabou.
Of course, not all split fibrations over BB can be obtained as externalisations
of categories internal to Idl(BB). But P_BB is equivalent to such a fibration.
Of course, this approach just mimicks the classical set theoretic approach
which many people dislike.

Type theory was mentioned as a possible alternative because via dependent
types one can formulate the structure of a category in a most natural way.
But if one works in extensional type theory (i.e. "judgemental"  and
"propositional" equality identified) there is also no problem with equality.
Actually extensional type theory with a cumulative sequence of universes is
an attractive alternative for those who dislike a set like approach.

The current official version of type theory is intensional type theory with
a weak "judgemental" equality and a stronger "propositional" equality. The
distinguishing feature of intensional type theory is that type checking is
decidable (which is not the case for extensional type theory). Living with
two equalities doesn't really make one's life easier but it's a price to be
paid for having the nice (and practically most useful) property of decidable
type checking.

But there is a way of turning this defect into an advantage. This was observed
in the mid 90s by Martin Hofmann and myself when we considered the model where
types are groupoids and families of types are (split) fibrations of groupoids.
Of course, the diagonal on a groupoid will be a fibration if and only if the
groupoid is discrete. Therefore, we interpreted the equality on a groupoid A
as the fibration corresponding to Hom_A(-,-), i.e. equality as being isomorphic.
Thus there are different ways of being equal because there are in general
different ways of being isomorphic. (Finding models of type theory where there
are different ways of being propositionally equal was our main concern in this
paper). We also discussed in this paper (Sect.5.4) that one might add axioms
claiming for elements of some universe that being equal is equivalent to being
isomorphic. In Sect.5.5 of this paper we sketched how to exploit such an
extended type theory for formalizing category theory in such a way that
equality of objects is equivalent to them being isomorphic.

There are 2 defects of the groupoid model, namely that it is 2-dimensional
and that it is strong and not weak. In his PhD Thesis Michael Warren has shown
that strict \omega-groupoids do form a model of intensional type theory. In a
talk some time ago (2006) I suggested to model intensional type theory in the
topos SSet of simplicial sets interpreting types as Kan complexes and families
of types as Kan fibrations. Recently, in Nov. 2009 V.Voevodsky gave a talk in
Munich on "Homotopical Lambda Calculus" where he presented such a setting as
a model for type theory where equality can be understood as being isomorphic.
The latter was precisely his motivation for doing it. He said he will write up
this work in the near future.

Thomas








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

Re: A challenge to all

[Michael Shulman]

Just to respond to one aspect of this:

Joyal wrote:
> I am also reluctant to base category theory on type theory because
> constructive mathematics tends to be much more complicated than
> ordinary mathematics.

I can't speak for others, but I did not intend, in making the suggestion
to base category theory without equality for objects on type theory,
that constructive mathematics be necessarily also adopted.  While many
of the adherents of type theory have a constructive point of view, and
type theory is a natural home for constructive mathematics, type theory
with classical logic is also a perfectly well-defined notion.  Its
type-theoretic properties are not as good as those of the constructive
version, but that's irrelevant for the purposes I had in mind: it can be
used as a language just like the ordinary classical first-order logic in
which classical set theories such as ZFC are formulated.

Mike


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

re: the definition of "evil"

[Fred E.J. Linton]

After Mike Shulman's remarks beginning with

> It looks to me like there are (at least) two different ideas of "evil"
> floating around.

I'm tempted to ask: which idea(s) of "evil" does 
the notion of a category's being *skeletal* embody?

And is that *really* "evil" in the everyman's sense of the word?

Cheers, -- Fred




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