From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 16 Oct 2017 09:34:10 -0700 (PDT) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <527dc7a5-b3c2-44e2-9d3b-2d47dc118fcf@googlegroups.com> In-Reply-To: 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_3194_1439804705.1508171650387" ------=_Part_3194_1439804705.1508171650387 Content-Type: multipart/alternative; boundary="----=_Part_3195_2136970338.1508171650387" ------=_Part_3195_2136970338.1508171650387 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Monday, October 16, 2017 at 11:01:13 AM UTC-4, Michael Shulman wrote: > > On Mon, Oct 16, 2017 at 5:30 AM, Neel Krishnaswami > > wrote: > > 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. > I was thinking that where you'd really get in trouble is with impredicative quantifiers. From what I understand, hereditary substitutions are a variant of cut elimination, which can't directly handle impredicativity. But so far, HoTT has added impredicativity with an axiom, so maybe it'll work out somehow. Like HoTT's proof-theoretic strength would be impredicative, but its "coherence strength" would still be predicative in some weird sense. That would be a bit unnatural though, in my opinion. ------=_Part_3195_2136970338.1508171650387 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Monday, October 16, 2017 at 11:01:13 AM UTC-4, Michael = Shulman wrote:
On Mon, Oct 16, = 2017 at 5:30 AM, Neel Krishnaswami
<neelakantan....@gmail.com> wrote:
> 1. The addition of universes is an open problem. Basically the log= ical
> =C2=A0 =C2=A0strength of the theory goes up and the proof of Harpe= r and Pfenning
> =C2=A0 =C2=A0needs to be redone. (They exploited the fact that LF = doesn't have
> =C2=A0 =C2=A0large eliminations to do a recursion on the size of t= he type.)
>
> =C2=A0 =C2=A0I would be rather surprised if this couldn't be m= ade to work, though.

Me too.

I was thinking that where you'd re= ally get in trouble is with impredicative quantifiers. From what I understa= nd, hereditary substitutions are a variant of cut elimination, which can= 9;t directly handle impredicativity. But so far, HoTT has added impredicati= vity with an axiom, so maybe it'll work out somehow. Like HoTT's pr= oof-theoretic strength would be impredicative, but its "coherence stre= ngth" would still be predicative in some weird sense. That would be a = bit unnatural though, in my opinion.
------=_Part_3195_2136970338.1508171650387-- ------=_Part_3194_1439804705.1508171650387--