From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6830:14d6:: with SMTP id t22mr16221559otq.323.1588624734451; Mon, 04 May 2020 13:38:54 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a4a:b4c7:: with SMTP id g7ls7197ooo.3.gmail; Mon, 04 May 2020 13:38:53 -0700 (PDT) X-Received: by 2002:a4a:e83d:: with SMTP id d29mr143787ood.46.1588624732929; Mon, 04 May 2020 13:38:52 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588624732; cv=none; d=google.com; s=arc-20160816; b=zifv/6HPPf/YoWfhClbH/4MLcj0OWMRBm9YpqjXy6JUZtbc/fHQR0fLHGaZQKJC1PW hMGENi8vPVtXCydy2/2Oc639YboJ91Dc+xrBW8wkjDQR/jZ7m478pvJO3SeMOBvxcRET 0aTd5DEqYznNDNWZuj2Z/2nsfd80PK1E2NnC8bYFpHYij55zGVgPyVkaoFNdT1mCODIY VdmYnUYyQdbtEb47ZYSReD+Y6yjiRdGzaPNYMFLzvQ4G19gqitTp24NMqhKqiCa7CQlM uJwYGYF0pPECaqIwH2dwH6xEmVkueVFhQXD6Tn7sXQgjtntQ1laBzM01Y710il1equok T27w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=54kVdnb24hTKEI4+TtfTq6K7/AqD0M6pOtP3m13bxwk=; b=d18UWe24z8nUGNEdCX5xmBlACdXeiGp/MooLeRbr6PJQgr0KTQzTC/nl+Tdk17Jd8J AK/v/FIoIvDZnRKOJ0yOZYgyq6uKIqMqv/pC+oL7n8WskVSighf97XZWFCGLR5k03wIp ApZtNKxcWad+L5Afg02W8f9m2/5oud0uHuzbvu0sKOQgpKdNuyMFedJRlhTFSvirblzx tMKEcYQfn78tUu9BELTEDAxEsckeD/6vjg2jYha2MceGFU74znVb9CC15ji5SzUsxSy8 xo2xJM4urpUS3lYtznTcG2Z18SCdHqqZSBc3kBVDIE/cSiT/T9Vsz6BDSTVtqjwwIi69 MAhA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id h17si12050otk.1.2020.05.04.13.38.52 for ; Mon, 04 May 2020 13:38:52 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: TrMVAJBjkghTwEkYWnkzuKXI3h6hsaxmzSaLHYnWEyNs4KraUrTe7a8Zv2TVMgCrpvNrSRuMlg JLF2PXi+hhJbr+3uxLiumMYw/iH+kHXAtJv5QDNMG+RpVZuqGZrQXKVWx20Mu/e4UjkExaqCzS vcKjaJoqzvQss+sogDzG4vHBQL+JUYT/oG2eIvVon+iregnlulBBgsxz8miT5YRl1ehN+g181E vn9JDT5cT0NlbePP/vNeMUBbmK+IiE2ttDCknKCIBudYSYI5kAgul02LqTYRwriESL0IEQRELI Gd8= X-IronPort-AV: E=Sophos;i="5.73,353,1583211600"; d="scan'208";a="10119558" Received: from unknown (HELO Billet.gst.uqam.ca) ([132.208.216.73]) by mail6.uqam.ca with ESMTP; 04 May 2020 16:38:52 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Billet.gst.uqam.ca ([169.254.5.38]) with mapi id 14.03.0439.000; Mon, 4 May 2020 16:38:51 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Michael Shulman , Stefan Monnier CC: Thorsten Altenkirch , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] "Identifications" ? Thread-Topic: [HoTT] "Identifications" ? Thread-Index: AQHWIiMSjXqlf/k7YUmG/+lTb1bxCKiYWNmA//+9QrmAAEmdQA== Date: Mon, 4 May 2020 20:38:50 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F3F8C@Pli.gst.uqam.ca> References: ,,<8C57894C7413F04A98DDF5629FEC90B1652F3F0F@Pli.gst.uqam.ca> In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F3F0F@Pli.gst.uqam.ca> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Of course, the term "identification" has other meanings. As when the police is trying to identify the victim of a murder. An identification may require an identity document.=20 A hacker may prefer to stay anonymous. The term "iso" could be better. Let f:a=3Db be an iso between the elements a and b of a type A. Let f:A=3DB be an isomorphism between the types A and B. The univalence principle state that every isomorphism is an iso. A ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Joyal, Andr=E9 [joyal...@uqam.ca] Sent: Monday, May 04, 2020 12:16 PM To: Michael Shulman; Stefan Monnier Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com Subject: RE: [HoTT] "Identifications" ? Dear all, I am tempted to add my grain of salt to this discussion. I like the word "identification". But what about "iso" ? It means "equal". As in "iso-morphism", "iso-tope", etc. https://wordinfo.info/unit/2795/page:9 Best, Andr=E9 ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Michael Shulman [shu...@sandiego.edu] Sent: Monday, May 04, 2020 11:59 AM To: Stefan Monnier Cc: Thorsten Altenkirch; homotopyt...@googlegroups.com Subject: Re: [HoTT] "Identifications" ? 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. On Mon, May 4, 2020 at 7:48 AM Stefan Monnier wro= te: > > > 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. > > 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 e= mail to HomotopyT...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQx_2TinRHBrmOAZFnmFp8VVQ-yMcPvtKFtX-d9wGsD%2B2Q%40= mail.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 e= mail to HomotopyT...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F3F0F%40Pli.gst.uqam.= ca.