From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.228.196 with SMTP id n187mr13149147ywe.87.1490216476040; Wed, 22 Mar 2017 14:01:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.24.83 with SMTP id t19ls3520980ott.28.gmail; Wed, 22 Mar 2017 14:01:15 -0700 (PDT) X-Received: by 10.13.246.199 with SMTP id g190mr16823974ywf.81.1490216475646; Wed, 22 Mar 2017 14:01:15 -0700 (PDT) Return-Path: Received: from pps4.ias.edu (pps4.ias.edu. [192.16.204.92]) by gmr-mx.google.com with ESMTPS id d67si344246ywb.3.2017.03.22.14.01.15 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 22 Mar 2017 14:01:15 -0700 (PDT) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) client-ip=192.16.204.92; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps4.ias.edu [127.0.0.1]) by pps4.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v2ML195F004958 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 22 Mar 2017 17:01:09 -0400 Received: from pps4.ias.edu (pps4.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v2ML1961004952; Wed, 22 Mar 2017 17:01:09 -0400 X-Proofpoint-Sentinel: stfjNi3ZQPC7ji5O7xKaR7lERMb6QCVMf9ekBn/JJPi5rHFTYWx0ZWRfX/qz 3mw0P+z0G1rb+vuVhr6XXf3wQu7Xo2A/Ks7NLXsQybg7g9CNPjVqoc1Q9v/p8fE/PZDsZ2bFuj7o ts/u11wNAzv+ZogolQ== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps4.ias.edu with ESMTP id v2ML19L6004951 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Wed, 22 Mar 2017 17:01:09 -0400 Received: from 84.224-78-194.adsl-static.isp.belgacom.be ([194.78.224.84] helo=[172.20.5.247]) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1cqnNV-0000Xi-FY; Wed, 22 Mar 2017 17:01:09 -0400 From: Vladimir Voevodsky Message-Id: <7EFC9320-4852-469F-9609-16C27D969316@ias.edu> Content-Type: multipart/signed; boundary="Apple-Mail=_4415B3A4-2C65-426A-89F7-AA0E20C0CD64"; protocol="application/pgp-signature"; micalg=pgp-sha512 Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [HoTT] about the HTS Date: Wed, 22 Mar 2017 22:01:07 +0100 In-Reply-To: Cc: "Prof. Vladimir Voevodsky" , Matt Oliveri , Homotopy Type Theory , "univalent-...@googlegroups.com" To: Thierry Coquand References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <96ed5e86-5564-4d98-a759-5a3301968501@googlegroups.com> X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-03-22_17:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1702020001 definitions=main-1703220180 X-IAS-PPS-PHISH: NO --Apple-Mail=_4415B3A4-2C65-426A-89F7-AA0E20C0CD64 Content-Type: multipart/alternative; boundary="Apple-Mail=_A4F34E0A-8FB0-40FA-A4DC-C3AE1632004E" --Apple-Mail=_A4F34E0A-8FB0-40FA-A4DC-C3AE1632004E Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 1. As Thierry pointed out previously, the problem with sSet is that if we p= ostulate that nat:sSet, then for any (small) type T, the function type T ->= nat is in sSet, e.g. nat -> nat is in sSet. Since it is possible to construct two elements of nat -> nat the equality b= etween which is an undecidable proposition, it implies that the definitiona= l equality in any sufficiently advanced type system with sSet and nat:sSet = is undecidable. That means that witnesses, in some language, of definitional equality need = to be carried around and therefore the design of a proof assistant where th= e proof term is the proof is not possible in this system. 2. It is not so clear what would happen with only bSet and nat:bSet. Vladimir. > On Mar 22, 2017, at 5:49 PM, Thierry Coquand wrote= : >=20 >=20 > If my note was correct, it describes in the cubical set model two univale= nt universes > (subpresheaf of the first universe) that satisfy >=20 > (1) if A : sSet and p : Path A a b then a =3D b : A and p = is the constant path a > (equality reflection rule) >=20 > (2) if A : bSet and p and q of type Path A a b then p =3D q : Path A= a b > (judgemental form of UIP) >=20 > Maybe (1) or (2) could be used instead of HTS (and we would remain in an= univalent > theory, where all types are fibrant) >=20 > For testing this, one question is: can we define semi-simplicial types = in (1)? in (2)? >=20 > Best regards, > Thierry >=20 >=20 >=20 >> On 20 Mar 2017, at 16:12, Matt Oliveri > wrote: >>=20 >> So the answer was yes, right? Problem solved? >>=20 >> On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote: >> Just a thought=E2=80=A6 Can we devise a version of the HTS where exact e= quality types are not available for the universes such that, even with the = exact equality, HTS would remain a univalent theory. >>=20 >> Maybe only some types should be equipped with the exact equality and thi= s should be a special quality of types. >>=20 >> Vladimir. >>=20 >> PS If there are higher inductive types then the exact equality should no= t be available for them either. >>=20 >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeThe...@googlegroups.com . >> For more options, visit https://groups.google.com/d/optout . >=20 >=20 > -- > 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 . --Apple-Mail=_A4F34E0A-8FB0-40FA-A4DC-C3AE1632004E Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 1. As Thierry poin= ted out previously, the problem with sSet is that if we postulate that nat:= sSet, then for any (small) type T, the function type T -> nat is in sSet= , e.g. nat -> nat is in sSet.

Since it is possible to construct two elements of nat -> nat t= he equality between which is an undecidable proposition, it implies that th= e definitional equality in any sufficiently advanced type system with sSet = and nat:sSet is undecidable.

That means that witnesses, in some language, of definitional eq= uality need to be carried around and therefore the design of a proof assist= ant where the proof term is the proof is not possible in this system.=

2. It is not so clear = what would happen with only bSet and nat:bSet. 
<= br class=3D"">
Vladimir.





On Mar 22, = 2017, at 5:49 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:


If my note was correct, it describes in the cubical set mod= el two univalent universes
(subpresheaf of the first universe)  that satisfy

 (1)   if   A : sSet    and  = p : Path A a b   then   a =3D b : A  and p is the constant = path a
(equality reflection rule)

 (2)   if A : bSet and p and q of type Path A a b=   then p =3D q : Path A a b
(judgemental form of UIP)

 Maybe (1) or (2) could be used instead of HTS (and we= would remain in an univalent
theory, where all types are fibrant)

 For testing this, one question is:  can we defin= e semi-simplicial types in (1)? in (2)?

 Best regards,
 Thierry



On 20 Mar 2017, at 16:12, Matt Oliveri <atm...@gmail.com> wrote:

So the answer was yes, right? Problem solved?
On Thursday, February 23, 2017 at 9:47:57 AM UTC-5, v v wrote:
Just a thought=E2=80=A6 Can we devise a version of the HTS where exact equa= lity types are not available for the universes such that, even with the exa= ct equality, HTS would remain a univalent theory.

Maybe only some types should be equipped with the exact equality and this s= hould be a special quality of types.

Vladimir.

PS If there are higher inductive types then the exact equality should not b= e available for them either.

--
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 e= mail to HomotopyT= ypeThe...@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 e= mail to H= omotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_A4F34E0A-8FB0-40FA-A4DC-C3AE1632004E-- --Apple-Mail=_4415B3A4-2C65-426A-89F7-AA0E20C0CD64 Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename=signature.asc Content-Type: application/pgp-signature; name=signature.asc Content-Description: Message signed with OpenPGP -----BEGIN PGP SIGNATURE----- Comment: GPGTools - https://gpgtools.org iQEcBAEBCgAGBQJY0uYUAAoJEH5eMY79Hy7tZmoH/0MtyB8VQPpNMhTC/w3sqNEH pRr302Z7Omt1qk6EEkAyDPYnfh3bVQDPB8GPR1KZIJb1csBiK3vnF9mw8X1QTd1n ay0+VqJ1N4lo6k8Lr6nvAH/7Yt658B4ch8ETuZEqZAAub5z5dZOnOZgDGnuZgW2k rQnqkhFcWp+cGczobcvkWxlqfAOft9to+k60mSY06q/gh9o2ykMOrJ/tsSI4RHEv l29aIron/rOqohapvJTTcLqFV9lxTYFeeQjOhGOtzADorQDGOwl5/G85e0BmZHXr UMWoiuGMpAqMSBVfMlwwE186xMkva6hECP4VjUfHzJs23Hq5fsnrM8Eh33QDBNE= =2e4O -----END PGP SIGNATURE----- --Apple-Mail=_4415B3A4-2C65-426A-89F7-AA0E20C0CD64--