Re: A challenge to all

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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