Re: [HoTT] Re: Canonical forms for initiality

[Andrea Vezzosi <sanz...@gmail.com>]

To maybe add a third way: you can define the graph of hereditary
substition as a proposition if you have already proven judgmental
equality is decidable.

Let me write "Γ ⊢ e : A" for the typing judgment where Γ, e, and A are
not necessarily in normal form, and "(e , d) [[ σ ]]" for
type-preserving non-hereditary substitution for a typing derivation d.

Defining hereditary substitution mutually with the syntax seems like a
huge task to me because it involves a proof that your language is
normalizing, and I wouldn't want to convince any I-R schema that the
whole construction is well-founded.

However if one first proves that judg. equality is decidable for "Γ ⊢
e : A"[1], then we can define

t1 [ σ ] = t2 := isTrue (decideEq ((U-term t1) [[ U-subst σ ]]) (U-term t2))

where U is a function defined by I-R which converts normal form
judgments back into expressions and typing judgments; for both terms,
types, contexts and substitutions:

U-term : Γ ⊢ A → Σ (e : Expr). fst (U-cxt Γ) ⊢ e : fst (U-type A)

After the fact It should then be possible to show that the normal form
judgments are a set, and then define an actual substitution function.

However I don't know if this construction would still satisfy what we
want out of a type of normal forms? Would that be an initiality
theorem for a class of models? What class?

Best,
Andrea

[1] Like here https://github.com/mr-ohman/logrel-mltt , but I'd expect
a proof with intrinsic typing like https://arxiv.org/abs/1612.02462 to
also work.










[1] https://github.com/mr-ohman/logrel-mltt

On Fri, Oct 20, 2017 at 1:16 PM, Michael Shulman <shu...@sandiego.edu> wrote:
> 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.
>
> --
> 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.