From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:620a:16db:: with SMTP id a27mr14979967qkn.116.1588598233661; Mon, 04 May 2020 06:17:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:51c4:: with SMTP id d4ls9544899qtn.9.gmail; Mon, 04 May 2020 06:17:12 -0700 (PDT) X-Received: by 2002:ac8:735a:: with SMTP id q26mr16941061qtp.233.1588598232482; Mon, 04 May 2020 06:17:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588598232; cv=none; d=google.com; s=arc-20160816; b=NsRW/TEqzf5prenz60/QPHNhsaWV/rwKgUwXyaCB6ejbV6rSIaHpRsdHzS90ZIc00p nVRkzsqi4zI7kc6CDfZMV0bDtBWOhKtldydMVvRT4GtM+FdX15WkYwrMtm738KQ6Oo/g B1cV3SNhrN5TfsDLQLnYvCiPeESxJJ66u1poT2vgec/8GtbOt19iuuPuF4iLQcvxxSBw 3Mb/A6OO/fTeXKdQlx3WW+BoPuzKua3g5uUzW502MfE1tD+gs1t+ou3vAxw8QuKqJA4o 2pOcEKRzwdoVKHsD1dsqO5Zh2Hib2xcfriP3/4sW7L95zt+uaFC132lVL84GMiEhMYXd tgxg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=QYyTaoKfmE5umYtEb0fxJpMfoJ6Qm3VaablVwOK8vf8=; b=k/BvZd2S+hEpwT9+OqMhFwp1nMwpKlMv3ZzlZwwAmyJ+/Lag5RT5kqx78YTnJLouy0 a6OYM41CL1WSdj7NE+C4A2/jpRuCIkV3AEHQQxrqbmDQH5HUG3YAI+BKoAFg69/0aY+p 0Ac4kpcWBb/qCkOguV09NNLvR44qHkUjhlGIZWMNbvbRHP7eLl0gJGI7DfCbG6cmMhqa 48+SVdFnCsCgX+6YY1qketMVDnvbW0OlI+FwuIxiDl2rBege2bSX+oz/MclD/Igk0dTd /sziXo9KtQBs9KnTj67BrDsm5/WkCj6ILkqILB2QCZhSuRiZyIdOb+a8p9qUZQDyTA37 h9TA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WaeZazys; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Return-Path: Received: from mail-ot1-x336.google.com (mail-ot1-x336.google.com. [2607:f8b0:4864:20::336]) by gmr-mx.google.com with ESMTPS id l23si782824qkl.0.2020.05.04.06.17.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 06:17:12 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) client-ip=2607:f8b0:4864:20::336; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WaeZazys; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::336 as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x336.google.com with SMTP id z25so8739424otq.13 for ; Mon, 04 May 2020 06:17:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=QYyTaoKfmE5umYtEb0fxJpMfoJ6Qm3VaablVwOK8vf8=; b=WaeZazysBEodDZwbbtH9sVsylMEwUOImMuabbgnTpOEa1Oby3/iYO8EyWQcnVhdsEG lmfbZmVkBOYrkcxjUrAleab77O0wjPkY0/lk10+B17oYETlxXSzLddntvZwWJgcFuXhe l9sKkxzI1dTqVUv7dKs98/tsVUgca5RTByO04/SKKP+ZBMEHbJJFVXCtaC2d5wMuI1jE 7srygL4h5jtkmoCu2d5tl7E7ZuBH2AZIx9sGXmYrGQMwu+3uhc2GKx3MJtBLRAtNf1dh eNITudTwCPH4y4PrgKIvwd4eSb4DS9p2qbzXqntkCw9ue6ekKiGCd4/xYIOsi1ysLIon tDWA== X-Gm-Message-State: AGi0PuaPa8zd6E70WDFIy2ThwxEoiyKSA3c4B+ckl8yfk4YD0X1XzzfR 92oLNklAiInJWJc0Q+5VCqRwAtb3skQ6I9YW3ksNqEcMBSfNNgGTgnX1NeKLEYUcZTq00KBPyrb xxhZcra5j/FQJbHLsPABMBOctB1vHqzploQ8iXol3LFaxpFqNy/IPBLG3Mv7LmsASIOeWzpQyl2 11fSSmFKc+ X-Received: by 2002:a9d:7d91:: with SMTP id j17mr13880335otn.342.1588598230628; Mon, 04 May 2020 06:17:10 -0700 (PDT) Return-Path: Received: from mail-ot1-f51.google.com (mail-ot1-f51.google.com. [209.85.210.51]) by smtp.gmail.com with ESMTPSA id k19sm3229354oof.33.2020.05.04.06.17.09 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 06:17:10 -0700 (PDT) Received: by mail-ot1-f51.google.com with SMTP id m18so8772485otq.9 for ; Mon, 04 May 2020 06:17:09 -0700 (PDT) X-Received: by 2002:a9d:170e:: with SMTP id i14mr14603278ota.283.1588598229600; Mon, 04 May 2020 06:17:09 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Mon, 4 May 2020 06:16:57 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] "Identifications" ? To: Thorsten Altenkirch Cc: "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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. On Mon, May 4, 2020 at 2:35 AM Thorsten Altenkirch wrote: > > I am just reading a paper which uses the word =E2=80=9CIdentification=E2= =80=9D instead of equality. I think this has been proposed by Bob Harper. C= an anybody enlighten me what is the difference between identifications and = equality? Maybe there is an identification between them but they are not eq= ual? Are the real numbers 0.999=E2=80=A6 identified or are they equal? > > > > Thorsten > > 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. > > 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 > where permitted by law. > > > > -- > 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/BBC0B8F3-AB16-4196-B9B9-B1B3031B2D7D%40nottingham.ac.u= k.