Subj:	CTCS 91, last announcement
Date:        Wed, 07 Aug 91 09:38:45 ADT
From: curien@FRULM63.BITNET (Pierre-Louis Curien)



                       FOURTH BIENNAL CONFERENCE ON
             CATEGORY THEORY AND COMPUTER SCIENCE (C.T.C.S.)
                           3-6  September 1991

LAST ANNOUNCEMENT
LATE REGISTRATIONS ARE ACCEPTED

The Fourth of the Biennal Summer Conferences on Category Theory and
Computer Science will be held in Paris (France).

The main purpose of these conferences is to link research in category
theory with computer science.  The importance of categories in
understanding basic issues in computer science is now well established.
Other structures in logic, algebra and topology are also seen as
fundamental and the scope of the conference is to cover
applications of these structures as well.
Proceedings are published in the Springer LNCS series.

                    Organising and Program Committee
Samson Abramsky, Pierre-Louis Curien, Peter Dybjer, Giuseppe Longo,
John Mitchell, David Pitt, Andrew Pitts, Axel Poigne', David Rydeheard,
Don Sannella, Eric Wagner.

                INVITED SPEAKERS
   Albert Burroni
   Eugenio Moggi
   Thierry Coquand
   Ugo Montanari
   Peter  Freyd
   Robert  Tennent

Local Arrangements Office

C.A.I.M.E.N.S/E.N.S.
45, rue dUlm
75230 Paris Cedex 05

Tel : (33) (1) 43 29 12 25 ext. 3279
Fax : (33) (1)  46 34 05 31
Email: butery@dmi.ens.fr
Person in charge:  Chantal Butery

Sponsorship: MRT (Ministe`re de la recherche et de la technologie),
CNRS (Centre national de la recherche scientifique),
MEN (Ministe`re de l'e'ducation nationale).

Location: The  conference will take place at:
                FIAP  Jean Monnet
                30, rue Cabanis
                75014 Paris
                France
                (Me'tro station : Glacie`re)

Accommodation, breakfast and self facilities for lunch or dinner
will be provided by FIAP and are included in the registration fees
(as well as a conference dinner).

Accommodation : On the basis of students prices, the FIAP arranged for
CTCS participants the possibility of booking double rooms to be shared
or single rooms (in a limited number).  Both types of rooms are provided
with private shower, wash-basin, toilets and telephone.

Other events : There will be a conference dinner.  FIAP can also provide
information on touristic or cultural activities in Paris and Paris area.

Accommodation :Please fill and return your registration form to the
Local Arrangements Office (CAIMENS/ENS), accompanied with a cheque of
the corresponding amount in French Francs payable at CAIMENS.
If you find it easier, you can also make a bank transfer to CAIMENS :

Bank name and address : Socie'te' Ge'ne'rale
37, rue Gay-Lussac, 75005  Paris.
Account number: 00037266208

with the reference CTCS, and making sure that your name will appear
clearly.  Acknowledgment will be dispatched in due time.


C.T.C.S - 91  Registration Form

Please complete and return this Registration Form(or a copy of it)
before July 19th  to
C.A.I.M.E.N.S -  45, rue dUlm - 75005 Paris - France .

One Form per participant is requested.  Enclose your payment of the
corresponding amount by cheque in french francs, (or join a copy of your
bank transfer) payable to C.A.I.M.E.N.S.

NAME _________________________________
Surname  (M / F)__________________________
Address :   ______________________________
Organisation (or Private)
______________________________________
______________________________________
______________________________________
City(+code)_____________________________
Country   _______________________________
E-mail __________________________________
Arrival date ________ Departure date :__________

Extension of accommodation cannot be guaranteed before and
after  the end of the conference).

To be registered at the Conference, you have to pay the general
fees for an amount of 1000,- (ff) (proceedings and conference dinner
included) and
ADD accommodation expenses:

Monday 2nd untill Thursday 5th  = 4 nights
including breakfast and self for  lunch or dinner

Single room (limited  number) :            1100,- (ff)
or
Double room *:                             800,- (ff)

Total amount :

 * Preferably  to be shared with;   Name, surname:

                  C.T.C.S.  -   91    P R O G R A M M E

        Tuesday   (September 3rd)

9:30  -  10:30   P.  Freyd, invited  talk
10:30  -  11:00 Coffee / Tea Break
11:00  -   11:40 T. Ehrhard & P.Malacaria, Stone  Duality
for Stable Functions
11:40  -   12:20 R. Amadio, Bifinite Domains:  Stable Case

Lunch

14:00  - 15:00  R. Tennent ,  invited talk
15:00  -  1540  A. Edalat & M. Smyth, Categories of
Information Systems
15:40  - 16:10  Coffee / Tea Break
16:10 - 16:50   R. Hoofman &  H.Schellinx,Collapsing
Graph Models by Preorders
16:50 - 17:30   P.  O'Hearn, Linear Logic and
Interference Control


        Wednesday   (September 4th)

9:30 - 10:30    A. Burroni, Invited talk
10:30 - 11:00   Coffee / Tea Break
11:00  - 11:40  S. Hirokawa, BCK-formulas
Having Unique Proofs
11:40 -  12:20  R. Blute, Proof Nets
and  Coherence Theorems

Lunch

Afternoon    free
Conference   Dinner


        Thursday  (September 5th)
9:30   - 10:30  E. Moggi, Invited  talk
10:30 -  11:00  Coffee / Tea Break
11:00  -  11:40 G. Jarzembski, Programs in Partials Algebras
- a  Categorical Approach
11:40  - 12:20  B. Jay, Tail Recursion
from  Universal  Invariants

Lunch

