external projectivity

]]>I’ll respond at the cafe.

]]>In view of Mike’s post on infinity-toposes, what prospects do we have for free elementary $(\infty, 1)$-toposes?

]]>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.

]]>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.

What about just removing the reference to countable choice and simply asserting that $N$ is projective? If we think it necessary, we could add a caveat that this does not imply that $N$ is *internally* projective, which would be the statement of countable choice.

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?

]]>I was perhaps misleadingly vague on what ’all toposes’ means in this context in the idea section since the specific category in which $\mathcal{T}$ is initial is somewhat inappropriate for an idea section with the intention to convey the intuition that $\mathcal{T}$ is the topos that corresponds to the type theory freely constructed from $1,\Omega, N$. 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.

]]>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!).

]]>Or else I misread what “$N$” is to stand for. All the more reason to add such explanations to the entry.

]]>If the free tops has an NNO, it’s not the initial object in the category of all toposes, no?

]]>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, $N$, and $\Omega$ lacking relations beyond the bare necessities.

to

]]>the only types are 1 (unit type), $N$ (natural numbers type), and $\Omega$ (type of propositions) lacking relations beyond the bare necessities.

*Culpa mea*, thanks for correcting this!

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

]]>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.

]]>Would you or anyone else be in a position to record proofs?

]]>I’ve added at free topos a short remark pointing to two “legendary” results on $\mathcal{T}$ mentioned in passing in Lambek and Scott’s book. I don’t know whether these results are meanwhile better documented in the literature!?

]]>I suppose this also deserves to be cross-linked (with comments, preferably) with *term model*.

Thanks. I have now made a bunch of keywords come out as hyperlinks. Also added (uncommented) cross-linking with *syntactic category*.

Quickly generated free topos. Mostly references.

]]>