Hi, Neelakantan.

I don't think the coherence problem of having multiple derivations of a judgment is a serious problem when working in a set-level theory. But I think Mike's planning ahead for what will generalize to initiality theorems internal to HoTT. He has talked about the possibility of using hereditary substitutions, and interpreting only normal forms. (Recently, actually: https://golem.ph.utexas.edu/category/2017/10/vladimir_voevodsky_19662017.html#c052824)

What's this business about commuting conversions? I don't think I've heard of that.

On Monday, October 16, 2017 at 8:30:43 AM UTC-4, Neelakantan Krishnaswami wrote:

On 16/10/17 06:09, Michael Shulman wrote:
 > What you call "intrinsically typed syntax" is what I favor.  I want
 > initiality theorems that are proven by a straightforward structural
 > induction over something that is inductively generated, and
 > derivations are the basic inductively generated object of a deductive
 > system.  It seems most natural to me to introduce terms as a
 > convenient 1-dimensional notation for derivations, and departing from
 > that is what causes all the problems.

For this to be true, it seems like you would want to arrange that there
is at most one derivation of judgmental equality for any pair of terms.

What leads me to this reading is the idea that if there are multiple
possible derivations of judgemental equality (for instance, if
conversion contains the symmetry rule), then you have to prove a
coherence theorem, which is what you seemingly to want to avoid.

This doesn't seem *impossible*, but it does seem challenging. A
plausible line of attack:

1. Give bidirectional typing rules to ensure only beta-normal, eta-long
    terms are typeable.
2. Hence, a conversion rule can be omitted, since all terms (including
    types) are in normal form.
3. Prove a bunch of lemmas, eventually culminating in proofs of
    (a) hereditary substitution and (b) identity expansion. (This
    basically ends up making normalization part of the definition of
    substitution.)

This seems plausible, since Harper and Pfenning worked it out in the
case of LF, but there are two outstanding issues, in order of
difficulty:

1. The addition of universes is an open problem. Basically the logical
    strength of the theory goes up and the proof of Harper and Pfenning
    needs to be redone. (They exploited the fact that LF doesn't have
    large eliminations to do a recursion on the size of the type.)

    I would be rather surprised if this couldn't be made to work, though.

2. The beta-eta theory of sum types (and naturals numbers) involves
    commuting conversions.

    This is a very complex problem, and I would want to know if the
    desired initiality theorem could be proved without the commuting
    conversions?

    If memory serves, book HoTT assumes judgmental eta for pi and sigma,
    but not for natural numbers? What is the desired relation between
    judgmental equality and propositional equality at the natural number
    type?

Best,
Neel