Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorspitters
    • CommentTimeJul 9th 2015

    Quickly generated free topos. Mostly references.

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

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

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

    See also the discussion on Math Overflow

    • 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, NN, and Ω\Omega lacking relations beyond the bare necessities.

    to

    the only types are 1 (unit type), NN (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 “NN” 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,Ω,N1,\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 NN is projective? If we think it necessary, we could add a caveat that this does not imply that NN 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 (,1)(\infty, 1)-toposes?

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeApr 6th 2017

    I’ll respond at the cafe.

    • CommentRowNumber20.
    • CommentAuthorspitters
    • CommentTimeJan 9th 2019

    external projectivity

    diff, v14, current