From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a50:e70a:: with SMTP id a10mr16125499edn.124.1588609295643; Mon, 04 May 2020 09:21:35 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:db4a:: with SMTP id n10ls3291576edt.4.gmail; Mon, 04 May 2020 09:21:34 -0700 (PDT) X-Received: by 2002:a05:6402:1596:: with SMTP id c22mr15886849edv.100.1588609293975; Mon, 04 May 2020 09:21:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588609293; cv=none; d=google.com; s=arc-20160816; b=K3Ba8GLKsZW1KifbO6mIo4U+or+UDWn9aqFtpmTzGRITLbIG/ZZRxBr8oDbv/1cag5 vvUND2SagXhp7cwHFln9z2xqoGR+n/zCox7TZ2LyDcY9Lkeh5TWttxv9cf7A07gxV3Ek R1Yh5PLY0f9PK0CM2hpvXhQ3ZOVxTGb2D8JUx6wTi8ngKEQsy7PMOR6V0nb0Kzu7wUfW ba+C221/gPXbCE0tTUwMTKOunOUUPjQBRwaC5u/3udbTHhYuvwTQxmpGpL+ziW+pUbww 032i7tZUmnSvXisgWrli+MNtJahtDIXaadLCr8s4F6qOPqV6W9cXIO5QXwBRgqoPLZPL LN8w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=h9Ao1q73gfHQMblkEluP7bD4H2xa85d2K1CRydswfco=; b=0zlQEwJXoj6bGgavNVYTOTOOdWmTIrqmSWroKnagg8MQdiFkFznG8YT3VJgJhx4Foo w7DIkOM2ccl7YIZFsFM+Y5GzzQcolg/6t0JXfjDfBuiUyzAw+gqLxqrmTogLDstPCW1q zi7VP/S69vMBoj5pEtt+YeJgwrfYtOspzAG/QwyC0x3DftkH5bsEhHE7ScHohZBQwgJD v+dtSFH342Fe8pw5b3p8qZmxewy0mMp7UaaANxSh2bnQuBKAT3W+6EomD6jhFv9GmZso SYy81E61O4hPtXJpHeGWN4vgn1PQDvgsW0wjq3LENCMdFNnjrJcYBo7BbXV0tAnNZgLO xFpQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=NZtHeKKe; spf=pass (google.com: domain of p.l.l...@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) smtp.mailfrom=p.l.l...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-lj1-x22e.google.com (mail-lj1-x22e.google.com. [2a00:1450:4864:20::22e]) by gmr-mx.google.com with ESMTPS id a3si627360edn.1.2020.05.04.09.21.33 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:21:33 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.l...@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) client-ip=2a00:1450:4864:20::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=NZtHeKKe; spf=pass (google.com: domain of p.l.l...@gmail.com designates 2a00:1450:4864:20::22e as permitted sender) smtp.mailfrom=p.l.l...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-lj1-x22e.google.com with SMTP id a21so10258260ljj.11 for ; Mon, 04 May 2020 09:21:33 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=h9Ao1q73gfHQMblkEluP7bD4H2xa85d2K1CRydswfco=; b=NZtHeKKefDi4N+A8y8fzqcq37bHI5a0xjZXyvFfAY086IyoLpuUZ1gH0ZLUk8K7+qi gNvQ4D3lfelDQQXtTkuA+czOHdXJPe2CfS7AgXQhxklw4IUkW1JeSgejOwIDOMdn0RA6 21vTlYGLNllqx5UfoFUCU05h7Ja4l4PiTDg3zf8PeKw/dErWryfMCZDmO+p1qhxfl9U7 WzLEE+3lvekTZ1JeTuCKU/gKsoA74iLclsf9tXQXJ5AWxchmR+EG7HBh2MxhsF1LtiGm qMBrKbn+oWVOoA8hdjW55q4mWy3+RdykosVkc/5DbvRCClVAlFOcLUqVSUyb2YM3mA9O u7FA== X-Gm-Message-State: AGi0PuZr1GGPtBmLHG8jNJoIYe2Ii3xlv2XkfbA/REnq5nqdTAx9K23Z JMI9elZqcpgPw63NZydcdO9mAQo+1tQ6k7o9v0M= X-Received: by 2002:a2e:7e0b:: with SMTP id z11mr10488151ljc.284.1588609293573; Mon, 04 May 2020 09:21:33 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Peter LeFanu Lumsdaine Date: Mon, 4 May 2020 18:21:21 +0200 Message-ID: Subject: Re: [HoTT] "Identifications" ? To: Steve Awodey Cc: Michael Shulman , Stefan Monnier , Thorsten Altenkirch , "homotopyt...@googlegroups.com" Content-Type: multipart/alternative; boundary="000000000000a16e5605a4d4ecc0" --000000000000a16e5605a4d4ecc0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Ah, I just thought the whole system was having a clock malfunction and re-sending a discussion from 2016=E2=80=A6 :-P On the serious side: one motivation for =E2=80=9Cidentification=E2=80=9D no= t yet mentioned is that it=E2=80=99s more in line with traditional mathematical usage. Say= ing that the circle defined as R/Z or as a subset of R^2 are =E2=80=9Cequal=E2=80=9D= clashes badly with the traditional mathematical usage of words, and (for at least some mathematicians) their mental picture of mathematics =E2=80=94 but saying th= at we can identify them, and that all nice properties respect such identifications, is completely consistent with traditional writing and worldviews. Also, the fact that we may identify things in multiple ways, and so have to be a little careful about how we make use of such identifications, fits with traditional intuition and practice. So saying =E2=80=9Cidentifications=E2=80=9D may require less rewiring in ou= r brains than saying =E2=80=9Cequalities=E2=80=9D or =E2=80=9Cpaths=E2=80=9D, at least in= types of algebraic structures and similar. (For synthetic homotopy theory, of course, =E2=80=9Cpaths=E2= =80=9D often fits closer to established usage.) =E2=80=93p. On Mon, May 4, 2020 at 6:07 PM Steve Awodey wrote: > I=E2=80=99m afraid that someone may have hacked Thorsten=E2=80=99s email = account. The real > Thorsten went through all this with us many years ago. > : - ) > > > > On May 4, 2020, at 12:00, Michael Shulman wrote: > > > > =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. > > > >> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier > wrote: > >> > >>> 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 identit= y > >>> type carries information. Calling it "an identification" suggests > >>> exactly the information that it carries: a way of identifying two > >>> things. > >> > >> I thought that's what "path" was for? > >> > >> > >> Stefan "who really doesn't know what he's talking about" > >> > > > > -- > > 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/msgid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOA= ZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com > . > > -- > 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/msgid/HomotopyTypeTheory/E31B538B-E0C9-4D4F-A= 4F1-4335E59CAE0D%40gmail.com > . > --000000000000a16e5605a4d4ecc0 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Ah, I just thought the whole system was having a cloc= k malfunction and re-sending a discussion from 2016=E2=80=A6 =C2=A0:-P

