From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.60.99 with SMTP id u32mr12341230qte.24.1491482438763; Thu, 06 Apr 2017 05:40:38 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.27.155 with SMTP id z27ls2516575otd.14.gmail; Thu, 06 Apr 2017 05:40:38 -0700 (PDT) X-Received: by 10.157.9.153 with SMTP id q25mr4113394otd.56.1491482438341; Thu, 06 Apr 2017 05:40:38 -0700 (PDT) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id f9si215227ywh.6.2017.04.06.05.40.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Apr 2017 05:40:38 -0700 (PDT) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) client-ip=192.16.204.88; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps5.ias.edu [127.0.0.1]) by pps5.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v36CebPS020872 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 6 Apr 2017 08:40:37 -0400 Received: from pps5.ias.edu (pps5.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v36Ceb8Q020866; Thu, 6 Apr 2017 08:40:37 -0400 X-Proofpoint-Sentinel: stfj1Wz5A044Td6EjivX5s3bRIOTNonkMZAUoYs5FUFPkwFTYWx0ZWRfXzHW wwoSHmT5xsZZZqTJ/f5kTdCIKHD0nYo3MKMxi6d3h7NXgI9mg3nNd2f7Y5TZ1HxoD/hspU+nkHY6 8tj2+5C2wP9w9G4Lyw== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v36CebZJ020865 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 06 Apr 2017 08:40:37 -0400 Received: from pool-96-248-86-80.cmdnnj.fios.verizon.net ([96.248.86.80] helo=vladimirs-mbp-2.home) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1cw6iL-0007DZ-Dj; Thu, 06 Apr 2017 08:40:37 -0400 From: Vladimir Voevodsky Message-Id: <9A3B1ACD-63F0-4115-BEDB-EF1B0ECD25D2@ias.edu> Content-Type: multipart/signed; boundary="Apple-Mail=_A847B20B-5F63-44D7-A9CB-FC89AC06D8F2"; protocol="application/pgp-signature"; micalg=pgp-sha512 Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Subject: Re: [HoTT] Conjecture Date: Thu, 6 Apr 2017 08:40:37 -0400 In-Reply-To: <28122de4-b334-8c92-5281-81da31ecb50b@googlemail.com> Cc: "Prof. Vladimir Voevodsky" , Jon Sterling , HomotopyT...@googlegroups.com To: Martin Escardo References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com> <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> <28122de4-b334-8c92-5281-81da31ecb50b@googlemail.com> X-Mailer: Apple Mail (2.3273) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-04-06_11:,, 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-1704060105 X-IAS-PPS-PHISH: NO --Apple-Mail=_A847B20B-5F63-44D7-A9CB-FC89AC06D8F2 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=us-ascii I looks like like you would also need the resizing rule to place hProp into= a lower universe. Is it so? Vladimir. > On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory wrote: >=20 >=20 >=20 > On 06/04/17 01:23, Jon Sterling wrote: >> I am curious, does this development use univalence except to establish >> functional extensionality and propositional extensionality? The reason I >> ask is, I wonder if it is possible to do a similar development of >> computability theory in extensional type theory and get analogous >> results. Additionally, I am curious whether you have found cases in >> which univalence clarifies or sharpens this development, since I'm >> trying to keep track of interesting use-cases of univalence. >=20 > Currently the only place that uses univalence is the equivalence of > (X->Y) with the type of single-valued relations X->Y->U. (This was > proved by Egbert in his mater thesis.) >=20 > But another point, compared with previous developments in topos logic > an extensional type theory, is that a number of things work as they > should for types more general than sets by replacing > subobject-classifier-valued functions by universe-valued functions. >=20 > An example is this: Consider the lifing in its representation with > subsingletons >=20 > L(X) =3D (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). >=20 > If we replaced U by Prop in this definition, this wouldn't work well > for types that are not sets. >=20 > For example, if X is the circle, any function into a set, and hence > any function into Prop, is constant, and so L(X) would be > contractible. >=20 > However, with the definition as it is, with U, we always have that X > is embedded into L(X), even if X is not a set. >=20 > The same phenomenon applies to the equivalence of (X->Y) with the type > of single-valued relations X->Y->U discussed above, but this > additionally requires univalence. >=20 > Martin >=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=_A847B20B-5F63-44D7-A9CB-FC89AC06D8F2 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 iQEcBAEBCgAGBQJY5jdFAAoJEH5eMY79Hy7tvyUH/2S/WbnS2lN/UfiL6JXbrJTM QsQH6t7qA5Mc0TR4J5HB/QxUC3vw8mSfyXfyM6KGaailiASTlgQhoAdqAlK4xTRG xbJx1uimaEI6rnlybc1g1khZKlxg2A7NEJnccUHZDOMRAbLQsZzrSfB9q1OEQG9X EjBtVSGcQvL+HRh6itNcYuBb8ziSBtAMEERfUa29QXiWNGyPHyp1mkxgXW7HYep1 IfaVg64ePnL3ch9t3stVRpcfLTXiyGLxXj6Q+oqeRpfuUfHTN1ASqRvtoDavENll uUEwxzidHzGSffuFPrvPfjzqumJ9blWwBUTlKHo7DRxyC3/e7iVCtDU9TxVmLCU= =K47W -----END PGP SIGNATURE----- --Apple-Mail=_A847B20B-5F63-44D7-A9CB-FC89AC06D8F2--