
Date: Fri, 27 Dec 1991 15:18 EST
From: MTHFWL@ubvms.cc.buffalo.edu

Lawvere and Schanuel's new book, CONCEPTUAL MATHEMATICS: A first
Introduction to Categories (Preliminary version), 347+vii pp, paper
is now available from Buffalo Workshop Press, P.O.Box l7l, Buffalo,
N.Y. l4226, USA.  Presupposing only high-school algebra, it is
intended both as a text for a first course in both finite and
continuous mathematics, emphasizing explicit treatment of concepts
as opposed to elaborate computational algorithms, as well as a
leisurely introduction to the categorical outlook for workers in
other areas.  The price of the volume is US$20 plus $3 shipping.

Bill Lawvere
e-mail: mthfwl@Ubvmsb.cc.Buffalo.edu
==============================================================

Date: January 6, 1992

Appended to this is a file listing sites containing material which
has been announced on the categories list as available by anonymous ftp.
The file is available by ftp in [anonymous.categories] at macc2.mta.ca
(138.73.1.2) and it would be happy to be expanded. It will be resent to 
the categories list occasionally. I would be glad for any suggestions
re format and appropriate data for this file, but it is not intended
to include a lengthy, article-by-article description. 

Bob Rosebrugh

+++++++++++++++++++++++++++
This is FTP.SITES in [anonymous.categories] at macc2.mta.ca (138.73.1.2)

The following sites have anonymous ftp directories with
documents of interest to subscribers to the categories list:

Machine                    Directory(ies)              Comment
-------                    -------------               -------

boole.stanford.edu         /pub                  papers by Casley, Crew
(36.8.0.65)                                        Pratt et al.

maths.su.oz.au             /sydcat               papers by the Sydney
(129.78.68.2)                                       categories group;
                                                 computational cat theory 
                                                    software,
                                                 seminar notices etc.

theory.doc.ic.ac.uk        /theory               papers by Abramsky, Taylor,
(146.169.2.37)                                     Vickers et al.;
                                                 diagram macro package by
                                                   Taylor

triples.math.mcgill.ca     /pub                  papers by Barr, Reyes,
(132.206.150.30)                                   Seely et al.;
                                                 diagram macro package by
                                                   Barr

macc2.mta.ca               [.mathcs.rosebrugh]   papers by Rosebrugh and Wood
(138.73.1.2)                                      !note Vax syntax for cd as 
                                                   e.g. cd [.mathcs.rosebrugh]


File updated
2 January 1992
======================================
Subj:	full sub-lex exponential ideals of lccc-s
Date: Thu, 9 Jan 92 12:37:21 MET
From: Thomas Streicher <streiche@fmi.uni-passau.de>

Does any body know the answer to the following question ?

Is there a locally cartesian closed category  C  such that there is a full
sub-left-exact category  D of  C  which is non-reflective and forms an exponen-
tial ideal, i.e. whenever  A is an object in  D  and  X  is an object in  C
then [X->A]  is  (isomorphic to) an object in  D ?

The background to this question is the following.
If something as described above would exist then one can perform the following
construction.

A morphism  f : Y -> X  in  C  is a DISPLAY MAP  iff

    for any  g : Z -> X  :  Pi (!Z) (g*f) : P -> 1  with  P  in  D .

For the collection DISP  of display maps then one can prove :

i) display maps are stable under arbitrary pullbacks

ii) for any  I  in  C  :  DISP / I ---> C / I  reflects finite limits

(iii)  if  f : X -> I  is a display map  and  g : I -> J  is an arbitary
       morphism in  C
       then

        Pi (g) (f)  is a display map as well  .

Now if D  forms an exponential ideal then  DISP / 1 is equivalent to  D
and we would get that the full subcategory of C (in the fibrational sense)
is not reflective w.r.t.  C / C .

This would give an answer to a question I raised on this forum about one year ago.


Thomas Streicher

======================================
Subj:	Re: full sub-lex exponential ideals of lccc-s
Date: Sat, 11 Jan 92 09:59:32 EST
From: pjf@saul.cis.upenn.edu (Peter Freyd)

The method I described to get examples for Streicher's request
can, in fact, be easily modified to achieve full completeness.
Let me give a specific example.

Let  D  be the opposite of the ordered set of all ordinals.
Except for the existence of a bottom element it is a Heyting
algebra, therefore a local CCC.  Let  C  be the result of adjoining
a bottom element.  Then  D  is a full left-closed exponential ideal
in  C.  The bottom of  C  does not have a reflection in  D.   QEF

Best thoughts
  peter freyd
======================================
Subj:	Re: full sub-lex exponential ideals of lccc-s
Date: Mon, 13 Jan 92 12:19:05 MET
From: Thomas Streicher <streiche@fmi.uni-passau.de>


Thanks for the nice counterexample ! I think what you meant is that the constru-
ction works for all Heyting algebras (I mean the finitary version : inf-semi-lat
tice with exponentiation, no infinite sups or infs are claimed) without a least
element. So the archetypical example is the natural numbers with an element for
infinity together with the inverse ordering.

By the way the display maps in a ll these examples are definable in the sense
that whenever  f : X -> I  is an arbitrary map then there is a greatest subob-
ject  m : J >--> I  such that  m*f  is a display map. Thus we have definability
in the sense of Benabou. In all these cases either  m  is identity or  J = 0 .

May it be correct that there are only posetal counterexamples because in this
case equalizers do not cause any problems ??

Thomas Streicher
======================================
Subj:	Re: full sub-lex exponential ideals of lccc-s
Date: Mon, 13 Jan 92 13:20:48 -0500
From: pjf@linc.cis.upenn.edu (Peter Freyd)

