From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.50.5 with SMTP id y5mr8462278pfy.4.1487886360990; Thu, 23 Feb 2017 13:46:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.137.37 with SMTP id l37ls1461988iod.41.gmail; Thu, 23 Feb 2017 13:46:00 -0800 (PST) X-Received: by 10.99.113.76 with SMTP id b12mr14159506pgn.162.1487886360180; Thu, 23 Feb 2017 13:46:00 -0800 (PST) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id f187si622601ywc.0.2017.02.23.13.45.59 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 13:46:00 -0800 (PST) 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 v1NLjv4d029245 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 23 Feb 2017 16:45:57 -0500 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 v1NLjtlC029234; Thu, 23 Feb 2017 16:45:57 -0500 X-Proofpoint-Sentinel: stfj1s+G2wfLrZH50ewfi9Fb9TdyHUItR0jQjpzvTHYoxxxTYWx0ZWRfX78w 90MwxPlpC3uyjllqQYmOqBPJHzKF4amEWtfkxYCczGC+q65cQK9ZqSOInitw5KWwBLdw9dvo+8WE SveD84DiiPkn9IftsA== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v1NLjs0I029231 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Thu, 23 Feb 2017 16:45:55 -0500 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 1ch1D0-0007Qs-Kq; Thu, 23 Feb 2017 16:45:54 -0500 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [HoTT] about the HTS From: Vladimir Voevodsky In-Reply-To: <29b2bdf5-3838-a268-5a44-4aea998cb878@gmail.com> Date: Thu, 23 Feb 2017 16:45:55 -0500 Cc: "Prof. Vladimir Voevodsky" , Univalent Mathematics , Paolo Capriotti , homotopytypetheory Content-Transfer-Encoding: quoted-printable Message-Id: <4796BE9D-E759-4F57-A3AB-8F8808C01D76@ias.edu> References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <484524d2-4054-5b7a-14af-e68a8e4b8375@gmail.com> <91160F61-2A67-4B1F-9A4A-F3510B99E9D3@ias.edu> <29b2bdf5-3838-a268-5a44-4aea998cb878@gmail.com> To: Benedikt Ahrens X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-23_14:,, 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-1612050000 definitions=main-1702230193 X-IAS-PPS-PHISH: NO BTW It is a little dangerous to define presheaves as functors C -> Sets^{op= }. While it gives the correct objects, the morphisms between presheaves are= not morphisms in the category of functors C -> Sets^{op} but in the opposi= te category. > On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens wrote= : >=20 > Section 1.4.8 "Equality" gives an informal account and points to several > precise definitions. > On page 43 two equality types are considered, one intensional one and > one with reflection rule. >=20 > Maybe Paolo (in CC) can explain his setup himself. >=20 > On 02/23/2017 07:08 PM, Vladimir Voevodsky wrote: >> I could not find where he defines the univalent (intensional) >> equality. It seems that all his equalities are strict. >>=20 >>=20 >>> On Feb 23, 2017, at 9:57 AM, Benedikt Ahrens >>> wrote: >>>=20 >>>=20 >>>=20 >>> On 02/23/2017 03:47 PM, Vladimir Voevodsky wrote: >>>> Just a thought=E2=80=A6 Can we devise a version of the HTS where exact= =20 >>>> equality 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 this should be a special quality of types. >>>>=20 >>>> Vladimir. >>>>=20 >>>> PS If there are higher inductive types then the exact equality >>>> should not be available for them either. >>>=20 >>>=20 >>> Paolo Capriotti, in his PhD thesis "Models of Type Theory with >>> Strict Equality" [1], has studied strict equality in type theory. >>>=20 >>>> From page 69: >>>=20 >>> "Finally, universes in the strict fragment of our system are not >>> assumed to be fibrant types, like in HTS." >>>=20 >>> You might be interested in Section 4.1.1, "Differences with HTS". >>>=20 >>> [1] https://arxiv.org/abs/1702.04912 >>>=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. >>=20 >=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.