Re: A challenge to all

["Joyal, André" <joyal.andre@uqam.ca>]

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