From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a17:902:bd42:: with SMTP id b2mr17555495plx.13.1588608473099; Mon, 04 May 2020 09:07:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:1657:: with SMTP id 84ls15852613pfw.7.gmail; Mon, 04 May 2020 09:07:51 -0700 (PDT) X-Received: by 2002:a65:6798:: with SMTP id e24mr7408380pgr.316.1588608471366; Mon, 04 May 2020 09:07:51 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588608471; cv=none; d=google.com; s=arc-20160816; b=A8evCaaAmuIbccd+u2huL+W8VQWC0yRzg3C/S4mMM24O5C9vnzUNS9CQGzLKnxYX4Q fHfyFKFF+yp4nZtfz7OJtjDsFzGi44exx68HTFbRkCVwDpnAauVoDjyl3brVjPjaQU76 y1XEgDur+KlfXXaoZ7z3WivunUt/yt5VEHh4C9FMVIbD8BMmUr8LQQL+pVrhkgck/E+M 3fwKWXvpCwV/ZnoQcEh9ZsgFNrxgVZbEDet6KWmiCwlMFMghYhdaWC45vneCsp2MHpBj MXBDn5UdeTZ5Y61VigKMJEL+o+rV2VvQqqPcYdPVP+YqOcJ8KQd8DZIee23QZjePCQa9 beMg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:cc:references:message-id:date:subject:mime-version :from:content-transfer-encoding:dkim-signature; bh=VoadFkQX4oP8Q9mS+cm+hz+yFGNniBDM2Q95fsNtlTY=; b=VX2yK3LDiEArVgXprCQ8rOHbGjIc6CfXHR4Py7nVE+LRpzY7sFvq3XlD+uZXQKK8JB g+enMg8p9+O+xTCgRYZvQpRgM6Zt0KJ/VtSih6RhusnlERgf3kreBsdvLN2eaAfWpEGy B0M6gGY1HZVwSDAO3l9vGd5Ka1KQQaSPvzu0oxNWQbooLZnDyCCKnEgWyDSTalLsV7aO pfr51KIGay0ny7BkFLngkVVXiljfVOGufO3VE91/s7zUXdA0lA5aFpjBK7or54SGpcmH a13HP/wApzoIqXLdQkm3VrzVyKaL19KTO4Iv9kM8TY19c6l27wzoK73tB3Hzdh5Ltx8G Uk1g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=CTuItIDS; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::830 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qt1-x830.google.com (mail-qt1-x830.google.com. [2607:f8b0:4864:20::830]) by gmr-mx.google.com with ESMTPS id u131si1097401pfc.6.2020.05.04.09.07.51 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:07:51 -0700 (PDT) Received-SPF: pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::830 as permitted sender) client-ip=2607:f8b0:4864:20::830; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=CTuItIDS; spf=pass (google.com: domain of steve...@gmail.com designates 2607:f8b0:4864:20::830 as permitted sender) smtp.mailfrom=steve...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-qt1-x830.google.com with SMTP id g26so10570589qtv.13 for ; Mon, 04 May 2020 09:07:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=content-transfer-encoding:from:mime-version:subject:date:message-id :references:cc:in-reply-to:to; bh=VoadFkQX4oP8Q9mS+cm+hz+yFGNniBDM2Q95fsNtlTY=; b=CTuItIDStZTg5snmDkli68nRT8WKa9wCQzjM+Q22lXnZvmmgUcx/IftbWLIa/vc1Z8 Jiy8vNzldUI2agSzeKz91ACAQZAXadtVLsX7IN0D9zTBuvAbd9c4hz6iDWYtjqtKToha VSfE+5KrqIPRUIJJQRXpQcHhx/FA0MxHjv5/GG+jbOflmEiRq+KBA9cIYeeuMIdy4F/V z6R/LcXLiwYkgt5JWLrSuP0ZYtiKESTykDKg/J/RpKdK009/cyiyNMcsQ2bsQ96DLiwK CL2wuNxLkL/ibGHLMrOUoRYSpSrS5mGBP9yywho3oKo67s8SxQ6LrJX4S5hDhYdlztKP vj0A== X-Gm-Message-State: AGi0PuaWyKSvxzxgP3jUZp921G7eCetOq/KcIkEhmcXMiU1hNKwLWOLH RXOBJ+uHEQnanRzpMMZZFeU= X-Received: by 2002:ac8:724b:: with SMTP id l11mr18729266qtp.35.1588608470495; Mon, 04 May 2020 09:07:50 -0700 (PDT) Return-Path: Received: from [192.168.1.152] (pool-74-111-173-45.pitbpa.fios.verizon.net. [74.111.173.45]) by smtp.gmail.com with ESMTPSA id h25sm10580891qto.87.2020.05.04.09.07.49 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:07:49 -0700 (PDT) Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable From: Steve Awodey Mime-Version: 1.0 (1.0) Subject: Re: [HoTT] "Identifications" ? Date: Mon, 4 May 2020 12:07:48 -0400 Message-Id: References: Cc: Stefan Monnier , Thorsten Altenkirch , "homotopyt...@googlegroups.com" In-Reply-To: To: Michael Shulman X-Mailer: iPhone Mail (17D50) I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s email ac= count. The real Thorsten went through all this with us many years ago.=20 : - ) > On May 4, 2020, at 12:00, Michael Shulman wrote: >=20 > =EF=BB=BFThe 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 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/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%= 40mail.gmail.com.