From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.237.197 with SMTP id w188mr121071ywe.2.1510091424034; Tue, 07 Nov 2017 13:50:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.13.225.140 with SMTP id k134ls1044098ywe.31.gmail; Tue, 07 Nov 2017 13:50:23 -0800 (PST) X-Received: by 10.129.96.69 with SMTP id u66mr113880ywb.224.1510091423248; Tue, 07 Nov 2017 13:50:23 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1510091423; cv=none; d=google.com; s=arc-20160816; b=RPaPvj0gZw8BdUOu+9ae8prpZWIf357DbTU+e9rqGql/X1CCh4wM+haxUVz1FDFsJl 3IWkn21wx938kk+JHVee5y/kfhQxSWP/xWxYEpsucAJmiuw9BRcMWapc2KM8Yuj876lE WNdKui2pjLm2Cw4cY9ibnzmKjXpbImTCNg2tH8NG+6xLm48LkCGrSDmT/xY9jIL+GhW5 2w9Qvo9FcUfTqbutl7bnN6BLKjIQrQ8xpp5PBa4ozdyaNQZQApyq6ja0ZckPPtSXbc8l hmbQKPpMIUTHsQmzQn70IxLJInKJWrFsdLIhA0PbkHMEUiwdM2dBQ8JtgT5RIjQyQdW9 6uDg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:cc:date:in-reply-to:from:subject :mime-version:arc-authentication-results; bh=kY5WKi14kO8sVe4fxUrAen8w/W5UbB2Mt7R+jdFgIuo=; b=FYyT+9YSa5QmIpjHmGXvB5mJ4RN32YnDUdn6c8E8Zk19y5IhQfXFZItEv+RZxJerOB UkkaC+VInPYjHAZeVMZW00xg/DCHyjKyM0uaydWZNqi85aFZoaiRhSfHRt4WyTCZhjfd ZWS9mw54TVc4KG+xEX0en6x/Gkav2fyDtSnKpKIGIoOqd0UEbHerF+eYmLvJ85fVRI9w 1zoBtnudZX0eufC0hIbvPDdox6akKLrXxI+z0VA+F9EHIZL6rn0jTLJRtnmYwqlmPO0g AcmGlDtM43JsvCCpPOfSIcZfO8lzNdNr6ZEolb2nR1fGKm+9AHZRSbTyYJT5ac0EI2qX y1pg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Return-Path: Received: from Princeton.EDU (ppa02.Princeton.EDU. [128.112.128.216]) by gmr-mx.google.com with ESMTPS id a13si221711ywe.0.2017.11.07.13.50.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 07 Nov 2017 13:50:23 -0800 (PST) Received-SPF: pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) client-ip=128.112.128.216; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of dtse...@princeton.edu designates 128.112.128.216 as permitted sender) smtp.mailfrom=dtse...@princeton.edu Received: from csgsmtp203l.Princeton.EDU (csgsmtp203l.Princeton.EDU [140.180.223.156]) by ppa02.princeton.edu (8.15.0.59/8.15.0.59) with ESMTPS id vA7LoM25016223 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT) for ; Tue, 7 Nov 2017 16:50:22 -0500 Received: from mac-e0accb9c0fda.home (pool-96-239-83-148.nycmny.east.verizon.net [96.239.83.148]) (authenticated authid=dtsement bits=0) by csgsmtp203l.Princeton.EDU (8.14.4/8.12.9) with ESMTP id vA7LoLxF010381 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NOT); Tue, 7 Nov 2017 16:50:22 -0500 Content-Type: multipart/alternative; boundary="Apple-Mail=_5A1DEACA-EB1A-4742-B322-1821996375F4" Mime-Version: 1.0 (Mac OS X Mail 8.2 \(2104\)) Subject: Re: [HoTT] Voevodsky obituary in Nature From: Dimitris Tsementzis In-Reply-To: <28b492f0-3d0f-4744-9a67-99bf24eae91c@googlegroups.com> Date: Tue, 7 Nov 2017 16:51:13 -0500 Cc: Homotopy Type Theory Message-Id: <19E2F9D6-5BAE-4E4D-B262-B2CBB5A356C5@princeton.edu> References: <28b492f0-3d0f-4744-9a67-99bf24eae91c@googlegroups.com> To: "Daniel R. Grayson" X-Mailer: Apple Mail (2.2104) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-11-07_07:,, signatures=0 X-Proofpoint-Spam-Details: rule=quarantine_notspam policy=quarantine score=0 spamscore=0 suspectscore=8 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1707230000 definitions=main-1711070285 --Apple-Mail=_5A1DEACA-EB1A-4742-B322-1821996375F4 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Dan, It is an interesting idea to refer to univalence as a =E2=80=9Cmechanism=E2= =80=9D rather than an =E2=80=9Caxiom=E2=80=9D. Even if you did it for expository reasons, I believe that in certain contex= ts it is a good phrase to adopt. Dimitris > On Nov 7, 2017, at 16:40, Daniel R. Grayson wro= te: >=20 > See https://www.nature.com/articles/d41586-017-05477-9 >=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=_5A1DEACA-EB1A-4742-B322-1821996375F4 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
Da= n,

It is an interesting idea to r= efer to univalence as a =E2=80=9Cmechanism=E2=80=9D rather than an =E2=80= =9Caxiom=E2=80=9D.

Even= if you did it for expository reasons, I believe that in certain contexts i= t is a good phrase to adopt.

<= /div>
Dimitris

O= n Nov 7, 2017, at 16:40, Daniel R. Grayson <danielrich...@gmail.com> wrote:

See https://www.nature.com/articles/d41586-017-05477-9

--
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=_5A1DEACA-EB1A-4742-B322-1821996375F4--