[ the first of Peter's messages did not arrive the first time,
and the moderator missed that reference in the second. 
Sorry about that.  Bob Rosebrugh ]


I sent two messages to the categories net only the second of which
seems to have been distributed.  The second begins by referring to
the first.   The following is a slightly edited version of the
first message:

********************************************************************

I wonder if Thomas Streicher's question is really as he states
it.  Take any Heyting Algebra and  "ideal", that is, a subset
closed under finite meet and hereditary upwards.  Then the
ideal is a full "sub-left-exact" subcategory and it is an
exponential ideal.  The bottom element of the Heyting Algebra
has a reflection in the ideal iff the ideal is principal.

If one wants the subcategory to be closed under the formation
of arbitrary limits (not just finite limits) then there are
counterexamples but none that I know that can be so easily described.

Best thoughts,
  peter freyd
======================================
Subject: Re: full sub-lex exponential ideals of lccc-s
Date: Tue, 14 Jan 92 21:06+0000
From: Paul Taylor <pt@doc.imperial.ac.UK>

I must be suffering from schizophrenia, because I can't remember this
counterexample.  Perhaps you'd remind me?

PS What was the simplifying lemma about display maps which you presented
at a PSSL in Cambridge in 1987?
======================================
Subj:	Re: full sub-lex exponential ideals of lccc-s
Date: Tue, 14 Jan 92 05:58:55 EST
From: pjf@saul.cis.upenn.edu (Peter Freyd)


With regard to the Thomas Streicher's question:

  May it be correct that there are only posetal counterexamples
  because in this case equalizers do not cause any problems ??

There may well be a sense in which the answer is yes.  But consider the
following:  let  C  with subcategory  D  be a counterexample.  Let  A  be any
local  CCC.  Then   A x C  with subcategory  A x D  is also a counterexample.
======================================
Subj:	Re: full sub-lex exponential ideals of lccc-s
Date: Wed, 15 Jan 92 12:05:22 MET
From: Thomas Streicher <streiche@fmi.uni-passau.de>

Thanks again. Due to this observation by choosing for A  the categories Set ,
omega-Set or PER-omega  we get counterexamples which are very rich.

IsnBt it the case that by taking the product of some lccc  A  with e.g. the nat
ural numbers with inverse order one gets some aspect of "time" into realizabili
ty models which destroy the existence of existential quantifiers.
Maybe it is worthwhile to investigate connections with Martin-LoefBs work in
mathematics of infinity where he considers sequences of models of type theory
in order to explain infinite objects.

Thomas Streicher

P.S. I think a further interesting counterexample is obtained by taking for  C
the product of 0mega-Set with (N u {infinity})*  and for  D  the full subcatego
ry which is the cartesian product of PER-omega with (N u {infinity})*.
======================================
Subj:	Five Postings
Date: Fri, 17 Jan 1992 20:55:04 EST
From: categories@mta.ca

Due to a mailer failure, most of you did not receive any of the 
messages following. A new mailer is promised soon. Five postings are
concatenated here in hopes of avoiding a recurrence of the problem. Bob ]

000000000000000000000000000
Date: Thu, 16 Jan 92 14:21:46 +11
From: kelly_m@maths.su.oz.au (Max Kelly)
Subject" Kan Complexes

 Does anyone know whether it is the case that a simplicial set B is Kan
whenever it has the property that, for each A (or for each n-simplex A),
homotopy of maps A ---> B is an equivalence relation? Of course here the
maps f, g : A ---> B are said to be homotopic iff they are the restrictions
of a map A x I ---> B. Michael Barr, in a recent letter to me, said that
this is a fact known to topologists; but I don't seem to be able to prove
it. I don't see how the property would even allow one to fill in a 1-horn;
there doesn't seem to be enough there to get any non-degenerate map on the
2-skeleton. Am I missing something?
                                      Max Kelly, 16 Jan.

1111111111111111111111111111
Date: Thu, 16 Jan 92 08:22:04 AST
From: Paul Taylor <pt@doc.ic.ac.uk>
Subject: Thomas Streicher's counterexample

Somewhere the impression has come about that I gave a counterexample to a
question posed by Thomas Streicher.  I think I should make it clear that
whatever this counterexample was, I didn't give it!

222222222222222222222222222
Date: Thu, 16 Jan 92 11:45:48 EST
From: barr@triples.Math.McGill.CA (Michael Barr)
Subject: A model for NWF sets?


