Re: equality is beautiful

Re: equality is beautiful

[David Leduc]

Dear Richard,

On Mon, Jan 11, 2010 at 11:26 AM, Richard Garner <rhgg2@hermes.cam.ac.uk> wrote:
> 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.

What about the characterization of limits in terms of products and
equalizers? It states that the limit of a functor F:J->C is
constructed by products indexed by the set(oid) of objects and the
set(oid) of arrows of J. But if you don't allow equality on objects in
J, you only have a preset of object, not a set(oid).

David


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

Re: equality is beautiful

[Toby Bartels]

David Leduc wrote:

>What about the characterization of limits in terms of products and
>equalizers? It states that the limit of a functor F:J->C is
>constructed by products indexed by the set(oid) of objects and the
>set(oid) of arrows of J. But if you don't allow equality on objects in
>J, you only have a preset of objects, not a set(oid).

Consider the analogy between small and strict categories.
(A category is strict if it is equipped with a notion of equality of objects.
Logically, this is a structure rather than a property like smallness.)

Often when speaking of small categories, one speaks relative to a universe
which is a collection of set(oid)s or a collection of set(oid) cardinalities,
so every small preset automatically comes equipped with a notion of equality.
In this case, every small category is strict.  Conversely,
every strict category is small relative to some universe,
if you accept an axiom such as Grothendieck's axiom of universes.
So these are very closely related concepts.

As is well known, we are most interested in the limit of F: J -> C for small J.
Less well known, but also true, we are most interested in it when J is strict.
In that case, there is no problem; the arrows of J form a set(oid),
and we can consider products indexed by that set(oid).
In principle, J doesn't have to be strict, any more than it has to be small,
but if you have some reason to believe that the limit exists,
then you can examine that reason to see what product is relevant.
Most of the time, you can just assume that J is small and strict.


--Toby


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

Re: equality is beautiful

[Michael Shulman]

To rephrase what Toby said: the construction of limits via products and
equalizers only works for limits over a domain category which has a
set(oid) of objects (what Toby calls a "strict category"), whether that
set is large or small.  Of course, it also only works when the products
and equalizers exist; a particular limit may exist without the relevant
products and equalizers existing.

It is true that we are most interested in limits over small strict
categories, but there are many limits over large categories that do
exist and are occasionally useful.  For instance, every object X of a
category C is the limit of the identity functor C --> C weighted by the
representable weight hom_C(X,-), whether or not C is small or strict.
Of course, by Freyd's theorem, a large category cannot have large
*products* unless it is a preorder, so one shouldn't expect to be able
to construct such large limits via products and equalizers.  This
matches quite nicely with the type-theoretic philosophy, according to
which the large categories which arise in nature are rarely strict, so
that it wouldn't even make sense to ask for the relevant products and
equalizers.

Mike

Toby Bartels wrote:
> David Leduc wrote:
>
>> What about the characterization of limits in terms of products and
>> equalizers? It states that the limit of a functor F:J->C is
>> constructed by products indexed by the set(oid) of objects and the
>> set(oid) of arrows of J. But if you don't allow equality on objects in
>> J, you only have a preset of objects, not a set(oid).
>
> Consider the analogy between small and strict categories.
> (A category is strict if it is equipped with a notion of equality of objects.
> Logically, this is a structure rather than a property like smallness.)
>
> Often when speaking of small categories, one speaks relative to a universe
> which is a collection of set(oid)s or a collection of set(oid) cardinalities,
> so every small preset automatically comes equipped with a notion of equality.
> In this case, every small category is strict.  Conversely,
> every strict category is small relative to some universe,
> if you accept an axiom such as Grothendieck's axiom of universes.
> So these are very closely related concepts.
>
> As is well known, we are most interested in the limit of F: J -> C for small J.
> Less well known, but also true, we are most interested in it when J is strict.
> In that case, there is no problem; the arrows of J form a set(oid),
> and we can consider products indexed by that set(oid).
> In principle, J doesn't have to be strict, any more than it has to be small,
> but if you have some reason to believe that the limit exists,
> then you can examine that reason to see what product is relevant.
> Most of the time, you can just assume that J is small and strict.
>
>
> --Toby
>

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

Re: equality is beautiful

[Richard Garner]

> To rephrase what Toby said: the construction of limits via products and
> equalizers only works for limits over a domain category which has a
> set(oid) of objects (what Toby calls a "strict category"), whether that
> set is large or small.

Is this really the case? Given any type (=preset) A and any
term A --> ob C (for C a non-strict category), one can define
what it means to be a product of this family of objects in C.
Now given a non-strict category J and a functor F:J->C, one
may construct the limit of F as an equaliser of two morphisms
between products in the usual way. I don't see where equality
on objects is necessary, or even useful.

Richard


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

Re: equality is beautiful

[David Leduc]

Dear all,

On 3/16/10, Richard Garner <rhgg2@hermes.cam.ac.uk> wrote:
> Is this really the case?

I did some research on internet and found a document by Mathieu Dupont
where, at the beginning of Section 4, he claims that it is the case.
But he did not write where equality on objects in necessary. I am
confused...

  http://breckes.org/dokumenty/warning.pdf

David


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

Re: equality is beautiful

[Michael Shulman]

