categorical formulations of Replacement

[Paul Taylor <pt08@PaulTaylor.EU>]

Dear Thomas,

I'm glad that we've now started to talk a common language about
Replacement, and am hopeful that it will be possible to come to
some agreement, but I think that we are still some way off doing so.

Since you have changed the Subject: line several times, I would like
first to give some help to anyone who might be trying to follow this
discussion from an archive in the future, by listing the Subject:
lines of recent postings.  Of course, they have "categories:" and
"re:" added to them.

  Categorial foundations
  categorical formulations of Replacement
  Heyting algebras and Wikipedia
  I was partly wrong
  internal versus external
  question to Colin about uniqueness in his Replacement axiom
  replacement and iterated powersets
  replacement and the gluing construction
  replacing set theory
  the axiom scheme of replacement in category theory
  trying to answer some of Paul's questions

When I was trying to understand replacement, ten years ago and more,
I found, both from my own experience and in looking that the work of
others, that it is easy to fall into one of two traps:

(1) lack of rigour;  using the words "external" or "meta-language" may
indicate this;

(2) lack of force;  using the word "definable" may indicate this.

You can talk rigorously about external or meta- things if you first set
up a two-level formal system.  Examples of such systems include
(1) first order logic and set theory expressed within it;
(2) first order logic and category theory expressed within it;
(3) a category with an internal category;
(4) a fibred category containing a universe in the sense that
     you and I discussed in the 1980s;
(5) a pretopos or arithmetic universe with a class of small maps
     (algebraic set theory).

A large part of the explanation for ideological conflicts between
mathematicians is that they work in different OUTER systems.  If
they can agree on the outer system, they have an arena in which to
compare their INNER systems.  Reading between the lines of your
posting suggests that you are not completely confident yourself
of the rigour of your own account.

One of the uses of a two-level system is to discuss logical questions
such a consistency.  For example, Godel's theorem is about truth and
provability, which may be seen as facts about the outer and inner
systems
respectively.  Andre' Joyal set this up in category theory by looking
at the free arithmetic universe inside an arithmetic universe.

The axiom-scheme of replacement seems to be about making the inner world
agree with part of the outer one.

I really do not have much idea of what you mean by statements like
       \forall n:N \exists i : X_{n+1} -> P(X_n)  Iso(i).
Nor do I understand similar statements to this in either
"An elementary theory of the category of sets (extended version)"
or "Exploring categorical structuralism"
by Bill Lawvere and Colin McLarty respectively.

It would help if you were all to give more "turorial" explanations of
these things, and precise internal references to relevant papers and
books, because these are often lengthy and largely devoted to simpler
categorical structure than replacement.

We agree, I believe, that fibred methods are they way that we can
express
in category theory ideas that the set theorists encode as sets of sets.
Thus a display map  p:X-->N  captures the same idea as
   { {{x, {x, n}}  |  x in X & p(x)=n } | n in N },
or whatever hieroglyphics the set theorists would use.

Similarly,  the idea of a functor from a small category to a large one,
say  F:CC-->Set,  can be captured as a discrete fibration   p:FF-->CC.

In order to have any chance of fitting the axiom scheme of replacement
into our skulls,  we have to take the technology (fibred category
theory,
for example) as read,  even though it is rather difficult and
complicated
itself.   The problem is that most accounts add replacement as a brief
footnote to a lengthy treatment of more basic topics.   My book is
guilty of this, and so, with all due respect, are you, I believe.

With regard to the example of the iterated powerset,  the statement of
yours that I quoted above claims to express this,  but I do not
understand the language.  I would like you to translate it into the
usual language of category theory, ie functors, pullbacks etc.

I suspect that what you will come up with is the same as in my posting
about this on Sunday afternoon.   I accept that I have taken the
technology of fibred category theory off the shelf to do this, but

*********************************************************************
*  I believe that I made a significant original contribution        *
*  (in my book) by formulating the equation X_{n+1} = P(X_n) as     *
*  a pullback along the structure map of a well founded coalegbra.  *
*********************************************************************

The example of the gluing construction illustrates the difficulty caused
by treating replacment as a footnote to a more elementary theory.
There is, as you say, no foundational difficulty in constructing the
comma category arising from a functor  U:AA-->SS.   Although I have
copied most of what I have to say about replacement in Section 9.6
of the book in these postings, I am not going to do so for my account
of the gluing construction, as it is mathematically too complicated
to do so. You will have to get the book itself and read section 7.7.

The foundational issue about this construction is its application to
consistency issues of various theories.   In these,  SS  is a "semantic"
model of the theory in question, maybe the universe "Set" in which we
claim to live,  and  AA  is the "syntactic" or "term" model.

We have to be careful about calling AA the "free" or "initial" model,
as this is exactly the foundational point.

The gluing construction is the comma category (SS,U) whose objects are
SS-maps of the form  X-->U(Gamma),  where Gamma is an object of AA and
X one of SS.   I use the letter Gamma because it is typically a context
of the theory under study.   One can show that  (U,SS)  typically
inherits the structure of this theory, and pi_1:(SS,U)-->AA preserves
it.

Since  (U,SS)  is a model of the theory,  whilst  AA is the term model,
there ought to be an interpretation functor   [[-]]:AA-->(U,SS).
We have no difficulty in saying what such a functor would be in
substance, since we can express it as a fibration  EE-->AA of small
categories.   However, this illustates the difficulty with the
word "definable" - if you already had this fibration then there
would be nothing left for Replacment to do.

The problem is whether the functor or fibration exists.   Now, as AA
is the term model, we can use recursion over its well founded system
of types, terms and proofs. For example,  if we already know  [[Gamma]]
and [[Delta]],  we can form the interpretation of the arrow type
Gamma -> Delta as the exponential
    [[ Gamma -> Delta ]]   =   [[Delta]] ^ [[Gamma]].

However, this is not a valid form of recursion, since recursion defines
new TERMS of pre-existing types.   We want to form new TYPES.  This
involves the axiom scheme of replacement.

******************************************************************
*  Again, I claim an original contribution in my book in         *
*  recognising that this application of the gluing construction  *
*  to logic requires the axiom scheme of replacement.            *
******************************************************************

Notice that replacement is not only a scheme indexed by types,  it is
also parametric in the theory under study:   each theory has its own
replacement scheme.   If the original theory was algebra,  we can
characterise the corresponding notion of replacement as what are
variously known as dependent products, partial products or W-types.

But also, the operation of formulating replacement turns one theory into
another, so it can be iterated.  Ten years ago, I briefly believed that
this leads to inconsistency in ZF.   I suspect that this is a necessary
though not sufficient "rite of passage" - ie that, only after
temporarily
believing that it is  inconsistent, can one claim to understand what
the Axiom of Replacement says.

Paul Taylor