# 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

## Site Tag Cloud

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

• 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

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

anqurvanillapy

3. Thanks for these fixes!

4. Added Mike’s recent paper to the references

5. Mike has chosen to allow composition along multiple types at once rather than only along one type at a time, corresponding to a prop rather than a polycategory. To the extent that this type theory is aimed at noncartesian monoidal categories and so perhaps of interest in quantum physics, what difference does the prop/polycategory choice represent there?

6. We should add it to the table at relation between type theory and category theory, but what to call it?

• CommentRowNumber33.
• CommentAuthorMike Shulman
• CommentTime1 day ago

Despite the temptation to speculate that the funny disjunction $\parr$ has something to do with entanglement, as far as I know there is no known application of polycategories to quantum physics. So this new type theory seems more likely to be applicable therein than standard classical linear logic. But I’d be ecstatic to be proven wrong…

• CommentRowNumber34.
• CommentAuthoratmacen
• CommentTime13 hours ago

I’m reading Mike’s paper and having some fun with the examples, but I don’t actually understand what’s so bad about using MILL for symmetric monoidal categories.

• CommentRowNumber35.
• CommentAuthorMike Shulman
• CommentTime11 hours ago

Re QM and CLL, a bit of googling turns up this and this.

Matt, try writing the examples in MILL and compare them.

• CommentRowNumber36.
• CommentAuthorTodd_Trimble
• CommentTime6 hours ago

I thought MILL stood for a fragment of linear logic involving both $\otimes$ and $\multimap$, or at least I feel certain I’ve seen the phrase/acronym used this way in the past.

• CommentRowNumber37.
• CommentAuthorMike Shulman
• CommentTime4 hours ago

@Todd: yes, that’s what the page linear logic says too. I didn’t realize multiplicative conjunction disagreed; I agree MILL should be $\otimes,\mathbf{1},\multimap$ since those are all the multiplicative and intuitionistic operations.

• CommentRowNumber38.
• CommentAuthoratmacen
• CommentTime3 hours ago

My bad, regarding MILL. I just forgot about $\multimap$.

Some typos:

In the step of tr(fg) = tr(gf) that has two “redexes”, it look like g is applied to the wrong label.

In self-duality of a Frobenius monoid, I think you swapped the components of the definition of eta, based on how you unfold it later.

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