The covariant powerset functor has no set-based initial model, but it
seems that the class of well-founded extensional trees is an initial
model.  (A tree is well-founded if every downward chain is finite and
extensional if no node has two isomorphic branches.)  This is
well-known to be a model of set theory, Goedel's standard model, in
fact.  For each n define the nth truncation function, t |--> t|n by
saying that t|0 is a bare root and and if t is derived by attaching
{t_i} to a bare root then t|n is the extensional reflection (there is
one; the obvious equivalence relation is Church-Rosser) of the tree
gotten by attaching {t_i|n-1} to a bare root.  Every tree is so derived,
from well-foundedness.  Now define a metric on the class of trees by
saying that d(t,t') is 2 to the negative of the greatest n such that t|n
= t'|n.  In other words the distance is 2^-n if t|n = t|n, but t|n+1 /=
t'|n+1.  Then the Cauchy completion of this class obviously looks like
NWF trees.  Does anyone know enough about Aczel's work to tell me if
this is a model of his axioms?

BTW, this Cauchy completion is a terminal coalgebra for the functor.
And it makes a difference whether you Cauchy complete and then take the
extensional trees or do it the other way round.  In other words, it is
possible for the limit of a sequence of non-extensional trees to be
extensional, but such trees are _not_ in the model.  The decisive
example is the NWF set defined by x = {x,{x}}, which is clearly the same
as the one defined by x = {x}.  (But I defy you to prove it by starting
with the first one; it is immediate if you begin with the second.)

Michael

333333333333333333333333333333333333
Date: Thu, 16 Jan 92 16:48:26 EST
From: barr@triples.Math.McGill.CA (Michael Barr)
Subject: Amalgamation property for Heyting algebras?

Michael Makkai has shown that something called the Craig Interpolation
lemma is equivalent to fact that in Heyting algebras a pushout of an
injection is an injection.  Now it is easy to show that a pushout of an
injection with a quotient map is an injection, so the question is
reduced to the amalgamation property.  Anyone have an easy proof of
that?

Michael
444444444444444444444444444444444444
Date: Fri, 17 Jan 92 15:34:00 MET
From: Thomas Streicher <streiche@fmi.uni-passau.de>
Subject: background to my question


I think it might be interesting for some people to get explained the background
of the question I posed on the e-mail forum and which has been ANSWERED by P.
FREYD in a very pleasing and hepful way.

Some time ago I was asking myself two questions.

 In the situation that one is given an lccc  C  and a
  class of display maps  D
  respresenting a full  internally complete category of  C    :

  1)  does this imply that display maps are closed under composition,
      i.e one has strong sums

      for this question the answer is no and described in my MSCS paper
      "Dependence and Independence Results for
        (Impredicative) Type Theories "

  2)  if one assumes that there is a generic morphism for  D
      then by an internalization of FAFT one can prove that
      the full subcat as given by  D  is reflective in the fibrational sense,
      i.e. one has weak sums or existential quantification

      now the question was whether existential quantification is still
      guaranteed if one drops the assumption that there exists a generic
      morphism, i.e. the assumption of SMALLness

      the answer to this last question is NO  and the counterexample
      - BASED on Peter FREYDs helpful lemma  -  is the following :

      take an lccc  C  together with a class of display maps  D  representing
      a full internally complete subcat of  C  ;

      let  N*  be the category which is the opposite of natural numbers 
      extended with an object   inf  strictly greater than all natural 
      numbers n ;

      now N* x C  is an lccc , too, but now take as display maps those
      morphisms

         (x -> y , f ) : (x,A) -> (y,I)

      where  f : A -> I  is in  D    and    x = inf   iff   y = inf   ;

      let us call this new class of display maps  DN ;

      then for the lccc  N* x C   with this new class DN  of diplay maps
      it is the case that

      DN  represents a full internally complete subcat of  N* x C

      BUT  it is NOT reflective  !!



Another question arising in this context is :

 How is the whole question related to
 sub-lccc-ness of the category represented by  D  ??

We call  D  REPRESENTING a FULL SUB-LCC  of  C

	 iff

 for any object  I  of  C

    the full subcat  D / I  of  C / I  is a full sub-lccc .

What I have shown in my MSCS paper is that

   If  D  represent a full sub-lccc of  C
  then D  is closed under composition !!

   On the other hand if  D  represents a full internally complete subcat of  C
    and  D  is closed under composition
    then  D  represents a full sub-lcc of C .


What I also have shown in my MSCS paper is that

    If you take for  C  the category  w-Set
    and for  D  those morphisms corresponding to families of extensional pers
    then  D  is NOT closed under composition,
    thus it does not represent a full sub-lccc !


This, of course, does not immediately imply that the category of extensional
pers  is not  lccc .

BUT my counterexample contains more. I have constructed a morphism  f : Y -> X
where  Y  and  X  are extensional pers and such that it holds that

     the domain of   Pi (! X) f  is not isomorphic to an extensional per .

Thus extensional pers do not form a sub-lccc of w-Set !



Even more one can show that  X  is Sigma replete and  f  represents a family of
Sigma replete pers.

Let us call  Y.x  the family of pers corresponding to  f  .

Of course, there is more to be shown than
that for any  x  in  X  the Y.x  is Sigma replete !
(Thanks to Wesley Phoa for pointing me to this problem !)

But as  Y.x   is   [Z.x -> Sigma]  for a family  Z.x  of pers ,
one can realize UNIFORMLY IN x  that  Y_x  is Sigma replete !

Thus w.r.t. the following aspects in Synthetic Domain Theory the situation
is the same as in ordinary domain theory :

The category of predomains is complete, but not lccc !



Thomas Streicher
======================================
Subj:	Kan complexes
Date: Sun, 19 Jan 92 09:04:58 EST
From: barr@triples.Math.McGill.CA (Michael Barr)

I have to admit not having ever seen a proof of what Max was asking
about.  Here is the way I see it in dimension 1.  I assume that it is
similar, but more complicated in higher dimensions.  Consider the
beginnings of a simplicial set and assume that homotopy, which I will
denote ~ is an ER:

                   d^0
                  ---->
              X_1 <---- X_0
                  ---->
                   d^1

with the degeneracy s in the middle.  The presence of the degeneracy
forces the homotopy relation to be reflexive, by the way, although that
is not what is involved here, but it is what is behind Max' question.
The crucial thing is that any 1-cell is a homotopy between its two
vertices.  If x in X_1, then x is a homotopy between d^0(x) and d^1(x).
Now let x^0, x^1 in X_1 satisfy d^0(x^0) = d^0(x^1), which is the only
equation satisfied by that kind of 1-horn.  Then we have d^0(x^0) ~
d^1(x^0), d^0(x^0) ~ d^1(x^0) and d^0(x^0) = d^0(x^1).  If homotopy is
to be an ER, we must have d^1(x^0) ~ d^1(x^1), which means that we
need an element we will call x^2 in X_1 such that d^0(x^2) = d^1(x^0)
and d^1(x^2) = d^1(x^1), which is the fill-in required.  There are two
other kinds of horns, depending on which simplex is omitted, but the one
with x^1 omitted I have checked and it is similar and the third one is
just the reverse of this one.