On the serious side: one motivation for =E2=80=9Cident= ification=E2=80=9D not yet mentioned is that it=E2=80=99s=C2=A0more in line= with traditional mathematical usage.=C2=A0 Saying that the circle defined = as R/Z or as a subset of R^2 are =E2=80=9Cequal=E2=80=9D clashes badly with= the traditional mathematical usage of words, and (for at least some mathem= aticians) their mental picture of mathematics =E2=80=94 but saying that we = can identify them, and that all nice properties respect such identification= s, is completely consistent with traditional writing and worldviews.=C2=A0 = Also, the fact that we may identify things in multiple ways, and so have to= be a little careful about how we make use of such identifications, fits wi= th traditional intuition and practice.

So saying = =E2=80=9Cidentifications=E2=80=9D may require less rewiring in our brains t= han saying =E2=80=9Cequalities=E2=80=9D or =E2=80=9Cpaths=E2=80=9D, at leas= t in types of algebraic structures and similar. =C2=A0(For synthetic homoto= py theory, of course, =E2=80=9Cpaths=E2=80=9D often fits closer to establis= hed usage.)

=E2=80=93p.

On Mon, May 4, 2020 at 6:07= PM Steve Awodey <steve...@gmail.c= om> wrote:
I=E2=80=99m afraid that someone= may have hacked Thorsten=E2=80=99s email account. The real Thorsten went t= hrough all this with us many years ago.
: - )


> On May 4, 2020, at 12:00, Michael Shulman <shu...@sandiego.edu> wrote:
>
> =EF=BB=BFThe word "path" is closely tied to the homotopy int= erpretation, and to
> the classical perspective of oo-groupoids presented via topological > spaces, which has various problems.=C2=A0 This is particularly an issu= e in
> cohesive type theory, where there is a separate "point-set level&= quot;
> notion of path that it is important to distinguish from
> identifications.
>
>> On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca>= ; wrote:
>>
>>> I don't think using "identification" necessarily= implies any
>>> difference between "identification" and "equali= ty".=C2=A0 I don't think of
>>> it that way.=C2=A0 For me the point is just to have a word tha= t refers to
>>> an *element* of an identity type.=C2=A0 Calling it "an eq= uality" 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.=C2=A0 Calling it "an identifica= tion" suggests
>>> exactly the information that it carries: a way of identifying = two
>>> things.
>>
>> I thought that's what "path" was for?
>>
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 Stefan "who really doesn't kno= w what he's talking about"
>>
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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/msgid/HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8V= VQ-yMcPvtKFtX-d9wGsD%2B2Q%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid= /HomotopyTypeTheory/E31B538B-E0C9-4D4F-A4F1-4335E59CAE0D%40gmail.com.
--000000000000a16e5605a4d4ecc0--