Re: Re: Algebraic closures and arithmetic universes

[Steve Vickers <s.j.vickers@cs.bham.ac.uk>]

Dear David,

I'm sure there's scope for optimizing the AU axioms. In my "Sketches for
AUs" I replaced the original list-arithmetic pretopos with a slightly
different formulation that exploits the fact that, in the presence of
list objects, the pretopos has all finite colimits. (This is essentially
because one can form transitive closures of relations and hence get
arbitrary coequalizers.)

However, note that to use finitary W-types as internal structure (the
way I described) you have to express "finitary" internally somehow; and
to use them, or some of them, as external structure, with externally
given A_i etc, you may need infinitely many operations to present the
theory of AUs.

My own feeling when I wrote "Sketches for AUs" was that the ugliest bits
of the presentation were the exactness and stability conditions needed
for a pretopos. (Look at the rules for exactness and stability in
definition 15, for equivalence extensions.) I wondered whether they
could be simplified in the presence of the list objects.

All the best,

Steve.

On 03/08/2017 09:25, droberts.65537@gmail.com wrote:
> Hi Steve,
>
> Ah, excellent. I do wonder then, if free parameterised list objects
> are finitary (parameterised) W-types and all of the latter exist when
> the former exist (in the presence of the other assumptions on the AU),
> if existence of W-types is a cleaner assumption for an AU. It may be
> like the definition of elementary topos, where terminal object,
> pullbacks and power objects suffice, but people sometimes just package
> (local) cartesian closedness into the definition (not to speak of
> finite colimits) as it is perfectly equivalent.
>
> From a categorical point of view W-types may be ok, though for certain
> parsimonious presentations I guess list objects may be smaller to
> describe and so desirable for that reason.
>



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]