Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

2-categories 2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration finite foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory lie lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology multicategories noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2009

    I incorporated some of my spiel from the blog into the page type theory.

    • CommentRowNumber2.
    • CommentAuthorTobyBartels
    • CommentTimeOct 28th 2009

    I don't like JA's propositions as types page either, but I don't think that we should let it destroy the links in the Lab. He's already written that he expects it to be replaced, so it would be nice if wiki magic makes links automatically work when we do that.

    • CommentRowNumber3.
    • CommentAuthorJonAwbrey
    • CommentTimeOct 28th 2009
    Sorry, did I miss some discussion somewhere?
    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeOct 28th 2009

    You probably just missed Mike's removing the link to propositions as types from type theory.

    And I shouldn't really say that I ‘don't like’ your page, only that I don't like having it as the page on propositions as types —which I think you anticipated when you wrote ‘if it’s necessary to adjust the title after a while, that’s okay, but this name will do for the time being’ there. So someday I'll at least add some introductory material explaining what I think the propositions as types paradigm is about (or maybe Mike will), and then maybe we'll agree to move your stuff to a subsidiary page. But I'm not trying to start a discussion about that early; I'm just trying to save the link.

    • CommentRowNumber5.
    • CommentAuthorJonAwbrey
    • CommentTimeOct 28th 2009

    I'm thinking that propositions as types done right might be just the thing.

    I started doing this ambidextrous thing back in the days when I had group theory profs with opposing prefs — later on I was encouraged to see that a small but valiant band of catgorevores like Ernie Manes made of point of applying operators on the right.

    So now you know who to blame …

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeOct 28th 2009

    I don't want type theory to link to "propositions as types" for as long as doing so will take people to Jon's page, or, to be honest, any page with Jon's stuff on it. Especially since type theory has been linked from the ncafe and there has recently been discussion about "propositions as types," and I think Jon's page will do nothing more than confuse people and turn them off to the nlab. The idea of propositions as types is confusing enough already. But I didn't feel competent to guess a better name for Jon's page myself, since it doesn't make any sense to me, so instead I removed the link. Would it have been better to rename that page to, say, "Jon Awbrey's propositions as types" and let him rename it again if he has a better name in mind?

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 28th 2009
    It never ceases to amaze me how nice you guys are. Where many very able thinkers are placing great ideas in their personal webs as they fear they are yet too tentative for nLab, Jon is happy to fill endless nLab pages with his theories that nobody else understands, and which have never been shown to have anything to do with n-categories. It's just squatting.

    No doubt I will be accused of wanting to create a self-congratulatory country club.
    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeOct 28th 2009

    Well, Jon just moved his page, so the danger is passed.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2009
    • (edited Oct 28th 2009)

    I said this before: if a page makes no sense to sombody who feels like he should be in position to follow it, he should at least leave a brief query box indicating this.

    This is in the interest of all parties involved:

    • the author of a page wants to be alerted if people who should be able to follow the page, don't. So that it can be improved on if possible.

    • the non-expert reader wants to be alerted to material that is regarded as controversial even among the experts. That's only fair.

    I mean, that's the point of us putting material here instead of on our private hard-disk. To get the feedback. And critical feedback.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 28th 2009

    Urs, it's increasingly difficult to believe that Jon Awbrey as author of a page wants to be alerted if people who should be able to follow his page, don't. Regardless, I agree query boxes should be applied where skepticism is warranted. Applied perhaps liberally.

    Having Jon Awbrey retitle the page in this way is completely inappropriate and antisocial and against the collaborative spirit of this enterprise, and my patience with him is now right at the breaking point.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeOct 28th 2009
    • (edited Oct 28th 2009)

    Regarding Urs's two listed reasons above:

    • I ignored the first, since I knew that Jon knew that already.
    • I should have done it for the second.

    Todd wrote:

    Having Jon Awbrey retitle the page in this way is completely inappropriate and antisocial

    I completely disagree. He wrote all of that, none of it is what Mike or I is likely to want to see on that page, and he even wrote in his first draft that he expected that the name would need to be changed. He changed it now to please us! He was trying to be nice.

    Although, it would probably be better if he put all of this stuff on a personal web in the first place, since it is idiosyncratic and doesn't particularly mesh with the idiosyncracies of the rest of us.

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 28th 2009

    Look at the title. It's Jon thumbing his nose at his critics. I find it puerile and antisocial. It just doesn't belong on the nLab IMO.

    I agree with you strongly that it would definitely be better relegated to his personal web.

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeOct 28th 2009
    • (edited Oct 29th 2009)

    I think that the title is another of his silly puns, referring to his usage of reverse Polish notation; see the end of the middle line of his comment #5 here.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 29th 2009
    • (edited Oct 29th 2009)

    Maybe. That's a generous interpretation. If that is really the explanation, then at a minimum the explanation belongs right at the top of the page. But at this point, I am in no mood to play games.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeOct 29th 2009

    It never ceases to amaze me how nice you guys are.

    For me it is more a combination of laziness and cowardice, a desire to avoid unnecessary confrontation. However, I'm getting more fed up and I think I'm now with David and Todd. Whether or not the title is a pun, it is inappropriate. Jon has provided no evidence that his theories are related to the collaborative enterprise the rest of us are engaged in, and so they don't belong on the main nlab web.

    Jon, if you were given a private web, would you accept to have all of your pages moved there?

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 30th 2009
    What the hell is going on here! Why does the 'proposition as types' link from type theory point to Jon's page. I thought this had been changed. Has the change been reversed?
    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeOct 30th 2009

    It looks like Jon moved it back. I put some stuff up top to orient the reader, and I think that it would be perfectly reasonable for anybody to move Jon's stuff to another page as I suggested there.

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 30th 2009
    'Move' you mean 'delete' surely!
    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeOct 30th 2009

    Some other movements of these pages were obscured for a while by the cache bug; all should be clear now.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2013

    Maybe somebody can help me with sorting out reference data concerning the following:

    I know of this citationn

    • Per Martin-Löf, An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), 73-118.

    and I know of this online available pdf of Martin-Löf of essentially, but not quite, the same title.

    I have trouble seeing if the reference data corresponds to that pdf. Can anyone help?

    • CommentRowNumber21.
    • CommentAuthorUlrik
    • CommentTimeSep 17th 2013

    The pdf you found looks like an early version, compared to the one available at the doi 10.1016/S0049-237X(08)71945-1 – which at least has a longer introduction (there may be other changes as well). Many passages are word-for-word the same, though.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2013

    Okay, thanks for checking!!

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 9th 2015
    • (edited Jan 9th 2015)

    Some trivia:

    Added at type theory a pointer to data type. There I added a pointer to Sale 77, “Primitive Data Types” (and nothing else yet).

    That article shows up when one searches for the phrase “A type is a concept”. I happened to wonder which other sources might explicitly introduce types under the name “concept”, “notion” (maybe pre-fixed with “mathematical”).

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeFeb 27th 2015

    Thomas Holder kindly points out further relevant articles on the pre-history of type theory, have added them to the References there (right at the beginning of the list).

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeFeb 28th 2015

    I added a link to an online version of Appendix B ’The doctrine of types’ by Russell

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeMar 17th 2016

    Responding to a question by email, I added to type theory a remark that when we construct a “term model” by arbitrarily choosing truth values for the undecided statements, we no longer get a model that proves the completeness theorem.

  1. fixed a tiny typo: represeting -> representing

    anqurvanillapy

    diff, v118, current

  2. fixed a tiny typo: dangling right parenthesis after f(x) in B(x)

    anqurvanillapy

    diff, v119, current

  3. Thanks for these fixes!

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)