From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.202.73 with SMTP id o9mr6232938pgi.154.1488221411884; Mon, 27 Feb 2017 10:50:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.21.124 with SMTP id z57ls14512005otz.38.gmail; Mon, 27 Feb 2017 10:50:11 -0800 (PST) X-Received: by 10.13.233.70 with SMTP id s67mr7430753ywe.24.1488221411388; Mon, 27 Feb 2017 10:50:11 -0800 (PST) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id y63si1750335ywe.5.2017.02.27.10.50.11 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 27 Feb 2017 10:50:11 -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 v1RIo6hj014977 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 13:50:06 -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 v1RIo6UW014970; Mon, 27 Feb 2017 13:50:06 -0500 X-Proofpoint-Sentinel: stfjcNexU7zFAsxfSfB075TLxURZqk1j0nVYzw0ivFZeaLZTYWx0ZWRfX6fW yXb1ORtpomQOaGT8rKtXk12BK0lytajNseVOBgUG50Y7AVkpQww+U7Q9kN60blt2eLcV4Rr9weHb 3xEVB/f7NKjQ1wavPA== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v1RIo6ub014969 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Mon, 27 Feb 2017 13:50:06 -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 1ciQN4-0003tA-Hp; Mon, 27 Feb 2017 13:50:06 -0500 From: Vladimir Voevodsky Message-Id: <528245BE-80DB-4E94-A887-97D33AD30788@ias.edu> Content-Type: multipart/alternative; boundary="Apple-Mail=_F26AEF0B-E82E-4B12-9991-F1C79DBD7459" Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [UniMath] [HoTT] about the HTS Date: Mon, 27 Feb 2017 13:50:05 -0500 In-Reply-To: <12C1D5CB-D95A-4EC1-B5F9-C67F92685529@chalmers.se> 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> 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-1702270173 X-IAS-PPS-PHISH: NO --Apple-Mail=_F26AEF0B-E82E-4B12-9991-F1C79DBD7459 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > 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 -judgmenta= lly- equal. This is not what I mean by a strict set. A strict set is a Bishop set where= any two points connected by a path are judgmentally equal. --Apple-Mail=_F26AEF0B-E82E-4B12-9991-F1C79DBD7459 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
On Feb 25, 2017, at = 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote:

 =E2=80=9CBishop set=E2=80=9D which corresponds
=
to the fact that any two paths between the same end poin= ts are -judgmentally- equal.

<= div class=3D"">This is not what I mean by a strict set. A strict set is a B= ishop set where any two points connected by a path are judgmentally equal.<= /div>


--Apple-Mail=_F26AEF0B-E82E-4B12-9991-F1C79DBD7459--