14:00  -  15:00 T. Coquand, Invited  talk
15:00  -  15:40 D. Pavlovic, Constructions and  Predicates
15:40  -  16:10 Coffee / Tea Break
16:10  -  16:50 B. Jacobs, E.  Moggi  & T.Streicher,  Relating
Models of Impredicative Type Theories
16:50  -  17:30 W.  Phoa, Set-theoretic Polymorphism after Robinson

        Friday  (September 6th)

 9:30  -  10:30 U.  Montanari, Invited  talk
10:30  -  11:00 Coffee / Tea Break
11:00   -  11:40 E. Stark,  Dataflow Networks are Fibrations
11:40  -  12:20 P. Degano,S. Kasangian  &  S.Vigna Applications
of the Calculus of Trees to Process Description Languages


Lunch


END  OF  CONFERENCE

==========================================
Subj:	Online bibliography for Information and Computation
From: dmjones@theory.lcs.mit.edu (David M. Jones)
Date: Tue, 13 Aug 91 21:13:57 EDT

A bibliography for the journal Information and Computation (formerly
Information and Control) covering the years 1982--present is now available
via anonymous ftp and mail server from theory.lcs.mit.edu (18.52.0.92).
The file is in BibTeX format and is in the file ftp/pub/meyer/iandc.bib.

To retrieve the file via ftp, connect to theory using "anonymous" as the
login name and "guest" as the password.

To retrieve the file via mail server, send a message to the address
archive-server@theory.lcs.mit.edu with the following line in the body:

        send meyer iandc.bib

An index of other files can be retrieved with the command

        send meyer Index

More information on the archive-server can be obtained by sending a
message with only the word "help" in the body.

David M. Jones
Editorial Assistant
Information and Computation
ic-request@theory.lcs.mit.edu

================================
Subj:	Logical Frameworks Workshop: Informal Proceedings
Date:        Wed, 14 Aug 91 15:54:07 ADT
From:       ccmj@dcs.ed.ac.uk

The informal proceedings of the 2nd Workshop on
Logical Frameworks (Edinburgh May 1991)
are now available by ftp.

To obtain the document by ftp use the
internet address 129.215.160.150
You should be connected to the machine 'cumbrae'
at Edinburgh. Use the login name 'anonymous'
(any password accepted), and the file name
 /export/bra/proc91.dvi.Z (file is compressed).

The contents include:

F. Barbanera, S.Berardi         Witness Extraction in Classical
                                   Logic through Normalization
D. A. Basin, R. L. Constable    Metalogical Frameworks
Y. Bertot                       A Canonical Calculus of Residuals
T. Coquand                      A semantics of evidence for
                                    classical arithmetic
R. Diaconescu, J. Goguen        Logical Support for Modularisation
     P. Stefaneas
G. Dowek                        A Complete Proof Synthesis Method
                                    for the Cube of Type Systems
A. Felty                        A Logic Program for Transforming Sequent
                                    Proofs to Natural Deduction Proofs
G. Huet                         A case study in Axiomatisation and Proof
                                    Development in the Coq Proof Assistant
C. Jones                        Completing the Rationals and Metric Spaces
                                    in LEGO
Y. Lafont                       Negation versus Implication
S. Matthews, A. Smaill          Experience with FS as a Framework
     D. Basin                       Theory
T. F. Melham                    A Mechanized Theory of the pi-calculus in
                                    HOL
D. Miller                       Unification of Simply Typed Lambda-Terms
                                    as Logic Programming
C. Murthy                       Finding the Answers in Classical Proofs:
                                    A Unifying Framework
T. Nipkow                       Order-Sorted Polymorphism in Isabelle
C. Phillips                     Well-founded Induction and Program
                                    Synthesis Using Proof Plans
D. Pym                          Towards an Algebraic Framework for
                                    Defining Sequential Logics
J. M. Smith                     An Interpretation of Kleene's Slash in
                                    Type Theory
N. Szasz                        A Machine Checked Proof that Ackermann's
                                    Function is not Primitive Recursive


Claire Jones
ccmj@dcs.ed.ac.uk

=====================================
Subj:	Free categories
Date:   Wed. Aug. 14
From: "P. B. Johnson" <PJOHNSON@Wesleyan.bitnet>

The underlying functor : cat ----> graph,
from small categories to small graphs, is tripleable.  I would like to
consider the same question over an arbitrary topos, and would appreciate
any hints from topos theorists.

It seems to me that, given a topos E,
the underlying functor: cat(E) ----> graph(E) is "equationally defineable",
that is to say, each internal category in E can be described by (in fact
finitary) operations on some object of graph(E), subject to some equations.
Then  cat(E) ----> graph(E) is tripleable if and only if it has a left
adjoint.  It seems that constructing free categories over graphs requires
some kind of countable colimits, which I don't imagine are always available.
Perhaps the existence of a natural numbers object (which seems to be in some
sense the most primordial of infinite colimits that a topos might possess)
ensures the existence of free categories.  Can such toposes with free
categories be characterized?  Thank you, Paul.

=================================
Date:        Wed, 14 Aug 91 15:54:29 ADT
Subj:   Online bibliography for TACS'91