That's a good point.  However, if C is a non-strict category, then
while you can define products over its preset of objects, such a
product is no longer necessarily a particular case of a limit, since
the preset may not have any "discrete" category structure.  So while
you can construct limits over arbitrary (non-strict) categories via
"products" and equalizers if you generalize the notion of "product" in
this way, the converse now fails -- having all limits doesn't seem to
guarantee that you have all "products" in this generalized sense.

Mike

On Tue, Mar 16, 2010 at 3:03 AM, Richard Garner <rhgg2@hermes.cam.ac.uk> wrote:
>> To rephrase what Toby said: the construction of limits via products and
>> equalizers only works for limits over a domain category which has a
>> set(oid) of objects (what Toby calls a "strict category"), whether that
>> set is large or small.
>
> Is this really the case? Given any type (=preset) A and any
> term A --> ob C (for C a non-strict category), one can define
> what it means to be a product of this family of objects in C.
> Now given a non-strict category J and a functor F:J->C, one
> may construct the limit of F as an equaliser of two morphisms
> between products in the usual way. I don't see where equality
> on objects is necessary, or even useful.
>
> Richard
>
>
> [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
>


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

Re: equality is beautiful

[Richard Garner]

> That's a good point.  However, if C is a non-strict category, then
> while you can define products over its preset of objects, such a
> product is no longer necessarily a particular case of a limit, since
> the preset may not have any "discrete" category structure.  So while
> you can construct limits over arbitrary (non-strict) categories via
> "products" and equalizers if you generalize the notion of "product" in
> this way, the converse now fails -- having all limits doesn't seem to
> guarantee that you have all "products" in this generalized sense.

Yes, exactly; however, if one wishes this notion of product
to become a special case of the notion of limit (a demand
which seems not unreasonable) then it is enough to ask your
type theory to have identity types: for then any preset A can
be made into a category A# whose hom-setoids are the identity
types Id_A(x,y) equipped with their propositional equality.
Now limits indexed by A# correspond with products indexed
by A, and so in this setting we recover the theorem that all
limits <---> products and equalisers.

Richard


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

Re: equality is beautiful

[Toby Bartels]

Richard Garner wrote:

>however, if one wishes this notion of product
>to become a special case of the notion of limit (a demand
>which seems not unreasonable) then it is enough to ask your
>type theory to have identity types: for then any preset A can
>be made into a category A# whose hom-setoids are the identity
>types Id_A(x,y) equipped with their propositional equality.

And as well, any preset is thus made into a set(oid).
(Categorially, we form the free set on a given preset.)
And so any category is strict.

Although this is a feature of most type theories in practice,
I've always found it rather artificial.  Bishop's insight
is that you have to *define* equality, and while it's a step up
to say that you *can* define equality if you wish to,
it's unsatisfying to fall back and say you don't *have* to.

Not that identity types can't have their own interesting structure.
The elements of identity types have their own identity types, etc,
so every type becomes not only a set but an infinity-groupoid;
see Awodey & Warren's paper at http://arxiv.org/abs/0709.0248
and Michael Warren's PhD thesis at http://aix1.uottawa.ca/~mwarren/Papers/

But in the philosophical mode where I avoid evil in category theory,
I don't see the justification for identity types in general.


--Toby


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

Re: equality is beautiful

[Thomas Streicher]

> What about the characterization of limits in terms of products and
> equalizers? It states that the limit of a functor F:J->C is
> constructed by products indexed by the set(oid) of objects and the
> set(oid) of arrows of J. But if you don't allow equality on objects in
> J, you only have a preset of object, not a set(oid).

I don't see a problem here. Usually one speaks about small limits, i.e. limits
of diagrams whose shape is a small category. But small categories are categories
internal to the base. Now under the quite common assumption that this base has
finite limits one can speak about equality of objects in the shape of the diagram.

Thomas


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

Re: equality is beautiful

[Michael Shulman]

On Sun, Mar 21, 2010 at 2:36 PM, Toby Bartels
<toby+categories@ugcs.caltech.edu> wrote:
> The elements of identity types have their own identity types, etc,
> so every type becomes not only a set but an infinity-groupoid;
> see Awodey & Warren's paper at http://arxiv.org/abs/0709.0248
> and Michael Warren's PhD thesis at http://aix1.uottawa.ca/~mwarren/Papers/

I think maybe the papers you wanted to refer to for that fact are
Benno van den Berg and Richard Garner, Types are weak ω-groupoids,
arXiv:0812.0298
Peter Lumsdaine, Weak ω-categories from intensional type theory, arXiv:0812.0409
The Awodey+Warren papers are about the other direction, that type
theory with identity types can be interpreted in any
well-enough-behaved model category.

I agree, though, that identity types vitiate the goal of doing
category theory without a notion of equality for objects.

Mike


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

Re: equality is beautiful

[Bas Spitters]

Thorsten Altenkirch suggested the arrow category as an example where
we would want equality on objects:
http://www.mail-archive.com/epigram@durham.ac.uk/msg00285.html

Bas

On Sat, Mar 20, 2010 at 8:18 AM, David Leduc
<david.leduc6@googlemail.com> wrote:
> Dear all,
>
> On 3/16/10, Richard Garner <rhgg2@hermes.cam.ac.uk> wrote:
>> Is this really the case?
>
> I did some research on internet and found a document by Mathieu Dupont
> where, at the beginning of Section 4, he claims that it is the case.
> But he did not write where equality on objects in necessary. I am
> confused...
>
>  http://breckes.org/dokumenty/warning.pdf
>
> David
>


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

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

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