# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorspitters
• CommentTimeJul 8th 2015

Quickly generated free topos. Mostly references.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJul 13th 2015
• (edited Jul 13th 2015)

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJul 13th 2015

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

• CommentRowNumber4.
• CommentAuthorThomas Holder
• CommentTimeSep 11th 2015

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!?

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeSep 11th 2015

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

• CommentRowNumber6.
• CommentAuthorThomas Holder
• CommentTimeSep 11th 2015
• (edited Sep 11th 2015)

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.

• CommentRowNumber7.
• CommentAuthorjonsterling
• CommentTimeMar 15th 2017
• (edited Mar 15th 2017)

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.

• CommentRowNumber8.
• CommentAuthorThomas Holder
• CommentTimeMar 15th 2017

Culpa mea, thanks for correcting this!

• CommentRowNumber9.
• CommentAuthorUrs
• CommentTimeMar 15th 2017

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.

• CommentRowNumber10.
• CommentAuthorDavidRoberts
• CommentTimeMar 15th 2017

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

• CommentRowNumber11.
• CommentAuthorUrs
• CommentTimeMar 15th 2017

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

• CommentRowNumber12.
• CommentAuthorDavidRoberts
• CommentTimeMar 15th 2017
• (edited Mar 15th 2017)

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

• CommentRowNumber13.
• CommentAuthorThomas Holder
• CommentTimeMar 15th 2017
• (edited Mar 15th 2017)

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.

• CommentRowNumber14.
• CommentAuthorjonsterling
• CommentTimeMar 15th 2017

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?

• CommentRowNumber15.
• CommentAuthorMike Shulman
• CommentTimeMar 15th 2017

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.

• CommentRowNumber16.
• CommentAuthorThomas Holder
• CommentTimeMar 16th 2017
• (edited Mar 16th 2017)

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.

• CommentRowNumber17.
• CommentAuthorMike Shulman
• CommentTimeMar 16th 2017

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.

• CommentRowNumber18.
• CommentAuthorDavid_Corfield
• CommentTimeApr 6th 2017

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

• CommentRowNumber19.
• CommentAuthorMike Shulman
• CommentTimeApr 6th 2017

I’ll respond at the cafe.

• CommentRowNumber20.
• CommentAuthorspitters
• CommentTimeJan 9th 2019

external projectivity