discussion on Replacement at CT08

discussion on Replacement at CT08

[Paul Taylor]

A couple of months ago, there was a discussion in this forum about
categorical formulations of the Axiom-Scheme of Replacement.

 From this, no fewer than four approaches emerged, as follows:

(1) Steve Awodey considered Algebraic Set Theory
(2) Colin McLarty considered an Elementary Theory of the
     Category of Sets
(3) Thomas Streicher considered Universes
(4) I (Paul Taylor) considered iterations of a functor
     indexed by a well founded coalgebra.

(I was going to write a one-paragraph summary of each of these,
but decided that the risk of error was too great.)

Following the public discussion, the four of us, together with
Mike Shulman, who had raised the question in the first place,
continued it in private for a while.   What I wanted to achieve
from this was some agreement on a metalanguage for the classes
(such as a Heyting pretopos) and a statement of each formulation
within this metalanguage.  Then someone (else) could compare the
definitions, and ask to what extent they are equivalent.  (I don't
want to re-open the substantive discussion at the moment,  but
I should point out that the objective of my formulation was to
avoid the need for such a metalanguage, although this is needed
to compare my view with the others.)

We didn't manage to do this, but the five of us adjourned our
discussion, with an agreement to re-open it later.  One possibility
is the Category Theory meeting in Calais next month,  and I suggested
to the Programme Committee that they might set aside a room for a
parallel session devoted to this topic.   In their response,
they seem to have interpreted the proposal in a rather more formal
way than we had intended.  Also, it turns out that, of the five,
only Steve and I will be present.

So, to get to the point, Steve and I invite anyone who would like
to take part in a discussion (of whatever degree of formality) about
Replacement during the course of the conference to contact us
privately,  so that we can make arrangements with the programme
committee.

Paul Taylor  pt08@PaulTaylor.EU
Steve Awodey awodey@cmu.edu