From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Mon, 18 Dec 2017 03:17:46 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <4c4fe126-f429-0c82-25e8-80bfb3a0ac78@gmail.com> <11CC10D7-7853-48E7-88BD-42A8EFD47998@exmail.nottingham.ac.uk> <20171212120233.GA32661@mathematik.tu-darmstadt.de> <643DFB5A-10F8-467F-AC3A-46D4BC938E85@exmail.nottingham.ac.uk> <20171215170011.GA22027@mathematik.tu-darmstadt.de> <20171217102151.GA16619@mathematik.tu-darmstadt.de> Subject: Re: [HoTT] Impredicative set + function extensionality + proof irrelevance consistent? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_6214_352860681.1513595866355" ------=_Part_6214_352860681.1513595866355 Content-Type: multipart/alternative; boundary="----=_Part_6215_1581574217.1513595866355" ------=_Part_6215_1581574217.1513595866355 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten Altenkirch wrote= : > > > With static props, you can't prove unique choice, but it may be consisten= t=20 > as an additional primitive, or you can ensure in some other way that you= =20 > have a subobject classifier. > > =20 > > Yes, indeed. However, adding postulates to Type Theory is just a stop gap= =20 > measure because you still don=E2=80=99t have a computational interpretati= on. While=20 > we have a computational interpretation for most of HoTT, namely cubical= =20 > type theory ala Coquand et al, one might hope that there is a simpler way= =20 > to deal with the set level fragment of HoTT. > I suspect one could also come up with a type system with a computational=20 interpretation that has static props and unique choice. I was counting this= =20 possibility too as an additional primitive. > The static props approach can also be used in a dependent type system,=20 > along with unique choice or equivalent. (To say nothing of whether that's= a=20 > natural kind of system.) > > In a dependent type system, a type of static props may or may not be a=20 > universe. > > =20 > > What do you mean by =E2=80=9Cis a universe=E2=80=9D here? > Just that the type of props would be one of the built-in universes, either= =20 Russell or Tarski-style. > But if it is, you should at least have typal proof-irrelevance. (That is,= =20 > stated using equality types.) > > In that case, with equality reflection, you automatically get judgmental= =20 > proof-irrelevance.=20 > > =20 > > For equality but not for propositions in general. > I'm saying if you have typal proof-irrelevance and equality reflection, you= =20 get judgmental proof-irrelevance by reflecting the equalities between=20 proofs given by typal proof-irrelevance. =20 > > This does not necessarily mean that proofs are computationally irrelevant= .=20 > > =20 > > Now I am confused: what is the difference between judgmental and=20 > computational irrelevance? > By computationally-irrelevant proofs, I mean that terms of propositions are= =20 never needed when evaluating closed terms of non-proposition types. Like,= =20 Coq has a type of static propositions: the universe Prop. And the proofs=20 are supposed to be computationally irrelevant. This is relied upon to erase= =20 them with program extraction. From the earlier messages about Lean, it=20 sounds like Lean's proofs are also intended to be computationally=20 irrelevant. With equality reflection, irrelevance according to judgmental equality can= =20 be totally different from computational relevance. (Though it seems like a= =20 confusing and unhelpful possibility. When judgments are undecidable anyway,= =20 computationally irrelevant proofs can simply be removed from the term=20 language entirely.) ------=_Part_6215_1581574217.1513595866355 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
On Monday, December 18, 2017 at 5:10:15 AM UTC-5, Thorsten= Altenkirch wrote:


With static props, you can't prove unique choice, but it may be consist= ent as an additional primitive, or you can ensure in some other way that yo= u have a subobject classifier.

=C2=A0

Yes, indeed. However, adding postulates to Type Theo= ry is just a stop gap measure because you still don=E2=80=99t have a comput= ational interpretation. While we have a computational interpretation for mo= st of HoTT, namely cubical type theory ala Coquand et al, one might hope that there is a simpler way to deal with the= set level fragment of HoTT.


I suspect one could also come up wi= th a type system with a computational interpretation that has static props = and unique choice. I was counting this possibility too as an additional pri= mitive.


<= p class=3D"MsoNormal" style=3D"margin-left:.5in"> The static props approach can also be used in a dependent type system, alon= g with unique choice or equivalent. (To say nothing of whether that's a= natural kind of system.)

In a dependent type system, a type of static props may or may not be a univ= erse.

=C2=A0

What do you mean by =E2=80=9Cis a universe=E2=80=9D = here?


Just that the type of prop= s would be one of the built-in universes, either Russell or Tarski-style.


But if it is, you sho= uld at least have typal proof-irrelevance. (That is, stated using equality = types.)

In that case, with equality reflection, you automatically get judgmental pr= oof-irrelevance.

=C2=A0

For equality but not for propositions in general.


I'm saying if you have typal p= roof-irrelevance and equality reflection, you get judgmental proof-irreleva= nce by reflecting the equalities between proofs given by typal proof-irrele= vance.

=C2=A0

This does not necessarily= mean that proofs are computationally irrelevant.

=C2=A0

Now I am confused: what is the difference between ju= dgmental and computational irrelevance?

<= div>
By computationally-irrelevant proofs, I mean that terms of proposit= ions are never needed when evaluating closed terms of non-proposition types= . Like, Coq has a type of static propositions: the universe Prop. And the p= roofs are supposed to be computationally irrelevant. This is relied upon to= erase them with program extraction. From the earlier messages about Lean, = it sounds like Lean's proofs are also intended to be computationally ir= relevant.

With equality reflection, irrelevance according to judgmen= tal equality can be totally different from computational relevance. (Though= it seems like a confusing and unhelpful possibility. When judgments are un= decidable anyway, computationally irrelevant proofs can simply be removed f= rom the term language entirely.)
------=_Part_6215_1581574217.1513595866355-- ------=_Part_6214_352860681.1513595866355--