From a categorical point of view W-types may be ok, though for certain
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. parsimonious presentations I guess list objects may be smaller to describe and so desirable for that reason. To advertise slightly some of my own work that I presented at Topos à l'IHÉS (or at least some approximation of the following), the following construction gives an arithmetic pretopos (with finitary W-types), plus some. Take a filtered category R that is (classically) well-founded with terminal object, R may be large. Let E:R^op --> Topos/Set be a diagram in Grothendieck toposes. Define E*: R --> (Topos/Set)^op --> Set/LEX where the latter functor sends a topos to the underlying infinitary-lextensive category and a geometric morphism to its left exact cocontinuous inverse image functor. I allow for objects of LEX to be large categories. Then colim E* is an infinitary Heyting pretopos with subobject classifier and parameterised finitary W-types. If R is small, this is the limit of the diagram of toposes, but if R is large then this colimit arises in set theory as "(Easton) class forcing". If one starts instead with a base other than set, and even not with toposes but the underlying pretopos then I imagine one still have a reasonable structure at the end, minus perhaps the infinitary colimits and the subobject classifier. One of the points I wasn't sure on is the classical well-foundedness; I'm not 100% sure I conjecture than for any "pretame" class forcing (a partial order with top and with some local smallness conditions) then one has a similar result, constructing an Easton pretopos. There are conditions one can give that ensure one has a topos at the end. The pretameness could be generalised to other sites than partial orders with double negation. David On 3 August 2017 at 17:15, Steve Vickers <s.j.vickers@cs.bham.ac.uk> wrote:
Dear David,
Any AU should have finitary W-types, at least if "finite" is in the strong sense of "isomorphic to an initial segment of N".
Consider f: B -> A in an AU AA, such that f is finite in the slice AA/A. It will correspond to a morphism ar: A -> N, which we can think of as an arity map.
The elements of the W-type are trees, but an alternative representation is as elements of List(A), using reverse Polish notion. This is the key insight: that trees can be encoded as lists. After that, the rest is just about manipulating lists.
Now think of stack evaluation of reverse Polish expressions. We have a function sd: List(A) -> Z, such that sd(as) is the stack depth change after evaluating as:
sd empty = 0 sd (as ++ [a]) = sd(as) - ar(a) + 1 (pop ar(a) arguments, push the result)
Then the elements of the W-type are those bs such that sd(as) = 1 (just one value at the end), and sd(as') >= 1 for every non-empty prefix as' of as (no stack underflow).
All that can be expressed in AUs.
Obviously there's more to be done to show that the object constructed here has the right properties for a W-type, but our knowledge of reverse Polish notation gives us good grounds for conjecturing that it does. I haven't addressed "or rather a parametrized version", but hopefully that will work out.
I'm relating this to your formulation as follows. A_n is the fibre of ar over n. (Note - in my formulation I haven't assumed that A is finite, or that ar is bounded.) Then P(X) is the subobject of A x List(X) comprising pairs (a, xs) such that length of xs = ar(a).
Regards,
Steve.
On 2 Aug 2017, at 00:31, droberts.65537@gmail.com wrote:
Has anyone considered a version of arithmetic universes admitting all finitary W-types? I'm thinking initial algebras for "explicit polynomial" endofunctors, like
P(X) = A_0 + A_1 x X + A_2 x X^2 +... +A_n x X^n
or rather parameterised versions, for any given family A_0,...A_n.
Can these more general parameterised W-types be shown to exist from weaker considerations?
David
On 2 Aug 2017 8:42 AM, "Steve Vickers" <s.j.vickers@cs.bham.ac.uk> wrote:
Dear Andre,
Here's my own understanding of the history of AU definitions. Can you comment on its accuracy?
1. You defined the initial AU, with a concrete construction, as sufficient structure to embody arithmetic. You also showed that the initial AU has an internal initial AU, and used that to establish the Goedel gap between truth (external) and provability (internal).
2. You and others also discussed what the general definition might be. I picked this up from Gavin Wraith in the 1990s. (I had first learned about AUs from Gavin's talk at the 1985 Surrey conference on Categories in Computer Science.) Conceptually, it was "pretopos + free algebra constructions", but the question was how to get a collection of primitive constructions sufficient to get whatever else was needed. Gavin suggested free categories over directed graphs and free category actions over graph actions.
3. Milly Maietti proposed parametrized list objects, and I am persuaded her axiomatization is good. It is the one we used in our joint paper, and I used in "Sketches for AUs". I believe it provides adequate foundations for my proof with Palmgren of the existence of initial algebras for cartesian theories.
All the best,
Steve.
On 1 Aug 2017, at 01:26, a1078662@adelaide.edu.au wrote:
Hi,
There's a question at MathOverflow on the construction of algebraic closures in constructive mathematics by Joyal. The idea as far as I can tell is to construct the classifying arithmetic universe for the theory of the algebraic closure. People might either be interested or have something to contribute
https://mathoverflow.net/q/277551/4177
I repeat my respectful call for André to release his notes of arithmetic universes for us all to use, or at the least confirm that Maietti et al found the same definition :-)
Best regards, David
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
-- David Roberts http://ncatlab.org/nlab/show/David+Roberts [For admin and other information see: http://www.mta.ca/~cat-dist/ ]