Re: [HoTT] Re: Canonical forms for initiality

[Neel Krishnaswami <neelakantan....@gmail.com>]

Hi Mike,

Why do you prefer this style of definition to specifying the hereditary
substitution as a function (using an inductive-recursive definition)? It
seems like that would give you all the coherences you want since all
the substitution equations would hold judgmentally.[*]

I do want to see it worked out your way, now that you've told me about
it, but that's because doing the same thing two ways is usually
clarifying. However, the "obvious" way to generalize the simply-typed
presentation is with an inductive-recursive definition.

Best,
Neel

[*] I think?, since I haven't done the proofs.

On 19/10/17 20:07, Michael Shulman wrote:
> On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
>> Could you explain why you want to use normal forms and hereditary
>> substitution--rather than more typical typing rules--if you expect to need
>> an infinite tower of coherences anyway? Needing the coherence tower seems
>> like it will make the definition dramatically more complicated, so wouldn't
>> it be best to base it on the most simple and familiar typing rules?
> 
> The advantage of canonical forms and hereditary substitution is that
> the object-language judgmental equality automatically coincides with
> the metatheoretic equality, and the inductive-inductive syntax should
> simultaneously automatically form a set.  If we instead build a
> coherence tower of judgmental equalities and higher judgmental
> equalities, then we not only need to decide what that coherence
> structure should be (whereas I think the coherence structure for
> hereditary substitution should be fairly straightforward in
> principle), but prove that it is "coherent" in some sense, in order to
> enable the interpretation of raw syntax into inductive-inductive
> syntax.