This must be in some of the early papers of Kan (late 50s) or maybe John
Moore (early 60s).  Don't ask the categories net; ask algebraic
topologists.

Michael


======================================
Subj:	representable 2-functors
Date: Sun, 19 Jan 92 20:41:52 CST
From: kapranov@math.nwu.edu (Mikhail Kapranov)

I would like to be able to place a good reference about representable
functors from a weak 2-category (or a bicategory,--this is what
Benabou considered) to Cat -the 2-category of all categories.
For example the correspondence that takes each object to the
corresponding representable 2-functor is a (weak) equivalence
of 2-categories (analog of Yoneda's lemma). This, in particular,
shows at once that any WEAK 2-category is weakly 2-equivalent
to a STRICT one (where associativity for composition
of 1-morphisms and the units arer strict).
I suppose these things are well known to people, but what would
be a good reference?

Mikhail Kapranov

======================================
Subj:	Re: Amalgamation property for Heyting algebras?
Date: Mon, 20 Jan 92 09:10:09 +0000
From: Andrew.Pitts@cl.cam.ac.uk

>Michael Makkai has shown that something called the Craig Interpolation
>lemma is equivalent to fact that in Heyting algebras a pushout of an
>injection is an injection.

To be precise I think Michael was claiming a new proof of the latter fact (the
equivalence of CI to pushout stability is well known, to some).

>Now it is easy to show that a pushout of an
>injection with a quotient map is an injection, so the question is
>reduced to the amalgamation property.  Anyone have an easy proof of
>that?

For a constructive (and easy!) proof see my paper "Amalgamation and
interpolation in the category of Heyting algebras", Jour Pure Appl. Algebra
29(1983)155--165.

Andy Pitts
======================================
Subj:	Re: representable 2-functors
From: street@macadam.mpce.mq.edu.au (Ross Street)
Date: Tue, 21 Jan 92 16:35:55 EST

>
> Date: Sun, 19 Jan 92 20:41:52 CST
> From: kapranov@math.nwu.edu (Mikhail Kapranov)
>
> I would like to be able to place a good reference about representable
> functors from a weak 2-category (or a bicategory,--this is what
> Benabou considered) to Cat -the 2-category of all categories.
> For example the correspondence that takes each object to the
> corresponding representable 2-functor is a (weak) equivalence
> of 2-categories (analog of Yoneda's lemma). This, in particular,
> shows at once that any WEAK 2-category is weakly 2-equivalent
> to a STRICT one (where associativity for composition
> of 1-morphisms and the units arer strict).
> I suppose these things are well known to people, but what would
> be a good reference?
>
> Mikhail Kapranov
>

The Yoneda Lemma for bicategories appears in my paper "Fibrations in
bicategories" Cahiers top et geom diff 21 (1980) 111-160 [A correction, not
to do with the Yoneda Lemma, is in 28 (1987) 53-56.]

The application of this result to coherence for bicategories was realised
in the last year by Robert Gordon and John Power. It was discussed very
openly at the Category Theory Conference in Montreal Mid 1991. I remember
knowing of the application of the Yoneda Lemma to homomorphisms [essentially
that every fibration is equivalent to a split one, as per Giraud's book] in
the late 60's, but I do not recall observing, and know of no old reference for
the Gordon-Power realisation.

[For readers who missed out in Montreal, the point is that: given a bicategory
K, there is a homom of bicategories K --> Hom(K^op,Cat) which is an equivalence
on hom-categories; but Hom(K^op,Cat) is a 2-category; so K is biequivalent to
the full sub-2-category of Hom(K^op,Cat) consisting of the representables. This
gives a different proof of Mac Lane's coherence theorem for monoidal categories
and of the Mac Lane-Pare version for bicategories.]

A full account of a very slightly modified version of this approach to
coherence of monoidal (=tensor) categories appears in Joyal-Street "Braided
tensor categories" (still to appear in Advances in Math). We go on to do
coherence for tensor functors (=strong monoidal functors) and braided tensor
categories.

Furthermore, Gordon, Power and I have used a similar technique to prove a
coherence theorem for tricategories. This was announced in the Abstracts for
the American Math Soc Meeting in Baltimore a week or so ago; Bob Gordon gave
a talk at that conference. We have a paper in preparation. [Tricategories
are like 3-categories except that composition of 1-cells is only associative
up to equivalence and is only a homomorphism of bicategories &c &c.] While
every bicategory is biequivalent to a 2-category, not every tricategory is
triequivalent to a 3-category; the Gray tensor product is relevant, as expected
after the work of Joyal-Tierney on homotopy 3-types.

Regards to all,
--Ross Street
======================================
Subj:	Re: Amalgamation Property ...
Date: Wed, 22 Jan 92 16:18:13 EST
From: barr@triples.Math.McGill.CA (Michael Barr)

I would still like to see a simple algebraic proof based on the fact
that a cyclic H-module is flat, for a Heyting alg H.  Andy's proof
didn't seem all that easy to me. The background is that there is a
notion of H-module and the pushout of a pair of Heyting algebra maps
out of H is also the tensor product of H-modules.  By an H-module I
mean a sup semi-lattice that has unary ops x /\ - and x ==> - for
each element x of H, and satisfying the obvious identities.  Now for
a ring R if every cyclic R-module is flat, so is every R-module.
Here, every cyclic H-module is flat.  Are they all?

Michael
======================================
Subj:	my recent question whether a complex is Kan if homotopy is an ER.
Date: Fri, 24 Jan 92 14:10:25 +11
From: kelly_m@maths.su.oz.au (Max Kelly)

 Michael Barr's letter of 19 Jan to the bulletin board about this seems to
me to be based on a misunderstanding. He says he shows how to fill in a 1-horn;
but all he does is to produce the third side of a triangle when two sides are
given - while what the Kan property demands is that one be able to fill in the
whole triangle, interior and all. My difficulty was to see how to get any non-
-trivial stuff on the interior at all, using "homotopy is an ER".
 At any rate, I have now received a counter-example from Bill Dwyer at
Notre Dame; here it is:
               --------------------------------------------------
 I'm beginning to think that the answer to your question is "no".
Here's a possible counterexample and a line of argument. Suppose that
E is the category with one object x and one non-identity morphism
e: x-->x, where e^2=e.  Then

(1) If C is a category and F, G: C --> E are functors, then F and G
are connected by a natural transformation.  In fact, the function
which assigns to any morphism of C the map e: x --> x is a natural
transformation from F to G.  There are only four diagrams to check:

      1                1              e               e
   x ---> x	    x ---> x       x ---> x    	   x ---> x
e  |      | e	 e  |      | e  e  |      | e  	e  |      | e
   V      V	    V      V       V      V    	   V      V
   x ---> x	    x ---> x       x ---> x    	   x ---> x
      1        	       e              1        	      e

(2) Let N be the nerve functor from categories to simplicial sets and
L its left adjoint.  L assigns to any simplicial set A the category
whose objects are the vertices of A and whose morphisms are generated
by the one-simplices of A, with one relation for each two-simplex.
Let f, g: A --> N(E) be two simplicial maps.  These correspond to
functors F, G: L(A) --> E.  As in (1) there is a natural
transformation between F and G, which passes to a homotopy

          H : N(L(A)) x \Delta[1] ----> N(E)

between N(F) and N(G).  Composing H with the map

             A x \Delta[1]  ----->  N(L(A)) x \Delta [1]

induced by the adjunction map A --> N(L(A)) gives a homotopy between f
and g.   In other words, for any two maps f, g: A --> N(E) there is a
homotopy from f to g, so that in particular homotopy is an equivalence
relation on maps A -> N(E).

(3) N(E) is not a Kan complex.  The nerve of a category is a Kan
complex iff the category is a groupoid.  For instance, in N(E) the
following cofiguration cannot be extended to a two-simplex, because e
does not have an inverse.

                    x
                   A
               e  /
                 /
               x  ---> z
                   1

I think this is ok.  Let me know if you find a hole in it.

                                                           Bill Dwyer
                 ----------------------------------------------------------
                                              Max Kelly, 24 Jan.
======================================
Subject: 2-natural transformations
Date: Fri, 24 Jan 92 15:12:26 +11
From: kelly_m@maths.su.oz.au (Max Kelly)

 Does the community have any reaction to the following observation, that we
have made these last few days?

 Let A and B be 2-categories, and F,G : A ---> B be 2-functors. There is
a notion of 2-natural transformation t : F ---> G; such a t is not only to
be natural, in the usual sense, with respect to 1-cells, but to have the
appropriate property with respect to 2-cells as well. Certainly mere natural-
ity does not imply 2-naturality, as one sees on taking for A the free-living
2-cell. Yet it DOES imply 2-naturality if A admits tensor products with the
arrow-category 2 (or dually cotensor products with 2).

 A consequence is that the forgetful functor, from the category of finitary
2-monads on a locally-finitely-presentable 2-category A to the category of
finitary monads on the underling category of A, is a fully-faithful functor
with both adjoints. In particular, a finitary monad on Cat or such-like has
at most one enrichment (although usually none) to a 2-monad; and similarly
for the more common case of enrichability over the closed category of
groupoids.

                John Power and Max Kelly, at Sydney - 24 Jan.
======================================
Subj:	with some trepidation
Date: Thu, 23 Jan 92 14:03 GMT
From: MAP010@vaxa.bangor.ac.uk (Philip Ehlers)

%This is a LaTeX file which outlines a possible counterexample
%to the conjecture which was on the mailing board at the
%beginning of the week. I apologise for forgetting who
%originally asked the question, and for the somewhat eccentric
%style of the answer!

\documentstyle{article}
\title{A Counter Example}
\date{23 January 1991}
\begin{document}
\maketitle

The question was asked, on the category theory mailing board, as to
whether this conjecture is true.

\newtheorem{Kan}{Conjecture}
\begin{Kan}
Let $B$ be a simplicial complex. If homotopy is an equivalence
relation on ${\em SS}(A,B)$ for all $A \in ob({\em SS})$, then
$B$ is a Kan complex.
\end{Kan}

I think I have a counter example, and would appreciate it if anyone
could spot the flaw(s) in the argument.

\rule{0mm}{20mm} Let B be the simplicial set which is the complete
directed graph on three vertices. Pictorially, this is the following:-


\begin{picture}(200,150)
\put(50,110){\circle*{5}}
\put(150,110){\circle*{5}}
\put(100,20){\circle*{5}}
\put(55,112){\vector(1,0){90}}
\put(145,108){\vector(-1,0){90}}
\put(55,105){\vector(1,-2){40}}
\put(90,25){\vector(-1,2){40}}
\put(145,105){\vector(-1,-2){40}}
\put(110,25){\vector(1,2){40}}
\end{picture}

This simplicial set is clearly not Kan.

\rule{0mm}{10mm} There are nine simplicial set morphisms
$I \longrightarrow B$ which we shall call $f_{jk}$ where this
maps the non-degenerate element of $I_1$ to the edge from $j$ to $k$
(for $j = k$ this is just the degenerate edge at $j$).  We shall
denote the non-degenerate element of $I_1$ by $\iota$.

\rule{0mm}{10mm} Now, consider any $f:A \longrightarrow B$ for any
simplicial set $A$. Since all $n$-simplices in $B$ are degenerate
for $n \geq 2$, we have that $f_n(a) = sf_{jk}$ where $s$ is some
combination of degeneracy maps; note that if $j = k$, then $s = s_0^n$.
Since simplicial morphisms commute with the face and degeneracy maps,
this means that $f$ is completely determined by its effect on the
$0$-simplices and $1$-simplices.

\rule{0mm}{10mm}

We require to show that the relation of homotopy is an equivalence
relation on the hom-set $\underline{\em SSets}(A,B)$ for any $A$.
Clearly it is reflexive, as there is a simplicial set morphism from
$(A \times I)$ to $B$ which is dummy in the second variable.

\rule{0mm}{10mm}
If we now consider any two simplicial morphims $f,g:A \longrightarrow B$
and a homotopy $F:(A \times I) \longrightarrow B$ from $f$ to $g$,
we construct a homotopy $G$ from $g$ to $f$ as follows:-

\[G_0(a,0) = F_0(a,1) \;\;\; \mbox{and} \;\;\; G_0(a,1) = F_0(a,0)
\;\;\; \mbox{for} \;\;\; a \in A_0\]

\[ \mbox{If} \;\;\; F_1(a,\iota) = f_{jk}(\iota) \;\;\; \mbox{then} \;\;
\; G_1(a,\iota) = f_{kj}(\iota) \;\;\; \mbox{for} \;\;\; a \in A_1 .\]

Since these are all the elements of $B$, this determines $G$. Clearly

\[ G(a,s_0^n1) = F(a,s_0^n0) = g(a) \;\;\; \forall a \in A_n \]

\[ G(a,s_0^n0) = F(a,s_0^n1) = f(a) \;\;\; \forall a \in A_n \]

\rule{0mm}{10mm} Lastly, assume we have two homotopies, $F$ from $f$
to $g$ and $G$ from $g$ to $h$.  Then, we construct a homotopy $H$
from $f$ to $h$ as follows:-

\[ H_0(a,0) = G_0(a,0) = h_0(a) \;\;\; \mbox{and} \;\;\; H_0(a,1) =
F_0(a,1) = f_0(a)  \;\;\; \mbox{for} \;\;\; a \in A_0 .\]

If $F_1(a,\iota) = f_{jk}(\iota)$ and If $G_1(a,\iota) = f_{kl}(\iota)$
then $H_1(a,\iota) = f_{jl}(\iota)$ for $a \in A_1$.

This is transitivity, and so the example is complete.

\rule{0mm}{20mm}

Comments, please!

\rule{100mm}{0mm}  ${\em Phil}$


\end{document}
======================================
Subj:	Kan complexes (twice)

Date: Sun, 26 Jan 92 12:38:47 EST
From: barr@triples.Math.McGill.CA (Michael Barr)
Kan complexes


Max is right; I forgot what I was doing.  Nevertheless, I learned long
ago that a simplicial set is Kan iff the homotopy relation on maps to
that set is an equivalence.  I tried to prove it here with no references
and I cannot, but I can certainly give a plausibility argument.  I'm not
sure I ever knew the whole proof.  It must be in papers of Kan, in the
late 50s.  The plausibility argument is that if x^0 and x^1, say, are
such that d^0x^0 = d^0x^1 and I want to find a 2-simplex of which x^0
and x^1 are d^0 and d^1, I begin by showing that x^0 ~ s^0d^0x^0 =
s^0d^0x^1 ~ x^1.  It follows that there is a simplex of which x^0 and
x^1 are two of the faces.  Then you have to find one of which it is the
first two faces and I am not sure how to proceed.  To see that x^0 ~
s^0d^0x^0, we calculate that d^0s^1x^0 = s^0d^0x^0, while d^1s^1x^0 =
x^0.

Dwyer's example seems to be that the nerve of a category isn't Kan.
Yes, in fact about 1970, Boardman and Vogt showed that the nerve of a
category always satisfies the "middle Kan" condition, meaning that it
satisfies the condition for all missing indices except the first and
last, but is not in general Kan.

But it is not clear what is the point of including Dwyer's example.  It
is certainly not an example of a complex in which homotopy is an
equivalence relation.

Michael
++++++++++++++++++++++++++
Date: Sun, 26 Jan 92 14:53:29 EST
From: barr@triples.Math.McGill.CA (Michael Barr)

The example from Philip Ehlers is interesting and, although I haven't
checked it, I presume it is correct.  On the other hand, my last posting
is also right (and his example fails it too).  And I _do_ remember being
told that a complex is Kan iff homotopy is an ER.  So what gives?  Well,
way back when I studied algebraic topology, we were told that two k
simplexes in a SS were homotopy if there was an n-simplex (n > k) of
which they were faces.  Then homotopy of simplexes is the ER generated
by this.  Now when you triangulate a square (that is, I x I) you get two
triangles, so that, for example, two 1-simplexes are homotopic, by the
reln that Ehlers used, if there are a pair of simplexes with a common
edge of which these are faces of the one and the other.  Of course,
these generate the same ER, but they are not the same ER and it is
possible for one, but not the other, to be an ER.

Michael
======================================
Subject: groups in GROUPOIDS
From: dyetter@math.ksu.edu (David Yetter)
Date: Mon, 27 Jan 92 9:20:08 CST

I'm wondering whether anyone (most likely by anyone I mean Ross Street,
Andre Joyal or Ronnie Brown, but I thought I'd ask the net) knows a
structure theorem for groups in GROUPOIDS.

I've worked out that if G is the group of objects, H the group of
connected components and A the (necessarily abelian) group of automorphisms
of the identity object, then the group of arrows must by a semi-direct
product of G x_H G with A, with source and target maps being projections, but
I have not been able to show or find a counter-example to the conjecture that
the map assigning identity maps to objects must be (\Delta, 0) and composition
must be addition on the A components, and forgetting the common target/source
in the other components.

This seems to be something which should be known, so before putting more
time in, I thought I'd ask.

--David Yetter
======================================
Subj:	Re: my recent question whether a complex is Kan if homotopy is an ER.
Date: Tue, 28 Jan 92 13:30 GMT
From: MAP010@vaxc.bangor.ac.uk

I have to apologise, because my example is incorrect - firstly,
the proof of symmetry is wrong, and secondly, the proof of
transitivity is wrong, and neither can be rectified -
	There is a homotopy from any edge to its end point, and
a homotopy from the start of any edge to the edge itself. This
kills symmetry - and transitivity fails because there is no
homotopy between edges if they cover all three vertices, yet
if (say) we have an edge from 0 to 1 and an edge from 1 to 2, we
have a homotopy from 01 to 1 and a homotopy from 1 to 12.
So the whole example fails - fairly comprehensively!
	As a matter of interest, why was the question asked in the
first place? - also, has anyone asked Prof. Kan?
		I'll check my counter-examples more carefully next
time! -
		Phil Ehlers
======================================
Subj:	extensional realizability refutes Scotts axiom
Date: Tue, 28 Jan 92 14:35:00 MET
From: Thomas Streicher <streiche@fmi.uni-passau.de>


EXTENSIONAL REALIZABILITY REFUTES SCOTT'S AXIOM

It is well known that in the category of w-Sets there are several
full small internally complete subcategories :


-   PER  :  interprets propositions


-   complete extensional pers , Sigma replete pers  :



       candidates for effective domains  !


Now the idea might be to use  PER  as propositions to speak about
effective domains.

Of course, this is possible !

BUT the logic is quite weak in the sense that the Proposition
expressing Scott's Axiom is not realized !!

PROOF :  Let  SIG  denote the per corresponding

         to the r.e. subobject classifier .

If Scott's Axiom (see e.g. M. Hyland in the Como Proc. or P. Taylor

                  in the LICS'91 Proc. !)

were realizable then there would exist a realizable morphism

   M : ((N -> SIG) -> SIG) -> N*


( N  is the predomain of natural numbers and  N*  is  N  with bottom)

such that  for all   F  in  (N -> SIG) -> SIG)  :

(a)    M(F) = )bot)   iff   F()lambda ) x . )top)) = )bot)

