Re: no membership-respecting morphisms

["V. Schmitt" <vs27@mcs.le.ac.uk>]

Paul Taylor wrote:

>Mike Barr quoted a "thought of Chairman Pratt" that was attributed to him,
>
>
>
>>Monotone functions respect order, group homomorphisms respect the
>>group operation, linear transformations respect linear combinations,
>>and gangsters respect membership in the Cosa Nostra, but what
>>morphism has ever respected membership in a set? It is sheer hubris
>>for a relation that can't get no respect to claim to support all of
>>mathematics.  (Old argument of category theorist Mike Barr, new
>>polemics.)
>>
>>
>
>and commented on it,
>
>
>
>>That is not a bad rendition (save for the reference to Cosa Nostra)
>>of what I actually said which was that we create these elaborate
>>structures of well-founded trees subject to the rule that two
>>chidren of the same leaf cannot be isomorphic.  But then, unlike all
>>other structures that we build, we make no hypothesis that functions
>>preserve the structure.  Indeed, I think a structure-preserving map
>>must be the inclusion of a subset.  And there are no non-identity
>>endomorphisms.
>>
>>
>
>
>Of course, I entirely agree with the sentiment that epsilon-structures
>are completely inappropriate as a basis of most ordinary mathematics.
>
>However, mathematics and mathematicians are contrAry beasts, who
>treat any statement of the form "there is no such thing as ..." as a
>challenge, whether it be about membership-preserving functions or the
>square root of -1.
>
>Indeed, it's quite interesting to look at "carriers equipped with
>membership relations" in the same way as "carries equipped with group
>multiplications".  This is what I did in my paper "Intuitionistic
>Sets and Ordinals", JSL 61 (1996).
>
>For a more categorical treatment, we may regard the relation as a
>coalgebra structure for the full covariant powerset functor.  This is
>what Gerhard Osius did in his "Categorical Set Theory" in JPAA 4
>(1974) and what I did for other functors in my unpublished paper
>"Towards a Uniform Treatment of Induction - the General Recusion
>Theorem" in 1995-6.  (This was presented at "Category Theory 1995"
>in Cambridge and part of it appeared in Section 6.3 of my book.)
>
>As Mike Barr says, and Gerhard Osius proved in his paper, for
>"extensional" structures ("well-founded trees subject to the rule that
>two > chidren of the same leaf cannot be isomorphic"), the
>structure-preserving map must be a subset inclusion.
>
>However, without extensionality, it is a COALGEBRA HOMOMORPHISM.
>
>Well founded coalgebras behave like fragments of the initial algebra
>(the von Neumann hierarchy, in the case of the powerset functor), so
>their rigidity (lack of endomorphisms) is related to the uniqueness of
>homorphisms out of the initial algebra. The sense in which coalgebra
>homomorphisms are like partial algebra homomorphisms is explored in
>the early sections of my unpublished paper.
>
>Osius's recursion scheme has attracted some attention in recent years
>amongst functional programmers as a way of describing recursive
>programs.  See "Recursive Coalgebras from Comonads" by Venanzio
>Capretta, Tarmo Uustalu and Varmo Vene, in "Information and
>Computation" 2006.  In fact, the description also works for
>imperative programs - see Section 2.5 of my book.
>
>I have a longer survey of this subject that I intend to publish on
>"categories" later this month.
>
>
>MY WEB PAGES AT   www.cs.man.ac.uk/~pt
>
>While I'm here, I'd like to draw your attention to some new things
>that I have put on my web pages recently.
>
> * The slides that I have used at recent conferences and seminars.
>
> * The unpublished paper and scanned transparencies of 1995-6 talks
>   on well founded coalgebras.
>
> * A new web page for my book, "Practical Foundations of Mathematics",
>   including where to buy it, errata, who has used or cited it, etc.
>   If you have used it in a lecture or seminar series, please send
>   me a URL and your experiences.
>
> * The full text of Jean-Yves Girard's "Proofs and Types".
>
> * A new version of my TeX package for "commutative diagrams", together
>   with an explanation of the "PostScript" mode, why the "pure DVI"
>   mode is strongly deprecated (NB those long-standing users who have
>   spoiled their otherwise excellent books, papers and online journals
>   by using it), and how to overcome its uglier features if you really
>   insist on using it.
>
> * A collection of other TeX macros.
>
> * Scanned manuscripts of my 1983 Cambridge Part III Essay (= MSc thesis)
>   (see "domain theory") and undergraduate algebra lecture notes.
>
>
>Paul Taylor
>
>
>
>
Dear Paul, as far as i remember model theorists have
an extremely elegant way of comparing structures:
no morphisms there but "games" of finite isomorphism
extensions (see Fraisse' and Ehrenfeucht for the game
aspect or B.Poizat's book)
All the first order syntax is subsumed by those games.
I quite like categories and for sure I do not know everything,
but I have not seen so far a convincing categorical counterpart
for these games.
(And model theory is good stuff!)

Best,
Vincent.