From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.185.1 with SMTP id z1mr1618613pge.51.1488221613334; Mon, 27 Feb 2017 10:53:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.36.230 with SMTP id z93ls12230488ota.44.gmail; Mon, 27 Feb 2017 10:53:32 -0800 (PST) X-Received: by 10.13.212.195 with SMTP id w186mr6021150ywd.105.1488221612779; Mon, 27 Feb 2017 10:53:32 -0800 (PST) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id a202si1972389ywe.2.2017.02.27.10.53.32 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 27 Feb 2017 10:53:32 -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 v1RIrTZV016926 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 13:53:29 -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 v1RIrTmJ016920; Mon, 27 Feb 2017 13:53:29 -0500 X-Proofpoint-Sentinel: stfjO5eZYhRg16oQJcxybbZzUX1yg8pi+ddVPp92cQZ36gtTYWx0ZWRfX40G r9ChGldFcJOW9cJbrMWdy9CfpaArT6OqpzGyAvsJqa/4MFkxAvzj888sJVsU9Y4MyBXIQp2ViTUw 23TAVMrEm7hXb8IeeA== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v1RIrT4j016919 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 13:53:29 -0500 Received: from vladimirs-mbp-2.wireless.ias.edu ([172.16.158.102]) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1ciQQK-0003zL-VY; Mon, 27 Feb 2017 13:53:29 -0500 From: Vladimir Voevodsky Message-Id: <9803E33B-06CD-427D-8485-F817390ED527@ias.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_C95AC25F-84B8-4B9E-AFC6-465B7AD76C9C" Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [UniMath] [HoTT] about the HTS Date: Mon, 27 Feb 2017 13:53:27 -0500 In-Reply-To: <528245BE-80DB-4E94-A887-97D33AD30788@ias.edu> Cc: "Prof. Vladimir Voevodsky" , "univalent-...@googlegroups.com" , homotopytypetheory To: Thierry Coquand References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <12C1D5CB-D95A-4EC1-B5F9-C67F92685529@chalmers.se> <528245BE-80DB-4E94-A887-97D33AD30788@ias.edu> X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-27_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-1702270177 X-IAS-PPS-PHISH: NO --Apple-Mail=_C95AC25F-84B8-4B9E-AFC6-465B7AD76C9C Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 BTW, even if the universe of strict sets is not fibrant we can still have a= judgement that something is a strict set and the rule that a =3D b implies= a is definitionally equal to b if a and b are elements of a strict set. It is such a structure that would make many things very convenient.=20 It is non- clear to, however, why typing would be decidable in such a syste= m. Vladimir. > On Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky wrote: >=20 >=20 >> On Feb 25, 2017, at 2:19 PM, Thierry Coquand > wrote: >>=20 >> =E2=80=9CBishop set=E2=80=9D which corresponds >> to the fact that any two paths between the same end points are -judgment= ally- equal. >=20 > This is not what I mean by a strict set. A strict set is a Bishop set whe= re any two points connected by a path are judgmentally equal. >=20 >=20 --Apple-Mail=_C95AC25F-84B8-4B9E-AFC6-465B7AD76C9C Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 BTW, even if the u= niverse of strict sets is not fibrant we can still have a judgement that so= mething is a strict set and the rule that a =3D b implies a is definitional= ly equal to b if a and b are elements of a strict set.

It is such a structure that would make many= things very convenient. 

It is non- clear to, however, why typing would be de= cidable in such a system.

Vladimir.




O= n Feb 27, 2017, at 1:50 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:


On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se>= wrote:

 =E2=80=9CBi= shop set=E2=80=9D which corresponds
to the fact tha= t any two paths between the same end points are -judgmentally- equal.
=

This is not what I = mean by a strict set. A strict set is a Bishop set where any two points con= nected by a path are judgmentally equal.



--Apple-Mail=_C95AC25F-84B8-4B9E-AFC6-465B7AD76C9C--