A bibliography for the upcoming International Conference on Theoretical
Aspects of Computer Software (TACS'91) is now available via anonymous
ftp and mail server from theory.lcs.mit.edu (18.52.0.92).  The file is
in BibTeX format and is in the file ftp/pub/meyer/tacs91.bib.  Also
available are tacs91.tex and tacs91.ps, which are LaTeX and PostScript
versions of the file for those who prefer that format.

To retrieve the file via ftp, connect to theory using "anonymous" as the
login name and "guest" as the password.

To retrieve the file via mail server, send a message to the address
archive-server@theory.lcs.mit.edu with the following line in the body:

        send meyer tacs91.bib

An index of other files can be retrieved with the command

        send meyer Index

More information on the archive-server can be obtained by sending a
message to the archive-server with only the word "help" in the body.

David M. Jones
Secretary to Professor Albert R. Meyer

========================================
Subj:	Re: Logical Frameworks Workshop: Informal Proceedings
From: wald@theory.lcs.mit.edu (David Wald)
Date: Thu, 15 Aug 91 11:26:07 EDT

>Subject:    Logical Frameworks Workshop: Informal Proceedings
>From:       ccmj@dcs.ed.ac.uk
>
>The informal proceedings of the 2nd Workshop on Logical Frameworks
>(Edinburgh May 1991) are now available by ftp.

For readers who are closer to Massachusetts than to Edinburgh, the
proceedings are also available by anonymous ftp from theory.lcs.mit.edu,
in the file pub/lf/1991/proc91.dvi.Z (the file is compressed).

The file can also be retrieved from our archive server by sending the
line

     send lf 1991/proc91.dvi.Z

to archive-server@theory.lcs.mit.edu.  The file will be uuencoded and
shipped in pieces.  You can send the line "help" instead for further
information on using the archive-server.

-David Wald

=================================
Subj:	Re: free categories
Date:        Sat, 17 Aug 91 16:57:03 ADT

Two replies to Paul Johnson's question follow. I returned
from vacation today and take the opportunity to thank my colleague
Daniel Perron for minding the mailing list during this absence
and several others.

Bob Rosebrugh
+++++++++++++++++++++++++++++++++
From: David N Yetter <dyetter@magnus.acs.ohio-state.edu>
Date: Fri, 16 Aug 91 11:53:57 EDT


Re : Free categories

 Toposes with free categories are precisely toposes with NNO: in particular

TFAE:

     1) NNO

     2) the forgetful functor from the category of internal monoids is
tripleable

     3) the forgetful functor from the category of internal categories to
the category of internal graphs is triplable

The equivalence of 1) and 2) is Theorem 6.41 in Johnstone's Topos Theory.
That 3) implies 2) is immediate. That 1) implies 3) follows from the fact that
Finite Limit Theories (aka Essentially Algebraic Theories) have tripleable
categories of models over any topos with NNO (I don't recall a reference on
that last result, but I suspect it must be in Barr and Wells Toposes, Triples
and Theories).


Re: e-mail address

     As you can see from the header, my e-mail address is now

     dyetter@math.ksu.edu


Best Thoughts,
David Yetter
+++++++++++++++++++++++++++++++++++++++
Date:     Fri, 16 Aug 91 16:26:54 EDT
From:     "Andreas R. Blass" <USERGC4C@UMICHUB.BITNET>

This is in reply to Paul Johnson's question about constructing free
categories over graphs in elementary topoi (with natural numbers object).
Your own work on the indexed adjoint functor theorem is relevant to
this(see note from Bob R. below), as are the following:

B. Lesaffre, Structures algebriques dans les topos elementaires,
     C.R. Acad. Sci. Paris, 277 (1973) A663-666.

D. Schumacher, Absolutely free algebras in a topos containing an infinite
     object, Canad. Math. Bull. 19 (1976) 323-328.

Later, I wrote a paper (Words, free algebras, and coequalizers, Fund. Math.
117 (1983)117-160) showing that the usual set-theoretic existence proof
works in the internal logic of topoi.  (The emphasis there was on
varieties with infinitary operations, and things can be simplified in the
finitary case.)

Andreas Blass
++++++++++++++++++++++++
The article of mine Andreas refers to is:

On algebras defined by operations and equations in a topos,
JPAA 17(1980) 203-221

but David's reply answers the question completely ...

Bob Rosebrugh

========================================
Subj:	Query on initial algebras ...
Date: Mon, 19 Aug 91 08:43:49 EDT
From: barr@triples.math.mcgill.ca (Michael Barr)

Someone at the recent meeting in Durham mentioned that he had shown that
the canonical map from the intial algebra of some endofunctor on Set
to the terminal coalgebra was always monic.  Is that ``someone'' on the
distribution list and can he communicate with me.

Michael

==========================================
Subj:	Finite Limit Theories
Date: Sun, 18 Aug 91 20:09:22 -0400
From: cfw2@po.CWRU.Edu (Charles F. Wells)


David Yetter's comments concerning toposes with free categories

contains a misstatement.  It is not true that finite limit

theories have tripleable categories of models over any topos

with NNO.  For example, the category of small categories is not

regular, hence not tripleable over Sets for any underlying

functor (p. 120 of Triples, Toposes, and Theories).



--Charles Wells

=================================
Subj:	Partial morphisms in toposes
From: <jrk@information-systems.east-anglia.ac.uk>
Date: 23 Aug 91 16:15

What is known about partial morphisms in toposes?  A partial morphism
from A to B is a morphism from a subobject of A to B.  Composition needs
certain pullbacks to exist, which they do in a topos, so every topos has
a category of partial morphisms.  What is known about it?  E.g. it isn't
a topos, since its initial and terminal objects are the same.  Failing
that, does it have other nice properties, e.g. limits and colimits?

Johnstone's book touches on the subject in chapter 1: all partial
morphisms from A to B are representable by (ordinary) morphisms from A to
an object B~, and the mapping from B to B~ is a functor with a natural
transformation from the identity to that functor.  Monads seem about to
make an entrance (is there a product transformation from B~~ to B~?), but
he doesn't explore the matter any further.  Goldblatt's book and Fourman's
chapter in the Handbook of Mathematical Logic cover the same ground.

What else is known?

--
Richard Kennaway          SYS, University of East Anglia, Norwich, U.K.
Internet:  jrk@sys.uea.ac.uk            uucp:  ...mcsun!ukc!uea-sys!jrk

============================================
Subj:	latest update to CTCS
Date: Mon, 26 Aug 91 15:18:38 EDT
From: barr@triples.math.mcgill.ca (Michael Barr)

