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