added pointer (here and at calculus of constructions) to:
fixed author name and added more hyperlinks for this item
I noticed that the list of references here was lacking some glue where it jumped from Russel right to identity types. I have now filled in (here) pointer to:
But there is lots of room left for the eager type theorist to further expand and beautify the discussion of the literature in this entry…
]]>Probably, but I don’t know where.
]]>I see, thanks. That’s indeed recognizable, with some parsing effort. Did he ever state it in more streamlined form?
]]>Page 94, “I-elimination”.
]]>Where does he state it, clearly? In “An intuitionistic theory of types: predicative part” it appears in mere prose in Sec 1.7, and in some baroque form on p. 109.
]]>Martin-Lof’s version isn’t recognizable?
]]>I have added pointer to:
which may be the earliest reference that I have seen which actually states the J-rule in recognizable form
]]>added pointer to:
OK, I put it up at tensor projection. Please take a look and tell me what you think.
]]>Good news: I finished a drafty set of rules for , , and with tensor projections. Don’t set your hopes too high; it’s kind of a mess. Now I just have to figure out how to typeset this on a new page…
]]>Right. I was thinking about whether it’d be convenient to make it not sugar. Not convenient enough for me.
The could be sugar for (the same thing as) . Sugar doesn’t need to have good metatheoretical properties.
]]>Yes, but the latter is just sugar for or , and I also didn’t try to make that desugaring precise.
]]>Odd: if is a comonoid, in the context , you’d allow and but not , right? Makes type checking yet more complicated. I’m not going to handle that.
]]>As I always say to my calculus students, the more you practice it, the better you’ll get at it, and the more you’ll like it.
]]>I see it clearly now. I was guessing they were equal, I just wasn’t sure. You see? This is why I don’t like category theory much. I’m bad at it. :)
I’m going to put off the additive connectives at first. I have a plan, but the bookkeeping is more complicated, so I should work out the details of MILL first.
]]>By definition, is the unique morphism that produces and when composed with the two projections and respectively. But also has this property, since produces (by definition) and when composed with and respectively, and composition is associative. Therefore, they are equal.
]]>Probably? If I knew I wouldn’t have to ask. This is versus . Where brackets are pairing for , , yada yada. I know they’re the same in a cartesian category where , but I don’t know why, in categorical terms.
So you’re saying they should be equal. OK.
]]>Maybe I’m misunderstanding your notation, but doesn’t that equality simply follow from the naturality of the universal property of the cartesian product?
]]>Actually, I’m not sure about the semantics of a similar example, where the generator can be inside or outside the pair:
Dispensing with tensor projections, this could be written in two ways:
Are these actually equal? Maybe sometimes implicit -elim is just plain wrong, not tricky.
]]>For your entertainment, I’ll tell you about a tricky situation I ran into involving your tensor projections and generators, combined with -intro.
For both examples,
Example 1:
Example 2:
The problem is whether you use the generator rule on inside or outside the -intro. In example 1, you have to use it outside; in example 2, you have to use it inside the left component. But processing both examples left to right, the is first encountered in the left component, because the -elim is implicit.
I’m not sure if I’m going to handle this.
I guess there’s basically the same problem with -elim.
]]>Well, in principle both would be nice to have – one for simplicity of exposition, the other for convenience of practical use. I would say start with whichever is easier for you.
]]>To handle lollipop (internal-hom), do you want unidirectional inference with annotations on lambdas, or bidirectional typing with an optional annotation/cut rule. Do you want to require eta-long terms?
]]>