\documentstyle[12pt]{article}
\input diagram
\newcounter{lister}
\newenvironment{labeledlist}[1]
{\begin{list}{{\rm#1\arabic{lister}. }}{\usecounter{lister}
}}%begin text
{\end{list}}%
\def\blist#1{\begin{labeledlist}{#1}}
\def\elist{\end{labeledlist}}

\newcommand{\afour}{\oddsidemargin 18pt\evensidemargin 18pt
\textwidth 420pt\textheight 45\baselineskip\advance\textheight by \topskip}
%% Kludge to make article.sty width correct for A4
%% This works only for article.sty using the standard margin given

\textheight8in \headsep 0in \headheight0in \topmargin0in
\textwidth 6.5in \oddsidemargin0in
\mathchardef\Csc="0243
\mathchardef\Dsc="0244
\mathchardef\Esc="0245
\mathchardef\Gsc="0247
\mathchardef\Ssc="0253
\def\lncs#1{Lecture Notes in Computer Science {\bf#1}}
\def\springer{Sprin\-ger-Ver\-lag}
\def\mathrm#1{\expandafter\def\csname#1\endcsname{\mathop{\rm#1}\nolimits}}
\def\mathbf#1{\expandafter\def\csname#1\endcsname{\mathop{\rm\bf#1}\nolimits}}
\mathrm{id}
\mathrm{eval}
\mathrm{mult}
\mathrm{proj}
\mathbf{R}
\mathbf{Set}
\mathbf{Cat}
\mathbf{Mod}
\mathbf{Rel}
\mathrm{Hom}
\def\op{{}^{\rm op}}
\let\x=\times
\def\o{\mathop{\raise.3ex\hbox{$\scriptscriptstyle\circ$}}}
\mathcode`\<="4268 %left delimiter
\mathcode`\>="5269 %right delimiter
\def\inc{\subseteq}
\def\iso{\cong}
\def\[{[\kern-1.3pt [}
\def\]{]\kern-1.3pt ]}


\begin{document}

%\afour

\title{Category Theory for Computing Science: \\ Update}


\author{Michael Barr and Charles Wells}

\maketitle

We intend to maintain
our text, {\bf Category Theory for Computing Science}, Prentice Hall,
1990 (ISBN 0-13-120486-6),
% Our text, {\bf Category Theory for Computing Science}, Prentice Hall,
% 1990 (ISBN 0-13-120486-6) has just been published.
% We intend to maintain the text
in the sense that programmers maintain their programs,
by keeping a list of known errors and also of additions to the text that
we think might be useful.  (The latter will probably come in spurts as
we go to meetings and find out about wonderful new applications of
category theory to computing science.)

We will periodically
announce new errata and addenda on the category theory bulletin board.
The latest TeX version of the complete list is available by e-mail or
p-mail from either author.

The update consists of three parts: \ref{errors}: A list of errors discovered
so far.  \ref{newtext}: Additional examples, problems and pointers to the
literature. \ref{refs}: Additions and updates
to the list of references, pp. 417ff. of
the text.  Page references refer to the text.

Any further corrections or suggestions for additional text will be welcome.

{\footnotesize
\begin{center}\begin{tabular}{ll}
Michael Barr & Charles Wells \\
Department of Mathematics & Department of Mathematics \\
Burnside Hall & Case Western Reserve University \\
McGill University & University Circle \\
805 Sherbrooke St. West &  Cleveland, OH 44106-7058, USA \\
Montr\'eal, P. Q., Canada H3A 2K6 & cfw2@po.cwru.edu \\
barr@triples.math.mcgill.ca & \end{tabular}\end{center}
}
\newpage


\section{Errors}\label{errors}

\begin{description}

\item?p. xv? In the Chapter Dependency Chart, there should be a diagonal
line from Chapter 5 to Chapter 7.

\item?p. 23? (Jean-Pierre Marquis). SM--2 should read, ``If $m$,
$n\in S$, then $mn\in S$''.

\item?p. 31? (Jean-Pierre Marquis). S--1 should say
$\Dsc_0\inc\Csc_0$ and $\Dsc_1\inc\Csc_1$.

\item?p. 54? (Andrew Malton). Line 8: read ``$g \o h = f$'' for ``$h \o
g = f$''

\item?p. 56? (Han Yan). Line 7: $g:C\to C$ should be $g:B\to C$.

\item?p. 57? (Han Yan). Line 1: $f:A\to A$ should be $f:C\to A$.

\item?p. 57? (Han Yan). Line 2: $g:B\to C$ should be $g:B\to D$.

\item?p. 63? (Jean-Pierre Marquis). Last line: $TF(S)$ should
be $FT(S)$.

\item?p. 64? (Jean-Pierre Marquis). Definition 3.3.2, line 4:
$G(f)$ should be $F(g)$.

\item?p. 66? (Jean-Pierre Marquis). Section 3.3.10, line 2: ``is
to said'' should be ``is said''.

\item?p. 73? (Jean-Pierre Marquis). The reference to Wells ?1989?
should be deleted.

\item?p. 74? (Jean-Pierre Marquis). The reference to Wells ?1989?
should be to  Wells ?1990? (see updated reference
in Section~\ref{refs} of this document).

\item?p. 79?  Line 3: ``diagram'' should be capitalized.

\item?p. 79? (Al Vilcius). Line 7: replace ``$\id_i$'' by $\id_{D_i}$.

\item?p. 83? (Andrew Malton). Line --7: change ``of shape $U$'' to ``of
shape ${\cal U}$''.

\item?p. 87? (Al Vilcius).  In Theorem 4.2.20, line 2 replace ``$\Csc$''
by ``$\Gsc$'.  In the last line replace ``$\Mod(\Gsc,\Csc)$'' by
``$\Mod(\Gsc,\Dsc)$''.

\item?p. 90? (Andrew Malton). Line 5: change ``$f:  {\cal E}\to V{\cal
G}_1$'' to ``$f:  {\cal E} \to {\cal G}_1$''

\item?p. 92? In Proposition 4.3.12 and its proof, the letter $C$ (not
the script $\Csc$) is
used with two different meanings.  This can be corrected by changing $C$
to $S$ in the first line of the proposition, third line (first occurrence
only), fourth line (last occurrence only) and in the first line of the
proof (second occurrence only).

\item?p. 96? The reference to Seely should be ?1987? (the entry in the
list of references, p. 425, was incomplete and is updated in the
list of references below.)

\item?p. 101? (Jean-Pierre Marquis, Han Yan).
In the figure, $\Hom(f,C)$ should be
$\Hom(C,f)$.

\item?p. 102? ``The'' not ``the'' in line 7.

\item?p. 103? (Al Vilcius).  Change ``set'' to ``collection'' in the
second line of 4.6.2 and the sixth line of 4.6.3.  ?We are using
``collection'' as an informal synonym for ``class'', without getting
into set theory.?

\item?p. 103? Between the fourth and fifth lines of 4.6.3, add the following:
``We write $M:\Ssc\to\Csc$ for such a model.  This use of the same
symbol to denote both the sketch homomoprhism and the graph homomorphism
is a bit of notational overloading that in practice is always
disambiguated by context.''

\item?p. 105? The sentence before 4.6.9 has a misplaced parenthesis.  It
should read
``If you want a sketch for graphs which have a loop on every node, but not
a distinguished loop (so that a homomorphism takes the loop on $n$ to
some loop on $\alpha N(n)$, but it does not matter which one), you will
have to wait until we can study regular sketches in 9.4.5."

\item?p. 105? (Jean-Pierre Marquis). LT--1, second line: $a$
should be $f$.

\item?p. 108? (Al Vilcius).  Change ``set'' to ``collection'' in line 3
of 4.7.2.

\item?p. 137? (Jean-Pierre Marquis). Line 3 of proof of Theorem
5.5.5: $u_i\o s$ should be $s\o u_i$.

\item?p. 173? (Jean-Pierre Marquis). The second line of N--5
should be
$$f_1\x f_2\x\cdots\x f_n:a_1\x a_2\x\dots\x a_n\to
b_1\x b_2\x\cdots\x b_n$$
(no angle brackets around the arrow).

\item?p. 184? (Jean-Pierre Marquis). In the next to last line of
Example 7.7.3, ``sort $\tau$'' should be ``sort $\sigma$''.

\item?p. 186? (Jean-Pierre Marquis). Line 4 of Example 7.7.7:
``Let $u$ be the term $x$ of arity $\sigma$ and sort
`$\sigma$' '' should
be changed to
``Let $u$ be the term $x$ of arity `$\sigma$' and sort
$\sigma$''.

\item?p. 186? (Jean-Pierre Marquis). In line 8 of Example 7.7.7,
the path of $u$ is $\id:\sigma\to\sigma$.

\item?p. 190? (Nico Verwer).There is a series of errors in FE--5 to
FE--8.  The correct versions are as follows:
\blist{FE--}\setcounter{lister}{4}

\item$ + \o < {\id} , 0 \o <> > =
+ \o < 0 \o <> , {\id} > =
  \id : f \to f$

\item
$ * \o < j , {j} \o 1 \o <> > =
  * \o < {j} \o 1 \o <> , j > =
  j : u \to f$

\item
$ + \o {< \id , - >} =
  + \o {< - , \id >} =
  0 \o <> : f \to f$
\item
$ * \o (j \times j) \o {< \id , ()^{-1} >} =
  * \o (j \times j) \o {< ()^{-1} , \id >} =
  1 \o <> : u \to u$
\elist


\item?p. 208? (Al Vilcius).  Top diagram should have a $B$, not $C$ in
the SE corner.  The fourth line should say that $p_2$, not $p_1$ is the
pullback of $f$ along $g$.

\item?p. 227? (Jean-Pierre Marquis). Line 2 of Exercise 2 should
have $B_i$ for $B$ and $C_i$ for $C$.

\item?p. 228? (Al Vilcius). Last line:  Word ``be'' is missing.

\item?p. 232? (Jean-Pierre Marquis). The first line of the second
paragraph of section 9.1.5 has a font error (it is not
mathematically wrong): the second parenthesized expression
should read $(D,\mult_D,{\rm unit}_D)$

\item?p. 255? (Al Vilcius). Line --5:  Replace ``cleavage'' by
``opcleavage''.

\item?p. 256? (Al Vilcius). Line --8: the expression has misplaced
brackets.  Should be $$Fg?Ff(u)? \o\kappa(g,Ff(X))\o\kappa(f,X)$$

\item?p. 256? (Al Vilcius) Line --2 should be ``functors $\Csc\op\to\Cat$.''

\item?p. 258? (Al Vilcius).  Definition 11.2.3: GS--1 should be ``object
of $G_0(\Csc,F)$''.

\item?p. 259? (Al Vilcius). Line 8 should read ``$x'=Ff(x)$''.

In paragraph starting line 11, orientation of $G_0(\Csc,F)$ requires the
functor $G_0(F)$ to be the projection on the second coordinate, not
first.

\item?p. 261? (Al Vilcius).  In Theorem 11.2.9,  first projection should
be second as above.

\item?p. 263? (Jean-Pierre Marquis and Han Yan).
Line 15: Change ``then $F(C)$ and
$G(C)$'' to ``then $F(C)$ and $F(D)$''.

\item?p. 264? (Al Vilcius).  In Definition 11.3.4, FI--1, replace
``$P:\Esc\to\Cat$'' by ``$P:\Esc\to\Csc$''.

\item?p. 272? (Jean-Pierre Marquis). Line --4: The reference to
12.1.2 should be to 12.1.1.

\item?p. 281? (Jean-Pierre Marquis). In Exercise 1,
$f(S_0)\inc T_0$ should be $f_{*}(S_0)\inc T_0$.

\item?p. 287? (Jean-Pierre Marquis). The second line should read
$$\Hom_{\Csc/A}(u\x v,w) =\Hom_{\Csc/A}(\Sigma_u(u^*(v)),w)$$

\item?p. 302? Line --4ff should say, ``In particular, ${\rm\bf Cat}$
is enriched over ${\rm\bf Cat}$ itself, since its hom sets are
themselves categories (with the arrows as objects and the natural
transformations as arrows) and the hom functors preserve the extra
structure.''

\item?p. 303? (Jean-Pierre Marquis). In the second line of SP--4,
the $E$ should be $A$.

\item?p. 307? (Jean-Pierre Marquis). In line 5 of the second
paragraph, $(a_0, a_1, a_2, a_4\ldots)$ should be
$(a_0, a_1, a_2, a_3\ldots)$.

\item?p. 319? (Jean-Pierre Marquis). $G_0$ and $G$ in the diagram
should be $\Gsc_0$ and $\Gsc$.

\item?p. 331? (Jean-Pierre Marquis). Line 2:  ``That of (C)''
should be ``That of (c)''.

\item?p. 333? (Jean-Pierre Marquis).  In line 4 of the paragraph
after REAL--2, $\?fa_1=fa_2\?$ should be $\?\phi a_1=\phi
a_2\?$.

\item?p. 335? In the fourth paragraph of the discussion of the
internal category of modest sets, the sentence, ``We want to describe
this subset as consisting of those relations that are symmetric and
transitive'', should have the following phrase added:
``and double negation closed''.

\item?p. 345? Line 2 of the answer to exercise 12.a: the last letter
should be ``B'', not ``b''.

\item?p. 357? (Jean-Pierre Marquis) In the top diagram, one of
the arrows from BOOLEAN to BOOLEAN should be reversed.

\item?p. 358? (Jean-Pierre Marquis) In the answer to Exercise 5,
delete the phrase ``$\beta$ satisfies''.

\item?p. 365? In the answer to problem 8, $\beta C:\Hom(C,C)\to F(C)$.

\item?p. 368? (Jean-Pierre Marquis) In the second line of the
answer to Exercise 3, the $B$'s should be $C$'s.

\item?p. 370? (Jean-Pierre Marquis) Line --2:  Both occurrences
of $f$ should be $F$.

\item?p. 372? (Jean-Pierre Marquis) In the answer to Exercise 1,
the arguments to $f$ are reversed.  The end of the sentence
should read:
``$\ldots$by letting $f(b,0)=f_0(b)$ and having
defined $f(b,i)$ for $i\le n$, define $f(b,n+1)=t(f(b,n))$''.

\item?p. 373? (Jean-Pierre Marquis) In the answer to Exercise 1
of Section 6.1, every occurrence of $(\lambda\o\eval)$ should be
$\lambda(\eval)$.

\item?p. 380? (Jean-Pierre Marquis) In the diagram in the answer
to Exercise 2, the upper right arrow (labeled $<\id,e\o<>>$)
should go in the opposite direction.

\item?p. 381? (Jean-Pierre Marquis) The answer  to number 3 is
confused.  Here is the entire answer rewritten:
We give the answer for the case of real vector spaces; the other is
similar.  We assume the real number field $\R$ as a given structure.  We
suppose, for each $r\in R$, a unary operation we will denote $r^*:s\to
s$.   We require a unit element $z:1\to s$ for the operation $c$
and a diagram similar to the previous exercise to say that $z$ is the
unit element.   The following diagram says that $c$ is
commutative:
$$
\Atriangle?s\x s`s\x s`s;<\proj_2,\proj_1>`c`c?
$$
We have to add a unary negation operator $n:s\to s$ together with a
diagram to say it is the negation operator:
$$\bfig
\setsqparms?0`1`1`1;1500`500?
\putsquare(0,0)?s`s\x s`1`s;`<>`c`z?
\putmorphism(0,500)(1,0)?\phantom{s}`s\x s`<\id,\id>?{750}1a
\putmorphism(750,500)(1,0)?\phantom{s\x s}`\phantom{s\x s}`\id\x
n?{750}1a
\efig$$
In addition, we need diagrams that express the following identities:
\begin{eqnarray*}
0^*(x)&=&z\\
r^*(c(x,y))&=&c(r^*(x),r^*(y))\\
(r+s)^*(x)&=&c(r^*(x),s^*(x))\\
1^*(x)&=&x\\
r^*(s^*(x))&=&(rs)^*(x)
\end{eqnarray*}
We give, for example,
the diagram required to express the third of the equations above:
$$
\settriparms?1`1`1;600?
\qtriangle?s`s\x s`s;<r^*,s^*>`(r+s)^*`c?
$$

\item?p. 386? (Jean-Pierre Marquis) Line 4 of answer to 3b:
$D_m$ should be $Dm$.

\item?p. 402? (Jean-Pierre Marquis). The answer to Exercise 6 of
12.2 (page 281) uses Theorem 12.3.6, which comes in a later
section.  Here is an answer using only the definition of
adjoint:  If the functor defined in 12.2.4 has a left adjoint
$F$, then by definition of left adjoint there is for any set $X$
an arrow $\eta X:X\to FX\x A$ with the property that for any
function $f:X\to Y\x A$ there is a unique function $g:FX\to Y$
for which $(g\x A)\o \eta X=f$.  Now take $Y=1$, the terminal
object (any one element set).  There is only one function
$g:FX\to 1$, so there can be only one function $f:X\to 1\x A\iso
A$.  If $A$ has more than one element, this is a contradiction.

\item?p. 431? The word ``relation'' should also be indexed on p. 21.

\end{description}

\section{Additional text}\label{newtext}

\begin{description}

\item?p. xiii? (First paragraph).  Another book that develops
most of the topics further, except sketches, is ?Freyd-Scedrov,
1990?.  (Additional comment).  The reader may find the following
discussions of the uses of category theory in computing science
useful:  The tutorials in ?Pitt, Abramsky, Poign\'e and
Rydeheard, 1986?, and ?Goguen, 1991?.

\item?p. xiii? (Second paragraph).Another collection of papers is
?Pitt, Rydeheard, Dybjer, Pitts and Poign\'e, 1989?.

\item?p. 17? ?Additional example of category.?
Let $\alpha$ be a relation from a set $A$ to a set $B$
and $\beta$ a relation\index{relation}
from $B$ to $C$ (see 1.3.4).  The {\bf
composite} $\beta\o\alpha$ is the relation from $A$ to $C$ defined
as follows: If $x\in A$ and $z\in C$, $(x,z)\in\beta\o\alpha$ if and
only if there is an element $y\in B$ for which $(x,y)\in\alpha$ and
$(y,z)\in\beta$.  With this definition of composition, the {\bf
category of sets and relations} has sets as objects and relations
as arrows.

\item?p. 53? Add to third paragraph of 3.1.7:  Freyd-Scedrov
?1990?, pages 9 and 19, give a formal definition of forgetful functor.

\item?p. 71? ?New exercise? Show that the category of sets and relations
is equivalent, in fact isomorphic, to its own dual (see 2.6.7).
Answer: Let $\Rel$ denote the category of sets and relations.
For a relation $\alpha$ from $A$ to $B$, that is, a subset of
$A\x B$, let $\alpha\op$ denote the subset $\{(b,a)\mid (a,b)\in A\x B\}$
of $B\x A$.
Let $F:\Rel\to\Rel\op$ be the identity on objects and
for a relation $\alpha:A\to B$,
let $F(\alpha)=\alpha\op$.  $F(\alpha)$ is a relation from $B$ to
$A$ in $\Rel$, hence a relation from $F(A)=A$ to $F(B)=B$ in $\Rel\op$.
It is easy to check that if $\beta:B\to C$, then $F(\beta\o\alpha)=
\alpha\op\o\beta\op$ in $\Rel$, so $(\beta\o\alpha)\op=\beta\op\o\alpha\op$
in $\Rel\op$.  This says $F(\beta\o\alpha)=F(\beta)\o F(\alpha)$, so
$F$ preserves composition.  The identity relation on $A$ is $\Delta_A=
\{(a,a)\mid a\in A\}$, so $\Delta=\Delta\op$ and $F$ preserves
identities.  Since for any relation $\alpha$, $(\alpha\op)\op=\alpha$,
we have $F\o F$ is the identity functor on $\Rel$, so is its own inverse.
Hence  $F$ is an isomorphism.  By Exercise 1, it is therefore an
equivalence of categories.

\item?p. 96?
The applications of 2-categories have mushroomed and include
?Ji-Feng and Hoare, 1990?, ?Moggi, 1989? and ?Power, 1989? in
addition to the papers already listed.

\item?p. 97? Second paragraph of Section 4.5:  In addition to generalizing
the Cayley Theorem, the Yoneda Lemma also has as a special case the
embedding of a poset into its down-closed subsets.
Also: set-valued functors are studied further in Sections 11.2 and 14.4.

\item?p. 158? The assumption that every object in a cartesian
closed category has fixed points is inconsistent with other
desirable assumptions on the category.  See ?Huwig-Poign\'e,
1990?.

\item?p. 213? Freyd-Scedrov ?1990? have a different but closely
related definition of ``regular''.  If a category is regular in
our sense it is regular in theirs, and if it is regular in their
sense and has coequalizers, then it is regular in our sense.

\item?p. 257? Besides ?Coquand, 1988?, Moggi ?1989? also uses
the Grothendieck construction in modeling polymorphism.

\item?p. 283? Another reference for the Adjoint Functor Theorem
(with a different point of view) is ?Freyd-Scedrov, 1990?, pages
144-146.

\item?p. 287? Just before the exercise: See also ?Ehrhard, 1989?.

\item?p. 301? Some applications of triples (monads) in computing
science are in ?Moggi, 1991?, ?Power, 1990?

\item?p. 318? Add comment: We considered presheaves as actions in Section
3.2.  They occur in other guises in the categorical and computer science
literature, too.  For example,
a functor $F:A\to\Set$, where $A$ is a set treated as a
discrete category, is
a ``bag'' of elements of $A$.  If $a\in A$, the set $F(a)$ denotes the
multiplicity to which $a$ occurs in $A$.  See ?Taylor, 1989? for
an application in computing science.

\item?p. 325? Goguen ?1990? has developed a sheaf semantics for object
oriented programs.

\end{description}

\section{Additional references}\label{refs}
\fontdimen2\twlrm=4.3pt% space instead of 3.91663
\fontdimen3\twlrm=4.2pt%stretch instead of 1.95831
\fontdimen4\twlrm=1.7pt%shrink instead of 1.30554
\begin{list}{}{\leftmargin 8mm \itemindent -8mm
\parsep 0pt \itemsep 0pt plus 1pt}
\def\itm{\item??}

\itm \mbox{T.  Ehrhard}, {\it Dictoses}.  In {\bf Category theory and
computer science}, D. H. Pitt, D. E. Rydeheard, P. Dybjer, A. M. Pitts
and A. Poign\'e, editors.  \lncs{389}, \springer, 1989.

\itm \mbox{P. Freyd and A. Scedrov}, {\bf Categories,
Allegories}.  North-Holland Mathematical Library {\bf39},
North-Holland, 1990.

\itm \mbox{J.\ Goguen}, {\it Semantics of concurrent interacting
objects}.  Preprint, Programming Research Group, Computing Laboratory,
Oxford University, Oxford OX1 3QD, England.

\itm \mbox{J. Goguen}, {\it A categorical manifesto}.
Mathematical Structures in Computer Science {\bf 1}, 1991,
49--68.

\itm \mbox{C.\ A.\ R.\ Hoare}, He Jifeng and C. Martin, {\it
Pre-adjunctions in order-enriched categories}.  Preprint, Programming
Research Group, Computing Laboratory, Oxford University, Oxford OX1 3QD,
England.

\itm \mbox{He Ji-Feng and C. A. R. Hoare},
{\it Categorical semantics for programming languages}.
In M.\ Main {\it et al.}, eds., {\bf Mathematical
Foundations of Programming Semantics}. \lncs{442},
\springer,  1990, 402--417.

\itm\mbox{H. Huwig} and A. Poign\'e, {\it A note on
inconsistencies caused by fixpoints in a cartesian closed
category}.  Theoretical Computer Science {\bf73}, 1990,
101--112.

