From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:a405:: with SMTP id p5mr164231plq.36.1588611244292; Mon, 04 May 2020 09:54:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:90b:3657:: with SMTP id nh23ls106877pjb.1.canary-gmail; Mon, 04 May 2020 09:54:02 -0700 (PDT) X-Received: by 2002:a17:902:b614:: with SMTP id b20mr103881pls.217.1588611242455; Mon, 04 May 2020 09:54:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588611242; cv=none; d=google.com; s=arc-20160816; b=CIrvmKWsmsDAtOFYTIpAOBgS5N/MaeuosVT2l6lnYWqksrhqDGCaKMSQ/GMB6jaxct U5g1HubpBafEbr3daabRQc9d9gJzV1/52axBiRKSmRWIu/n7Qp50BVdUwVO2We96eRK/ WHtg0BC36Eeb+ghmy+gW1N6QC56jS5AAdhAO/6ZoiYHEP2Gx6mBEr0x/8hsafzKeL/0o S99j6NpI/EabvAcpfTc6VC8SB1XObWgnszezmx7yel5oTftsN0ecGAjVsdAa1gjvhgep Z+yk4ila0R0BgYcUQPRAqr9leK3cMkLcXESHeoGNGL6Y67/vnKw2kWGmiHZHS/RyFEA4 qoTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:subject:mime-version:from:sender:dkim-signature; bh=0/Zkzmm+39qa3CeVO8D+EXA8Z35bNh8FcZy7hWg2y1U=; b=j6zVFTgwDuO8dizc3izzWvAdKPs9udi7b+7oTudwv4yDhJ42HcaLh9v3eFzyvvP0U7 umPaYvEU006n6WAi+G0AFVVtJapZdEkoRtV99gttpH74DoXe0beFQCRZymJfIXw7yLuZ FswuWY7KTYPqHNc/WIcvqxNi8C3+lhDVntRttyF0Y2HVSzFaYJvXna2eaa2r4qmazEeK bbOe5sJUfyKxKRCAJSm28yn3+pFqjlivAOKmjqXtjWPu+jtfMUp1MZr52CMHinZWgA1H 8dEUR8+dIQrZ3Of/QlT2MqmTcCgBMdg+Nqf9uUQuIBqaDk/Z3EjtS2eQKLlOx487W6/v ZoBw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@andrew-cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=q9H1p5oU; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::736 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Return-Path: Received: from mail-qk1-x736.google.com (mail-qk1-x736.google.com. [2607:f8b0:4864:20::736]) by gmr-mx.google.com with ESMTPS id u131si1108698pfc.6.2020.05.04.09.54.02 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:54:02 -0700 (PDT) Received-SPF: pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::736 as permitted sender) client-ip=2607:f8b0:4864:20::736; Authentication-Results: gmr-mx.google.com; dkim=pass head...@andrew-cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=q9H1p5oU; spf=pass (google.com: domain of awo...@andrew.cmu.edu designates 2607:f8b0:4864:20::736 as permitted sender) smtp.mailfrom=awo...@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: by mail-qk1-x736.google.com with SMTP id n14so178658qke.8 for ; Mon, 04 May 2020 09:54:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=andrew-cmu-edu.20150623.gappssmtp.com; s=20150623; h=sender:from:mime-version:subject:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; bh=0/Zkzmm+39qa3CeVO8D+EXA8Z35bNh8FcZy7hWg2y1U=; b=q9H1p5oUq9jUX68TS7/Kt/rf5WXvlIXv02FUsbuO5HJS772IlwNJKKNPgVWVMTLCAF d48SYGA6Hgp4Hw/cXVVJDuZ85FOH3fKQPkHk3Upq/oKB19KLcl1/yy2dFN/+iv2Xq9hk PKf5rBz1aKTfw9AfLNO/GJc27C8y60gcWs7dZjjjFv39gygriqzkKxZ1+YlvMyb29oL7 yxjLn/4KfKliusbgX4ZcLH+KNXtQ0rXY4fGYfTpsVj4SL9ASe0o4fOEtGrn1K+yCojVF doTkWPTHUIFouppaNZ2hc+6yr765TcA6Iu1e3WmqXuvC4KLeJ4MUe3DAgGXtqKEYS3Qj CQiQ== X-Gm-Message-State: AGi0Puacn6I+OGbw3rXMnCx11dDJfy4TsVktNptbZCudssHtZrNut0uk a+RAkzsxwVvq9nN/0HeGpMtZ+w== X-Received: by 2002:a37:7b01:: with SMTP id w1mr88756qkc.167.1588611241286; Mon, 04 May 2020 09:54:01 -0700 (PDT) Return-Path: Received: from [192.168.1.13] (pool-74-111-173-45.pitbpa.fios.verizon.net. [74.111.173.45]) by smtp.gmail.com with ESMTPSA id g123sm10467622qkd.95.2020.05.04.09.54.00 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 04 May 2020 09:54:00 -0700 (PDT) Sender: Steven Awodey From: Steve Awodey Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.5\)) Subject: Re: [HoTT] "Identifications" ? In-Reply-To: Date: Mon, 4 May 2020 12:53:59 -0400 Cc: Michael Shulman , Stefan Monnier , "homotopyt...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <14AEC162-00A7-41E5-88EF-11501EF7C2AB@gmail.com> References: To: Thorsten Altenkirch X-Mailer: Apple Mail (2.3445.9.5) > On May 4, 2020, at 12:17 PM, Thorsten Altenkirch wrote: >=20 >=20 > I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s ema= il account. The real Thorsten went through all this with us many years ago.= =20 > : - ) >=20 > One of our dogs gained access to my laptop - sorry. These animals can be = very awkward. >=20 > However, even the real Thorsten had a friendly argument with Andre Joyal = when we were writing the book about whether to use =3D for the equality typ= e.=20 I remember that conversation.=20 I think we decided to put the question =E2=80=9Cwhat does x=3Dy mean?=E2=80= =9D aside,=20 until we had taken care of more important things. So is it time now? Steve >=20 > Thorsten >=20 > =EF=BB=BFOn 04/05/2020, 17:08, "Steve Awodey" wrote: >=20 > I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s ema= il account. The real Thorsten went through all this with us many years ago.= =20 > : - ) >=20 >=20 >> On May 4, 2020, at 12:00, Michael Shulman wrote: >>=20 >> The word "path" is closely tied to the homotopy interpretation, and to >> the classical perspective of oo-groupoids presented via topological >> spaces, which has various problems. This is particularly an issue in >> cohesive type theory, where there is a separate "point-set level" >> notion of path that it is important to distinguish from >> identifications. >>=20 >>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier = wrote: >>>=20 >>>> I don't think using "identification" necessarily implies any >>>> difference between "identification" and "equality". I don't think of >>>> it that way. For me the point is just to have a word that refers to >>>> an *element* of an identity type. Calling it "an equality" can have >>>> the wrong connotation because classically, an equality is just a >>>> proposition (or a true proposition), whereas an element of an identity >>>> type carries information. Calling it "an identification" suggests >>>> exactly the information that it carries: a way of identifying two >>>> things. >>>=20 >>> I thought that's what "path" was for? >>>=20 >>>=20 >>> Stefan "who really doesn't know what he's talking about" >>>=20 >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyT...@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q= %40mail.gmail.com. >=20 >=20 >=20 >=20 > This message and any attachment are intended solely for the addressee > and may contain confidential information. If you have received this > message in error, please contact the sender and delete the email and > attachment.=20 >=20 > Any views or opinions expressed by the author of this email do not > necessarily reflect the views of the University of Nottingham. Email > communications with the University of Nottingham may be monitored=20 > where permitted by law. >=20 >=20 >=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 HomotopyT...@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/D83C2B3E-AF61-409B-BE3A-A98839A00CF6%40nottingham.ac.u= k.