Re: [HoTT] A small observation on cumulativity and the failure of initiality

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

On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 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.)

Yes, that's what I'm proposing.

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

Me too.

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

Book HoTT (and HoTT in general) doesn't include any eta rules for
positive/inductive types.