\itm \mbox{E.  Moggi}, {\it A category-theoretic account of program
modules}.
Mathematical Structures in Computer Science {\bf 1}, 1991,
103--139.
% In {\bf Category theory and computer science}, D. H. Pitt, D.
% E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors.
% \lncs{389}, \springer, 1989.

\itm \mbox{D.\ Pitt}, D. Rydeheard, P. Dybjer, A. Pitts and A. Poign\'e,
eds.  {\bf Category theory and computer science}.  \lncs{389},
\springer, 1989.

\itm \mbox{A.\ J.\ Power}, {\it An abstract formulation for rewrite
systems}.  In {\bf Category theory and computer science}, D. H. Pitt, D.
E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors.
\lncs{389}, \springer, 1989.

\itm \mbox{A. J. Power},
{\it An algebraic formulation for data refinement}.
In M.\ Main {\it et al.}, eds., {\bf Mathematical
Foundations of Programming Semantics}. \lncs{442},
\springer,  1990, 390--401.

\itm \mbox{R.\ Seely}, {\it Modelling computations:  a $2$-categorical
framework.} In {\bf Proceedings of the Conference on Logic in Computer
Science}, IEEE, 1987.  ?Corrected reference?.

\itm \mbox{P.\ Taylor}, {\it Quantitative domains, groupoids and linear
logic}.  In {\bf Category theory and computer science}, D. H. Pitt, D.
E. Rydeheard, P. Dybjer, A. M. Pitts and A. Poign\'e, editors.
\lncs{389}, \springer, 1989.

