Acceptability of countable Replacement?
39 views
Skip to first unread message
David Roberts
Jun 16, 2021, 4:18:54 AM6/16/21
to construc...@googlegroups.com
Dear all,
I have a vague question, and perhaps people here can give me hints. It
is well-known that countable instances of choice (CC or DC, say) are
constructively acceptable for some. There are arguments, external to
the system, why such principles are "reasonable", and those sorts of
arguments are what I mean below.
Today I learned that it's probably the case that Borel Determinacy
only requires countable replacement (and in fact less), rather than
full Replacement. I was surprised, since I've been led to believe that
Replacement was strictly necessary for BD (and not some sub-schema).
I'm not so much interested in BD itself, but the idea that countable
replacement might be an axiom scheme justifiable by some external
argument, over a base theory like Zermelo+AC. Now of course, I don't
even care about Zermelo, but really something like ETCS, and
non-classical versions, like a constructively well-pointed topos with
nno.
Another reason one might think countable Replacement is sensible is
that it seems to be needed for recent work in arithmetic geometry,
namely Clausen and Scholze's condensed mathematics. Essentially it
looks like it is needed to construct a certain simplicial space, that
is in each dimension a Stone–Čech compactification of an increasingly
large set. There should be a nice locale-theoretic version of all
this, and it feels very constructive. But it seems odd to have to fall
back to a strong axiom schema to prove something that is ultimately
rather down to earth (I don't count BD as being in the same
neighbourhood, here).
Any thoughts? Apologies for such a vague email, I'm trying to see my
way through this.
All the best,
David
David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com
I have a vague question, and perhaps people here can give me hints. It
is well-known that countable instances of choice (CC or DC, say) are
constructively acceptable for some. There are arguments, external to
the system, why such principles are "reasonable", and those sorts of
arguments are what I mean below.
Today I learned that it's probably the case that Borel Determinacy
only requires countable replacement (and in fact less), rather than
full Replacement. I was surprised, since I've been led to believe that
Replacement was strictly necessary for BD (and not some sub-schema).
I'm not so much interested in BD itself, but the idea that countable
replacement might be an axiom scheme justifiable by some external
argument, over a base theory like Zermelo+AC. Now of course, I don't
even care about Zermelo, but really something like ETCS, and
non-classical versions, like a constructively well-pointed topos with
nno.
Another reason one might think countable Replacement is sensible is
that it seems to be needed for recent work in arithmetic geometry,
namely Clausen and Scholze's condensed mathematics. Essentially it
looks like it is needed to construct a certain simplicial space, that
is in each dimension a Stone–Čech compactification of an increasingly
large set. There should be a nice locale-theoretic version of all
this, and it feels very constructive. But it seems odd to have to fall
back to a strong axiom schema to prove something that is ultimately
rather down to earth (I don't count BD as being in the same
neighbourhood, here).
Any thoughts? Apologies for such a vague email, I'm trying to see my
way through this.
All the best,
David
David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com
Toby Bartels
Jun 17, 2021, 12:15:11 PM6/17/21
to 'David Roberts' via constructivenews
If being constructive is about avoiding Excluded Middle (and perhaps also avoiding other forms of Choice), then I don't think that Replacement is problematic at all. To take a standard example, N + P(N) + P(P(N)) + ... (the disjoint union of the iterated power sets of the set of natural numbers) seems straightforward to construct; an element consists of a natural number n and an element of P^n(N), where an element of P^0(N) is a natural number and an element of P^{n+}(N) is a subset of P^n(N). There are no impossible or arbitrary decisions to make here.
Of course, that's countable Replacement, the simplest kind, and what you mostly care about. But a more general application is no more difficult; if X is a set and φ is a functional entire relation in the first-order language of set theory between elements of X and sets, then an element of the disjoint union Σ_x φ(x) is an element x of X together with an element of φ(x), which is the unique set Y such that φ(x,Y) holds. A constructive proof that φ is entire will tell you how to find φ(x), and the result will depend only on x because φ is functional.
Traditionally, Replacement constructs the *set* of the φ(x) rather than their disjoint union, but you might consider that set ill-typed, or you might consider it equivalent to X; the disjoint union (together with its obvious function to X) is the structural heart of Replacement. There also versions of Replacement for fully structural set theories in which it's impossible or meaningless for φ to be functional (because necessarily φ(x,Y) <=> φ(x,Y') whenever #Y = #Y'), but this can be handled in much the same way that you can ensure that fully faithful eso functors have inverses.
Where Replacement is potentially a problem is when you are being *predicative*. Of course, predicativists tend not to accept even P^2(N), but even if you accept all power sets, the disjoint union in the example might be taking things one step too far. Or if you're a constructivist who doesn't accept power sets but does accept function sets (so weakly predicative), then you could repeat the example using 2^N instead of P(N) and still think of the disjoint union as too large.
But since Replacement doesn't imply impredicative Separation without Excluded Middle, one could argue that Replacement can be allowed in a weakly predicative set theory just like function sets can be. And for an argument from authority, notice that both Peter Aczel's Constructive ZF and Steve Awodey's Constructive Set Theory (even the Basic CST, which has no function sets) include Replacement. (CZF even has Strong Collection, which, without Excluded Middle, is stronger than Replacement but still doesn't imply full Separation.) (As usual, ‘Constructive’ in the names of these set theories means predicative as well; one uses ‘Intuitionistic’ instead for an impredicative constructive set theory.)
So all in all, I think that Replacement is fine if you're being impredicative, and it's probably fine even if you're being weakly predicative as long as you're being constructive.
—Toby
Of course, that's countable Replacement, the simplest kind, and what you mostly care about. But a more general application is no more difficult; if X is a set and φ is a functional entire relation in the first-order language of set theory between elements of X and sets, then an element of the disjoint union Σ_x φ(x) is an element x of X together with an element of φ(x), which is the unique set Y such that φ(x,Y) holds. A constructive proof that φ is entire will tell you how to find φ(x), and the result will depend only on x because φ is functional.
Traditionally, Replacement constructs the *set* of the φ(x) rather than their disjoint union, but you might consider that set ill-typed, or you might consider it equivalent to X; the disjoint union (together with its obvious function to X) is the structural heart of Replacement. There also versions of Replacement for fully structural set theories in which it's impossible or meaningless for φ to be functional (because necessarily φ(x,Y) <=> φ(x,Y') whenever #Y = #Y'), but this can be handled in much the same way that you can ensure that fully faithful eso functors have inverses.
Where Replacement is potentially a problem is when you are being *predicative*. Of course, predicativists tend not to accept even P^2(N), but even if you accept all power sets, the disjoint union in the example might be taking things one step too far. Or if you're a constructivist who doesn't accept power sets but does accept function sets (so weakly predicative), then you could repeat the example using 2^N instead of P(N) and still think of the disjoint union as too large.
But since Replacement doesn't imply impredicative Separation without Excluded Middle, one could argue that Replacement can be allowed in a weakly predicative set theory just like function sets can be. And for an argument from authority, notice that both Peter Aczel's Constructive ZF and Steve Awodey's Constructive Set Theory (even the Basic CST, which has no function sets) include Replacement. (CZF even has Strong Collection, which, without Excluded Middle, is stronger than Replacement but still doesn't imply full Separation.) (As usual, ‘Constructive’ in the names of these set theories means predicative as well; one uses ‘Intuitionistic’ instead for an impredicative constructive set theory.)
So all in all, I think that Replacement is fine if you're being impredicative, and it's probably fine even if you're being weakly predicative as long as you're being constructive.
—Toby
Paul Taylor
Jun 21, 2021, 6:12:07 AM6/21/21
to construc...@googlegroups.com
à propos of David Roberts' question about Replacement:
It's fifty years since elementary toposes were introduced.
It's 22 years since my April Fool about the inconsistency of ZFC.
It's a disgrace that categorical logicians still have no answer
to the axiom-scheme of replacement.
That is not, of course, to say that we should be answerable
to set theorists for our foundations, or even take dictation
from them about problems or axioms.
What is undeniable is that an elementary topos with natural
numbers object is not enough to do various common constructions
in category theory and mainstream (ie outside set theory)
mathematics.
Principal amongst these is forming infinite limits or colimits
of rapidly growing chains of objects. Indeed, we can't even
formulate such a diagram, with a view to invoking the (co)limit
as a new axiom.
(More often these occur as colimits, but David Roberts' example
was a limit. However, despite his private explanations,
I didn't follow the topological background.)
It could be done by saying they're "external" (co)limits,
which amounts to introducing "universes", but that wholly
misses of the point of what Replacement claims can be done
"within" our own world.
The question becomes more reasonable if chains are obtained
by iterating a particular functor. That is, "transfinite
iteration of functors" could potentially be EXPRESSED within
the language of an elementary topos, though of course not
CONSTRUCTED.
For that we first need a good categorical theory of ordinals,
or at least of well founded structures. I did some work
on these ideas in the 1990s and have recently returned to that:
Well founded coalgebras and recursion
www.paultaylor.eu/ordinals
This proves a version of von Neumann's recursion theorem,
for well founded coalgebras, but the new version only assumes
that the functor preserves monos and not inverse images.
This requires a new constructive induction principle based
on Pataraia's fixed point theorem for dcpos.
Although the argument is inherited from Set, the requirements
on the category are thoroughly investigated, in particular
replacing "monos" with a factorisation system.
This doesn't go as far as transfinite iteration of functors,
but I believe that I can substantiate the remarks in the final
pages of my book and am currently writing that up.
I don't think I've ever seen a formal proof in set theory
that transfinite iteration can constructed using Replacement,
and have very little clue what the axiom-scheme is supposed
to say in general.
The problem is, if you ask a set theorist, you get an
answer in Hebrew.
[NB: this is a metaphor - no offence is intended to those
who write from right to left.]
Peter Freyd once commented that the "set theorists had made
a unilateral declaration of independence from mathematics".
I have some ideas what he might have meant, but I had not
had any email replies from him for a long time.
A good example of this that I do understand is known as
Mostowski's theorem:
every extensional well founded relation
is isomorphic to a unique set.
This requires Replacement, but purely because of the way
that set theory is set up.
A natural variation on the result is that
every well founded relation has an extensional quotient.
Proving this is simply a matter of constructing an
equivalence relation, corecursively, and can be done in
any elementary topos.
My recent work above proves a new version of Mostowski's
theorem, but with monos and equivalence relations replaced
by a factorisation system.
After that we can do some serious category theory, inventing
suitable categories, functors and factorisations to exploit
what then becomes an extraordinarily powerful construction.
As I said, I believe I can show how to express transfinite
iteration as an example of this.
I still don't know what Replacement means in general.
Returning to what prompted my "April Fool",
something that really puzzled me in the final stages of
writing my book was that,
- the "gluing construction" (aka "logical relations")
provides a a very simple and extraordinarily powerful
way of providing consistency-like results; but
- Godel's incompleteness theorem (and André Joyal's
categorical version of it that was more recently
written up by Alexander Gietelink Oldenziel) says
this can't be done.
This must mean that the gluing construction involves some
very powerful induction, based on Replacement.
I'll leave that there, because such ideas give me vertigo.
Paul Taylor
The web address for my draft paper again:
www.paultaylor.eu/ordinals
It's fifty years since elementary toposes were introduced.
It's 22 years since my April Fool about the inconsistency of ZFC.
It's a disgrace that categorical logicians still have no answer
to the axiom-scheme of replacement.
That is not, of course, to say that we should be answerable
to set theorists for our foundations, or even take dictation
from them about problems or axioms.
What is undeniable is that an elementary topos with natural
numbers object is not enough to do various common constructions
in category theory and mainstream (ie outside set theory)
mathematics.
Principal amongst these is forming infinite limits or colimits
of rapidly growing chains of objects. Indeed, we can't even
formulate such a diagram, with a view to invoking the (co)limit
as a new axiom.
(More often these occur as colimits, but David Roberts' example
was a limit. However, despite his private explanations,
I didn't follow the topological background.)
It could be done by saying they're "external" (co)limits,
which amounts to introducing "universes", but that wholly
misses of the point of what Replacement claims can be done
"within" our own world.
The question becomes more reasonable if chains are obtained
by iterating a particular functor. That is, "transfinite
iteration of functors" could potentially be EXPRESSED within
the language of an elementary topos, though of course not
CONSTRUCTED.
For that we first need a good categorical theory of ordinals,
or at least of well founded structures. I did some work
on these ideas in the 1990s and have recently returned to that:
Well founded coalgebras and recursion
www.paultaylor.eu/ordinals
This proves a version of von Neumann's recursion theorem,
for well founded coalgebras, but the new version only assumes
that the functor preserves monos and not inverse images.
This requires a new constructive induction principle based
on Pataraia's fixed point theorem for dcpos.
Although the argument is inherited from Set, the requirements
on the category are thoroughly investigated, in particular
replacing "monos" with a factorisation system.
This doesn't go as far as transfinite iteration of functors,
but I believe that I can substantiate the remarks in the final
pages of my book and am currently writing that up.
I don't think I've ever seen a formal proof in set theory
that transfinite iteration can constructed using Replacement,
and have very little clue what the axiom-scheme is supposed
to say in general.
The problem is, if you ask a set theorist, you get an
answer in Hebrew.
[NB: this is a metaphor - no offence is intended to those
who write from right to left.]
Peter Freyd once commented that the "set theorists had made
a unilateral declaration of independence from mathematics".
I have some ideas what he might have meant, but I had not
had any email replies from him for a long time.
A good example of this that I do understand is known as
Mostowski's theorem:
every extensional well founded relation
is isomorphic to a unique set.
This requires Replacement, but purely because of the way
that set theory is set up.
A natural variation on the result is that
every well founded relation has an extensional quotient.
Proving this is simply a matter of constructing an
equivalence relation, corecursively, and can be done in
any elementary topos.
My recent work above proves a new version of Mostowski's
theorem, but with monos and equivalence relations replaced
by a factorisation system.
After that we can do some serious category theory, inventing
suitable categories, functors and factorisations to exploit
what then becomes an extraordinarily powerful construction.
As I said, I believe I can show how to express transfinite
iteration as an example of this.
I still don't know what Replacement means in general.
Returning to what prompted my "April Fool",
something that really puzzled me in the final stages of
writing my book was that,
- the "gluing construction" (aka "logical relations")
provides a a very simple and extraordinarily powerful
way of providing consistency-like results; but
- Godel's incompleteness theorem (and André Joyal's
categorical version of it that was more recently
written up by Alexander Gietelink Oldenziel) says
this can't be done.
This must mean that the gluing construction involves some
very powerful induction, based on Replacement.
I'll leave that there, because such ideas give me vertigo.
Paul Taylor
The web address for my draft paper again:
www.paultaylor.eu/ordinals
David Roberts
Jun 21, 2021, 11:48:05 PM6/21/21
to construc...@googlegroups.com
> (More often these occur as colimits, but David Roberts' example
> was a limit. However, despite his private explanations,
> I didn't follow the topological background.)
Not to contradict my esteemed colleague, but what I was meaning was a countable disjoint union \coprod_{n\in N} of the result of an iterative construction of objects U_n in the category of topological spaces, each of which is the result of applying the endofunctor \beta U:Top\to Set \to Top to a (linearly-growing) finite limit built from the previously-built objects U_{n-1}, U_{n-2},..., In the construction all the U_n, being Stone–Čech compactifications of sets, turn out to extremally disconnected. The original input to get U_0 is a Stone space.
> was a limit. However, despite his private explanations,
> I didn't follow the topological background.)
As the cardinality of (the underlying set of) each U_k grows doubly-exponentially, this countable disjoint union cannot be proved to exist in ETCS, but does in ZFC, or even in ZFC with mild instances of Replacement. Hence my question.
A version of this in foundations other than ZFC would be interesting, as it is a construction in Clausen and Scholze's recent innovation "condensed mathematics", serving to show that certain cohomology groups vanish.
All the best,
David
> You received this message because you are subscribed to the Google Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/constructivenews/alpine.DEB.2.21.2106211110100.29529%40maclane.
Steve Vickers
Jun 22, 2021, 6:34:29 AM6/22/21
to drobert...@gmail.com, construc...@googlegroups.com
Dear David,
Interesting to see this reference to condensed mathematics, work that Joyal has alerted me to.
Their basic question is how to do algebra when rings/modules/groups carry a topology, and for me, with my interest in exploring the scope of geometric reasoning, it is of central importance.
Their work quickly goes non-geometric, with extremally disconnected spaces where the *frame* is a (complete) Boolean algebra: so maybe this is an indication of the limits of geometric reasoning. On the other hand, it may be that point-set intuitions are polluting a good underlying idea of condensed mathematics. For example, it is all too easy to overlook situations where a space is properly Stone, not discrete.
A notorious example is the exponential 0^X where X is a set. The *point-free topological* exponential is Stone, and this affects the result of the iterated 0^0^X. This is discrete, but different from what you get if you calculate 0^X as a set. Think of the topology on 0^X as restricting the continuous maps 0^X -> 0. In fact, 0^0^X is the image of the map X -> 1, so if X is a subset of 1 then 0^0^X = X.
Another example, more algebraic, is the space of square roots of a complex number z_0. If z_0 is non-zero, then its square roots form a Kuratowski finite, discrete space with decidable equality (and cardinality 2, of course), giving a sheaf over the punctured complex plane C-{0}. Being finite decidable, it is also Stone: in other words, the local homeomorphism is entire. We can extend this bundle to include z_0 = 0, by using the squaring map C -> C. This is still Stone (and one can calculate its sheaf of Boolean algebras), but no longer discrete (the squaring map is not a local homeomorphism).
Hence we should think of the space of square roots of z_0 as being Stone but not discrete. Similar considerations are going to apply to the space of roots of any polynomial over C and hence should pervade algebraic geometry.
My speculation - not even a conjecture - is that if one applies observations like that consistently, then it may be possible to adjust the Clausen-Scholze development, including the initial definition of “condensed sets”, to reach their destination in a geometric way. That would presumably also sidestep the set-theoretic discussion of axiom of replacement. So far I am nowhere close to an understanding of how they get to their cohomology results, but I sense that may be more important than a literal examination of the initial postulates. Do you have any insights you can share?
All the best,
Steve.
Interesting to see this reference to condensed mathematics, work that Joyal has alerted me to.
Their basic question is how to do algebra when rings/modules/groups carry a topology, and for me, with my interest in exploring the scope of geometric reasoning, it is of central importance.
Their work quickly goes non-geometric, with extremally disconnected spaces where the *frame* is a (complete) Boolean algebra: so maybe this is an indication of the limits of geometric reasoning. On the other hand, it may be that point-set intuitions are polluting a good underlying idea of condensed mathematics. For example, it is all too easy to overlook situations where a space is properly Stone, not discrete.
A notorious example is the exponential 0^X where X is a set. The *point-free topological* exponential is Stone, and this affects the result of the iterated 0^0^X. This is discrete, but different from what you get if you calculate 0^X as a set. Think of the topology on 0^X as restricting the continuous maps 0^X -> 0. In fact, 0^0^X is the image of the map X -> 1, so if X is a subset of 1 then 0^0^X = X.
Another example, more algebraic, is the space of square roots of a complex number z_0. If z_0 is non-zero, then its square roots form a Kuratowski finite, discrete space with decidable equality (and cardinality 2, of course), giving a sheaf over the punctured complex plane C-{0}. Being finite decidable, it is also Stone: in other words, the local homeomorphism is entire. We can extend this bundle to include z_0 = 0, by using the squaring map C -> C. This is still Stone (and one can calculate its sheaf of Boolean algebras), but no longer discrete (the squaring map is not a local homeomorphism).
Hence we should think of the space of square roots of z_0 as being Stone but not discrete. Similar considerations are going to apply to the space of roots of any polynomial over C and hence should pervade algebraic geometry.
My speculation - not even a conjecture - is that if one applies observations like that consistently, then it may be possible to adjust the Clausen-Scholze development, including the initial definition of “condensed sets”, to reach their destination in a geometric way. That would presumably also sidestep the set-theoretic discussion of axiom of replacement. So far I am nowhere close to an understanding of how they get to their cohomology results, but I sense that may be more important than a literal examination of the initial postulates. Do you have any insights you can share?
All the best,
Steve.
stre...@mathematik.tu-darmstadt.de
Jun 22, 2021, 8:54:03 AM6/22/21
to David Roberts, construc...@googlegroups.com, stre...@mathematik.tu-darmstadt.de
Replacement is the set theorist's tool allowing him to define families of
sets by recursion as e.g. P^k(N) for k in N.
A more conceptual way is to employ Universes as I discussed in my old
article "Universes in Toposes". The point is that functions from N to a
universe U can be defined by iteration as usual like the one in the above
example.
In set theory there is a universe, namely the class of all sets, which,
however, has poor closure properties.
All the toposes considered in the literature which are not of a sytactic
kind admit such universes.
In infinity category theory universes are also employed under the somewhat
confusing name "object classifiers".
For early references to universes in topos theory there come to my mind
the following ones.
Literally the same definition as in my above mentioned article can be
found in Jean Benabou's "Problemes dan les topos" from 1971 though his
motivating example were finite sets definable in any topos with nno. This
reference is given in my paper before the official definition which I
found independently triggered by my work on semantics of type theory.
The second reference is Ch. Maurer's paper "Universes in Topoi" in SLNM 445
where universes are coneptualized as monos U --> P(U) satisfying some
properties. This notion is closer to set theory and variations of it were
later employed in "algebraic set theory".
Thomas
sets by recursion as e.g. P^k(N) for k in N.
A more conceptual way is to employ Universes as I discussed in my old
article "Universes in Toposes". The point is that functions from N to a
universe U can be defined by iteration as usual like the one in the above
example.
In set theory there is a universe, namely the class of all sets, which,
however, has poor closure properties.
All the toposes considered in the literature which are not of a sytactic
kind admit such universes.
In infinity category theory universes are also employed under the somewhat
confusing name "object classifiers".
For early references to universes in topos theory there come to my mind
the following ones.
Literally the same definition as in my above mentioned article can be
found in Jean Benabou's "Problemes dan les topos" from 1971 though his
motivating example were finite sets definable in any topos with nno. This
reference is given in my paper before the official definition which I
found independently triggered by my work on semantics of type theory.
The second reference is Ch. Maurer's paper "Universes in Topoi" in SLNM 445
where universes are coneptualized as monos U --> P(U) satisfying some
properties. This notion is closer to set theory and variations of it were
later employed in "algebraic set theory".
Thomas
Paul Taylor
Jun 22, 2021, 9:23:27 AM6/22/21
to construc...@googlegroups.com
Steve Vickers rightly points out that, when one takes the
topology of a situation into consideration properly, the
need for set theory's scary "big" sets and opaque axioms
disappears.
However, David Roberts' question was about Replacement,
and he told me privately that he was interested in that
rather than the particular topological question that he
raised.
OK, instead of focusing on what was needed for the question
as he posed it, I advertised recent work of my own that
is a couple of steps away from being relevant.
So, let's cut that down to the ad hoc version needed
for N-indexed chains.
(I didn't really follow David's construction, but it seemed
like he had something more complicated than a chain, which
would be a reason for introducing my more general theory
of well founded coalgebras.)
---
The basic problem is that we have a functor T for which
we want to find the limit or colimit of T^n(0) over natural
numbers.
Of course this is not going to be a CONSTRUCTION in an
elementary topos, it will be a DEFINITION or CHARACTERISATION,
just as the universal property of an exponential or the
subobject classifier is a definition in a category with
finite limits.
Since T is applied to infinitely many things, we need to use
fibred or indexed category theory (or my notion of category
with display maps) to express T being applied in parallel
to each of the members of a family of objects.
In general we also need indexed (co)limits, although we can
get away with a single one since we just have an N-indexed
chain.
I will assume that readers are familiar with technology to
express these things.
Now, I want to wrap up this "family" as a single morphism
in a specially constructed category. The codomain is going
to be a poset (N or N+{oo} with the usual partial order).
The morphism is then a fibration whose fibres are the
objects in the family, so the domain is the "total category",
which is essentially the disjoint union of the family.
At this stage, we have ANY family of objects, not necessarily
the iterates of the functor. This is a familiar thing to
express using the logic of a topos.
Then we apply the functor to each of the members of the
family, to yield another family with the same indexing poset.
In the case of the diagram with "infinity" adjoined, we
assign the colimit at that point.
For a general well founded structure, the value at each
point is the colimit of the functor applied to the predecessors
of the point in the well founded structure.
----
So far, this is just any old family of objects.
The point is to characterise when this family actually
consists of the iterates of the functor.
The magic of fibred category theory is that this happens
exactly when we have a pullback square.
(I would need to be more formal and write LaTeX to show
this properly, but I am assuming that anyone reading this
on "constructivenews" will be sufficiently familiar with
fibred category theory to work it out.)
The categorical axiom that we would add to those of an
elementary topos is that such pullbacks exist.
-----
Now let me try to explain how this is an example of my
generalised Mostowski's theorem.
Think of any category whose objects are arrows and whose
morphisms are commutative squares, assuming we have finite
limits.
The morphisms (rectangles) in this category have a
FACTORISATION SYSTEM in which the "monos" are the pullback
squares and the "epis" are squares of which the bottom edge
is an isomorphism.
(Actually, I need to modify that and say that the "monos"
are pullback squares whose horizontals edges are plain monos
in the original category, and whose "epis" have epis rather
than isos from the original category as their bottom edges.)
Applying the general theory of my draft paper to this,
a well founded coalgebra in the arrow category is any family
over a well founded coalgebra in the base. Then it is
extensional iff it is the transfinite iteration as above.
The construction (called "successor quotient") in my paper
can be seen as "cranking the handle" of the transfinite
iteration. However, I would need to draw some diagrams
(instead of writing plain text) to demonstrate this.
----
The categorical version of the axiom of replacement should
be (a) a piece of category theory, not a parroting of set
theory and (b) something pretty bold.
Usually in category theory we express things in terms of
universal properties, aka adjunctions.
So, how about "any functor that preserves all limits has a
left adjoint"?
Unfortunately, that's too bold: the underlying set functor
from complete Boolean algebras preserves all limits, but
cannot have a left adjoint.
There needs to be some check on "reasonableness", which has
traditionally been done using well-foundedness.
My conjecture is that this can be done using my generalisation
of Mostowski's theorem.
---
PS Thomas Streicher posted his reply just as I had finished
writing the above. It is principally about universes.
As I commented before, I believe that to introduce universes
(whether in set- type- or categorical form) is to miss the
point of Replacement.
Somehow it constructs "very big" things, FROM BELOW, whereas
universes construct things FROM ABOVE.
My informal intuition about Replacement is that, if you have
a good set of architect's plans, you can build the skyscraper.
This is done from below, not by means of a crane that comes
down from the heavens.
I think it's something like turning a term model, say of
higher order logic, into one in which the predicates denote
concrete subsets and all subsets are so denoted.
Nevertheless, I thank Thomas for the references.
Paul Taylor
Reply all
Reply to author
Forward
0 new messages