and

(b)    M(F) = n  implies   F()lambda) x < n . )top)) = )top) .


As  M  is realizable it is monotonic we have that

for all   F  in  (N -> SIG) -> SIG)  :

    M(F)   less_or_equal    M()lambda ) f . )top))  .


Thus M  applied to the least element gives   )bot)  and

there exists a natural number  n  such that for all other  F

     M(F) = n .

But that would mean that for all  F  which are not least it holds
that

   f(k) = )top)  for all  k < n   implies   F(f) = )top)  .

BUT THIS IS A CONTRADICTION :

consider    F := )lambda) f . f(n)  ;

this  F  is nontrivial and   F()lambda) x < n . )top)) = )bot) .

Thus such an  M  (Modulus of Continuity)  cannot exist  .

                                      END OF PROOF

Of course, this proof can be performed for any reasonable
axiomatization of SDT in an extensional type theory :

If  N  is a proposition we can prove

that all elements of  N are equal !
Thus all propositions contain at most one element !

Thus we are again back at the effective tripos over w-Set ,
i.e. in some sense the topos-theoretic approach to SDT is the best we
can expect.
Actually to my opinion we do not need the full topos logic

it is sufficient to consider triposes.

I think the axiom of comprehension :

    A  type  ,  P  predicate on  A
   ---------------------------------
       { x : A | P(x) }  type