\item \mbox{C.\ Wells}, {\it A generalization of the concept of
sketch}.  Theoretical Computer Science {\bf 70} (1990), 159-178.
?Updated reference?.
\pagebreak?3?

\end{list}

\end{document}
=============================
Subj:	Online bibliography for Symposium on Logic in Computer Science
Date: Mon, 26 Aug 91 15:21:36 EDT
From: dmjones@theory.lcs.mit.edu (David M. Jones)

An online bibliography for the Annual IEEE Symposium on Logic in
Computer Science is now available via anonymous ftp and mail server
from theory.lcs.mit.edu (18.52.0.92).  The bibliography is in BibTeX
format and is in the file pub/meyer/lics.bib.

To retrieve the file via ftp, connect to theory using "anonymous" as
the login name and "guest" as the password.

To retrieve the file via mail server, send a message to the address
archive-server@theory.lcs.mit.edu with the following line in the body:

        send meyer lics.bib

An index of other available files can be retrieved with the command

        send meyer Index

More information on the archive-server can be obtained by sending a
message with only the word "help" in the body.

David M. Jones
Secretary to Professor Albert R. Meyer, General Chair, LICS

===============================
Subj:	Re:  Partial morphisms in toposes
Date: Wed, 28 Aug 91 10:55:43 +0200
From: Thomas Streicher <streiche@unipas.fmi.uni-passau.de>

