Re: [HoTT] Re: Canonical forms for initiality

[Michael Shulman <shu...@sandiego.edu>]

Good question!  I can think of three reasons:

1. We still don't know whether inductive-recursive definitions make
sense homotopically.
2. In my limited experience, inductive-inductive definitions generally
have more powerful induction principles than inductive-recursive ones.
In particular, it's much less clear to me that with an
inductive-recursive definition we could map out of it into any
(oo,1)-category.
3. I'm less confident than you that the inductive-recursive case would
be easier.  My experience with this sort of thing leads me to believe
that it's like playing whack-a-mole: if you think you solve the
coherence problem in one way then it pops up somewhere else.  But
someone should try it!

Mike

On Fri, Oct 20, 2017 at 3:57 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 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.
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.