is not very nice to work with syntactically.

At least I do not know a nice treatment by  proof rules.

By the way it is not a real restriction : from any tripos we can
construct the associated topos.


Thomas Streicher
======================================
Subj:	RE: groups in GROUPOIDS
Date: January 30,1992
From: MAS013@vaxa.bangor.ac.uk

Here is a reply to Dave Yetter's query.
The Magic words are "crossed modules".  The basic reference is :
R.Brown and C.B.Spencer, G-groupoids, crossed modules and the
fundamental groupoid of a topological group, Proc.Konink. Ned. Akad.
Weten. 79, 1976, 296-302.
The results seem to have been known earlier. In fact if one thinks of a
groupoid as being a generalisation of an equivalence relation, the proof
of the equivalence of crossed modules and groups in groupoids is but a
slight generalisation of the undergraduate proof that normal subgroups
and congruences are equivalent ways of presenting the same information.
Does this give the sort of structure theory required?
Tim Porter.
++++++++++++++++++++++
From: street@macadam.mpce.mq.edu.au (Ross Street)
Date: Wed, 29 Jan 92 10:37:42 EST

Dear David,

In a bit of a hurry, but saw your message. Groups in GPD are crossed modules
a la Whitehead. Is this what you want? There are many references (eg the
Mq Math Report on Braided monoidal categories --1986 version).

