Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Quickly generated free topos. Mostly references.
Thanks. I have now made a bunch of keywords come out as hyperlinks. Also added (uncommented) cross-linking with syntactic category.
I suppose this also deserves to be cross-linked (with comments, preferably) with term model.
I’ve added at free topos a short remark pointing to two “legendary” results on mentioned in passing in Lambek and Scott’s book. I don’t know whether these results are meanwhile better documented in the literature!?
Would you or anyone else be in a position to record proofs?
Don’t count on me for the proofs! I am afraid these are probably very deep theorems. I recollect that Jaap van Oosten has written somewhere that the proof of the projectivity of N is unknown to all the experts he had asked.
I have updated this page to change the claim that “Brouwer’s theorem holds in the free topos” to “All maps R -> R in the free topos represent continuous functions” (which is the claim that Lambek & Scott attributed to Joyal). I think it is easy to misunderstand the original statement as a claim that Brouwer’s theorem holds as a proposition in the internal language of the free topos, which is definitely false.
See also the discussion on Math Overflow
Culpa mea, thanks for correcting this!
For the sake of the reader of the entry who may not already know what it is about, I have expanded the line
the only types are 1, , and lacking relations beyond the bare necessities.
to
the only types are 1 (unit type), (natural numbers type), and (type of propositions) lacking relations beyond the bare necessities.
If the free tops has an NNO, it’s not the initial object in the category of all toposes, no?
Or else I misread what “” is to stand for. All the more reason to add such explanations to the entry.
I presumed it was an NNO too.
I guess this relates to Joyal’s use of arithmetic universes to prove Gödel (if only he would release it!).
I was perhaps misleadingly vague on what ’all toposes’ means in this context in the idea section since the specific category in which is initial is somewhat inappropriate for an idea section with the intention to convey the intuition that is the topos that corresponds to the type theory freely constructed from . The background is that the precise equivalence between type theories (per definition with NNO in Lambek-Scott) and toposes (by convention with NNO in Lambek-Scott) on which this relies as presented in their book is slightly technical.
Until an energetic person shows up and puts the precise proposition in I provisorily made it less ambiguous.
Jonas Frey tells me that based on a discussion w/ Steve Awodey and Pieter Hofstra, they do not think that a free topos w/ NNO satisfies countable choice; this is again the issue of internal vs external. As it is written, the page is implying a claim about the internal correctness of countable choice, but this is probably not the case. Any suggestions on how to rephrase the claim in the page?
What about just removing the reference to countable choice and simply asserting that is projective? If we think it necessary, we could add a caveat that this does not imply that is internally projective, which would be the statement of countable choice.
I removed the reference to countable choice. What I had written there was based on my reading of the remarks on p.250 of the Lambek-Scott book which I construed as referring to their discussion on pp.233-34. It would be nice if somebody could throw in some clarifying remarks as concerning the status of the in/external projectvity of N.
I also see that Lambek-Scott (p.viii) refer to the property of R as Brouwer’s principle. If this is established terminology it would be worthwhile to note this somewhere on the nLab.
IMHO Lambek-Scott are quite sloppy in their discussion of these two statements, as regards internal/external.
I don’t know how standard “Brouwer’s principle” is; I’ve also heard it called “Brouwer’s theorem” although of course Brouwer’s “proof” of it isn’t valid in most modern mathematical systems.
In view of Mike’s post on infinity-toposes, what prospects do we have for free elementary -toposes?
I’ll respond at the cafe.
1 to 20 of 20