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:
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.