Regards,
Ross
++++++++++++++++++++++

Date: Wed, 29 Jan 92 16:11:08 EST
From: beck@math.cornell.edu (Jonathan Beck 726 Univ Room 305)

   Stephen Chase tells me that the answer to the question, if he
understands it correctly, is contained in

   J.-L. Loday, "Spaces with finitely many nontrivial homotopy groups",
   JPAA 24(l982), Lemma 2.2, p. l83

and is "a crossed module."
   Jon Beck

+++++++++++++++++++++
From: Paul Taylor <pt@doc.imperial.ac.uk>
Date: Wed, 29 Jan 92 14:17:45 GMT

	Internal categories in the category of groupoids.

David Yetter asked whether there is a structure theorem for
"groups in GROUPOIDS".

I interpret this question as "models of the finite-product theory of groups
in the category (which has finite products) of groupoids and homomorphisms".
I have a suspicion that David had something different in mind,
such as "groupoids in groups", but shall consider the question as posed.

Remember, incidentally, that the category of sets is a full subcategory
(preserving all sorts of structure) of the category of groupoids.
[The latter is, unlike groups, (locally?) cartesian closed as well.]

Now internal *categories* in groupoids [and this easily specialises to groups]
seem a natural generalisation of the quotienting of a preorder to give a poset,
ie the "skeletalisation".
We know that there's no natural way of just picking one object from each
isomorphism class - so instead take the entire isomorphism class and
consider it as a group, ie as a component of the groupoid of objects.
Commutative squares with two sides isomorphisms provide the groupoid of
morphisms.
The construction is universal in a way which I shall leave to the
reader to formulate.

