Galchin Vasili <vngalchin@yahoo.com> asked:
I would like to know if anybody is doing research on applying category theory to hereditarily-finite sets, e.g. where an object is a hereditarily set with some kind of structure to it and morphism that preserves that structure.
Obviously, the subcategory of SET where objects are just hered. finite sets and morphisms are functions between hered. finite sets is not "interesting". Also, the case where an object is a hered. set together with an endomorphism doesn't sound "interesting".
I take it that you want to capture the WELL FOUNDED ELEMENT RELATION, and also the SUBSET RELATION, from set theory. You may be interested in 1. Gerhard Osius, "Categorical set theory: a characterisation of the category of sets", Journal of Pure and Applied Algebra 4 (1974) 79--119. 2. Peter Johnstone, "Topos Theory", Cambridge University Press, 1977, of which chapter 9 has a summary of Osius's work. 3. Andre Joyal & Ieke Moerdijk, "Algebraic Set Theory", LMS Lecture Notes 220, Cambridge University Press, 1995. 4. Paul Taylor, "Intuitionistic Sets and Ordinals", Journal of Symbolic Logic, 61 (1996) 705--744. 5. Paul Taylor, "Practical Foundations of Mathematics", Cambridge University Press, 1999, especially Sections 6.3, 6.7 and 9.5. http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations Gerhard Osius's work was significant in 1974 as one of the ways in which it was shown that toposes do the same thing as set theory. In fact Osius's is, so far as I am aware, the only 1970s work that discusses *set* theory - Benabou, Joyal, Lawvere, Mitchell etc showed that toposes do the same thing as some form of *type* theory. Of course, it is the latter that mathematicians actually use when they claim to be using set theory as foundations. (See Section 2.2 of my book for a type-theoretic formulation of set theory as mathematicians actually use it.) Joyal and Moerdijk treat a model of set theory as a free algebra (within some larger world) for singleton and unions of specified size. If you are specifically interested in "finiteness" rather than the hereditary aspects in general, this might be the structure that you want (page 88). My JSL paper develops the notions of "transitive set" and "ordinal" in the sense of a carrier equipped with a binary relation with particular properties. Its style is therefore like order theory or other "ordinary" mathematics, since it attributes no ontological significance to the relation. It gives a version of Mostowski's theorem, in which the extensional quotient of a well founded relation is constructed as the quotient by an equivalent relation, and not (as you will find the in the set theory textbooks) using Replacement. In both Joyal--Moerdijk and my work, it is shown that *several* qualitatively different notions of ordinal arise intuitionistically. What remains of considerable interest (once we have agreed that set theory is wrong, wrong, wrong) is Osius's categorical notion of recursion. The equation f(x) = r( { f(y) | y in [=element_of] x } ) he writes as the (3=1, not 2=2) commutative square P(f) { y | y in x } P(X) ---------> P(A) ^ ^ | | | | | | | | | | r | | | | | | - | f v x X -------------> A which we may of course generalise to a "homomorphism" from any P-coalgebra to any P-algebra, where indeed P may be any functor instead of the covariant powerset functor. The coalgebra admits recursion by definition if there is exactly one such "homomorphism" to any algebra whatever. Osius showed that coalgebra homomorphisms, P(h) P(A) --------> P(B) | | | | | r | s | | | | v v A -----------> B capture the set-theoretic inclusion relation A<B. The exercises in Chapter VI of my book explore applications of the commutative square to recursive functional programs. In particular, a categorical treatment is given for the idea of an "accumulator" that functional programmers use to write tail-recursive list programs. Osius's 3+1 square is about RECURSION - defining functions or programs - but I have also considered INDUCTION - proving theorems - categorically. Again this is a property of coalgebras. P(m) P(U) >------------------------> P(A) ^ | | | | | r | ----| | | | | | | m v H >---------> U >----------> A Suppose that, for any mono m, if the above diagram is a pullback, then m is in fact an isomorphism. The we say that r:PA->A is a WELL FOUNDED COALGEBRA. Sections 6.3 and 6.7 of the book give a sketch of the theory of well founded coalgebras, and the final section (9.5) shows how this categorical notion of ordinal can be used to define transfinite iterates of a functor (for example, internally in a topos) I have a long unfinished paper containing all of the details about well founded coalgebras. This shows how the various intuitionistic notions of ordinal (plus some new ones!) arise from considering the "lower sets" functor on Pos instead of the covariant powerset on Set. Besides the functor P and the underlying category, we can vary the class of maps that we call "monos". In its role in the above "broken pullback" diagram, this controls the logical strength of the induction scheme, ie the number of quantifiers that we allow in the definition of the predicates for which induction is applicable. However, for characterising the ordinals, the interesting variability is in the class of "monos" used to define EXTENSIONALITY. The full subcategory of extensional coalgebras (those for which r:PA >--> A is "mono") is closed under arbitrary limits in the category of well founded coalgebras and coalgebra homomorphisms. However, depending on the particular situation, we need the axiom of REPLACEMENT to construct the reflection (left adjoint to the inclusion). One day, I hope to use this to explore this frighteningly strong set theoretical principle categorically. Paul Taylor pt@di.unito.it www.di.unito.it/~pt PS I'm afraid this stuff took a back seat to Abstract Stone Duality.