Re: equality is beautiful

[Richard Garner <rhgg2@hermes.cam.ac.uk>]

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