This idea has an application to polymorphism.
Eugenio Moggi and Martin Hyland once proposed as a categorical interpretation
of quantification over types simply taking the product indexed by
the set of [names of] objects of the category.
[We have in mind categories with a small number of isomorphism classes of
objects - it's quite possible to have a cartesian closed category with exactly
two (nonisomorphic) objects - we call it a model of the lambda calculus with
eta and surjective pairing.]
Unfortunately this idea is not invariant under categorical equivalence,
and is therefore objectionable to the sensibilities of semantic categoricians
such as myself.

However the idea may be re-interpreted internally in the category of
groupoids, and then becomes invariant, as Edmund Robinson observed.

In fact something similar, though slightly more complicated, arises naturally
in stable domain theory. The trace factorisation (see my unpublished 1988
paper, available by anonymous FTP from theory.doc.ic.ac.uk) expresses
stable functors as spans and cartesian transformations as rigid comparisons
between them, making the original 2-category an internal category in the
category of domains and rigid comparisons.
In the case of coherence spaces, the latter is equivalent to just the
category of graphs and embeddings; this easily generalises to dI-domains.
For (my) quantitative domains [see my paper in the Manchester Category
Theory and Computer Science proceedings, LNCS 389, also FTP] it is the
category of groupoids and homomorphisms.
In both these cases, second order quantification in the standard domain way
[which has been attributed to Girard, but was in my thesis before, and I didn't
regard it as original, though I don't know to whom to attribute it - probably
Plotkin] coincides with the Moggi-Hyland-Robinson interpretation.

Paul Taylor
======================================
Subj:	Re: extensional realizability refutes Scotts axiom
Date: Thu, 30 Jan 92 20:49:50 EST
From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic)

	Actually to my opinion we do not need the full topos logic
	it is sufficient to consider triposes.
	I think the axiom of comprehension :

	    A  type  ,  P  predicate on  A
	   ---------------------------------
 	      { x : A | P(x) }  type

	is not very nice to work with syntactically.

I appreciate Thomas Streicher's interesting observation about PERs
but I don't see how does it lead him to this opinion about the comprehension.
Comprehension is not a special property of PERs, nor are PERs its special model.
Comprehension doesn't seem to play any role here.

PERs are used as propositions/truth values when one uses them to model
something like the Theory of Constructions. (Comprehension comes in, I suppose, 
only in a paper where I showed that Constructions can be given a familiar 
"set-theoretical" appearance, Springer LNCS #530.) I do not understand the
point of comparing whether it is better to use Constructions (with or 
without comprehension) or the internal language of a topos. These things 
are at different levels. (Tripos is clearly weaker. For some purposes, 
however, I am sure that even first order logic will do.)

	Regards to all,
	Dusko Pavlovic


P.S. Concerning the proof-theoretical difficulties with comprehension (if this
is meant by "not very nice to work with") I can only say that these
difficulties can not be a sufficient reason to dismiss a logical operation. 
Comprehension is certainly less difficult than the sum or the existential 
quantifier.
======================================
Subj:	Re: extensional realizability refutes Scotts axiom
Date: Fri, 31 Jan 1992 13:54:22 +0100
From: Thomas Streicher <streiche@fmi.uni-passau.de>

Here are some remarks on Duskos reaction on my comments about
comprehension.

What I meant was the following :  comprehension is a means for
TRANSFORMING PROPOSITIONS (i.e. objects in the fibre of some
hyperdoctrine) to DATATYPES (i.e. objects in the base)
in other words it allows to CONSIDER collections of proofs as types
of objects.
That is what I would call a mixing of levels of language :

   "data"  are "real objects"

   WHEREAS

    "proofs"  are  "meta objects"  .

So one might be able to define functions which depend on proof
objects but deliver say natural numbers.
If I remember correctly exactly this is what Dusko wants to avoid by
his theory of predicates.

Thomas Streicher

P.S.  I - of course - do not mean that comprehension is

      "inconsistent"  BUT I mean that it changes the notion of
      algorithm considerably and in an unintuitive way.
