From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 16 Oct 2017 06:35:34 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <01ab3701-d84a-4935-a857-84098aefddc6@googlegroups.com> In-Reply-To: <429a25c9-d331-1ee5-84d5-bafe48b3645f@gmail.com> References: <7ACEB87C-CF6E-4ACC-A803-2E44D7D0374A@gmail.com> <489BE14C-B343-49D1-AB51-19CD54B04761@gmail.com> <20171015074530.GA29437@mathematik.tu-darmstadt.de> <20171015135740.GA7845@mathematik.tu-darmstadt.de> <37664950-3045-4570-af39-5f44bfc13a1b@googlegroups.com> <429a25c9-d331-1ee5-84d5-bafe48b3645f@gmail.com> Subject: Re: [HoTT] A small observation on cumulativity and the failure of initiality MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_17656_429581888.1508160934747" ------=_Part_17656_429581888.1508160934747 Content-Type: multipart/alternative; boundary="----=_Part_17657_82894854.1508160934747" ------=_Part_17657_82894854.1508160934747 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit 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 > > ------=_Part_17657_82894854.1508160934747 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
Hi, Neelakantan.

I don't think the coherence pr= oblem of having multiple derivations of a judgment is a serious problem whe= n 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/categor= y/2017/10/vladimir_voevodsky_19662017.html#c052824)

What's this = business about commuting conversions? I don't think I've heard of t= hat.

On Monday, October 16, 2017 at 8:30:43 AM UTC-4, Neelakantan Kr= ishnaswami wrote:
On 16/10/17 0= 6:09, Michael Shulman wrote:
=C2=A0> What you call "intrinsically typed syntax" is what= I favor. =C2=A0I want
=C2=A0> initiality theorems that are proven by a straightforward str= uctural
=C2=A0> induction over something that is inductively generated, and
=C2=A0> derivations are the basic inductively generated object of a = deductive
=C2=A0> system. =C2=A0It seems most natural to me to introduce terms= as a
=C2=A0> convenient 1-dimensional notation for derivations, and depar= ting from
=C2=A0> 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
=C2=A0 =C2=A0 terms are typeable.
2. Hence, a conversion rule can be omitted, since all terms (including
=C2=A0 =C2=A0 types) are in normal form.
3. Prove a bunch of lemmas, eventually culminating in proofs of
=C2=A0 =C2=A0 (a) hereditary substitution and (b) identity expansion. (= This
=C2=A0 =C2=A0 basically ends up making normalization part of the defini= tion of
=C2=A0 =C2=A0 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
=C2=A0 =C2=A0 strength of the theory goes up and the proof of Harper an= d Pfenning
=C2=A0 =C2=A0 needs to be redone. (They exploited the fact that LF does= n't have
=C2=A0 =C2=A0 large eliminations to do a recursion on the size of the t= ype.)

=C2=A0 =C2=A0 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
=C2=A0 =C2=A0 commuting conversions.

=C2=A0 =C2=A0 This is a very complex problem, and I would want to know = if the
=C2=A0 =C2=A0 desired initiality theorem could be proved without the co= mmuting
=C2=A0 =C2=A0 conversions?

=C2=A0 =C2=A0 If memory serves, book HoTT assumes judgmental eta for pi= and sigma,
=C2=A0 =C2=A0 but not for natural numbers? What is the desired relation= between
=C2=A0 =C2=A0 judgmental equality and propositional equality at the nat= ural number
=C2=A0 =C2=A0 type?

Best,
Neel

------=_Part_17657_82894854.1508160934747-- ------=_Part_17656_429581888.1508160934747--