The subject of partial morphisms in a topos has been dealt with extensively
in Adam Obtulowicz's Theses which has appeared in Dissertationes Mathematicae.
He gives an essentially algebraic definition of what is a category of partial
maps in a topos.

There is a lot of work on categories of partial maps :

Robinson & Rosolini   (in Inform. & Comp.)

Curien & Obtulowicz   (also in Inf. & Comp )

Carboni   (Cahiers de Topologie et Geometrie Differentielle)

the Theses of Rosolini and Moggi

etc.



If you are interested not in arbitrary partial maps but in those whose domain of
definition is semidecidable you must work with so called dominions.
This is a class of subobjects of a topos which contains all iso, is closed under
composition and stable under pullpacks along arbitrary maps.


The notion of dominion already appears in Rosolini's Thesis.

Most prominently it also has been explained by Alex Heller in his paper
'Dominical Categories'  which has appeared in J.S.L.

Recently Barry Jay has been working on categories of partial maps from the point
of view of order enriched categories. I think there are some Edinburgh LFCS repo
rts on that.

Thomas Streicher

========================
Subj:	Re: Finite Limit Theories
Date: 27 Aug 91 14:02
From: Steven John Vickers <sjv@doc.imperial.ac.uk>

To try to clarify the remarks of David Yetter and Charles Wells on essentially
algebraic theories, let me pass on an extract from the paper "Preframe
Presentations Present" which I recently wrote with Peter Johstone (for "CT
'90", to appear in Springer Lecture Notes in Mathematics). I ought to say that
the section from which this extract is taken, which was intended to be a brief
yet helpful account of essentially algebraic theories, is a distillation of
Peter's knowledge rather than mine.

  "For a small essentially algebraic theory T, the forgetful functor from
T-models to Set (or Set^n if T is many-sorted) has a left adjoint, just as in
the algebraic case: the free T-model on a set X is constructed in the usual way
as the set of words (i.e. terms) in the elements of X, modulo T-provable
equality. The adjunction will not be monadic unless T is algebraic, but it will
be possible to factor it as a tower of monadic adjunctions in the style of
MacDonald and Stone ("The tower and regular decomposition", pp. 197-213 in
Cahiers Top. Geom. Diff 23 (1982))."

I presume, again without being an expert in these fields, that for finitary
theories this all works over arbitrary elementary toposes with NNO.

Steve Vickers
