From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:ac5:c810:: with SMTP id y16mr37506vkl.49.1588608990565; Mon, 04 May 2020 09:16:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:6081:: with SMTP id u123ls1100341vkb.7.gmail; Mon, 04 May 2020 09:16:29 -0700 (PDT) X-Received: by 2002:a1f:1ed1:: with SMTP id e200mr71054vke.96.1588608989288; Mon, 04 May 2020 09:16:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588608989; cv=none; d=google.com; s=arc-20160816; b=r14TiN3BPDOYr0oATOdCuaNXeojwZZHimwxNO9a+cSLRmcGErHHeYFoCu/6TBvETn8 d5Ud3+3pIsQfIgSMmoXnloF1h1P5g7FbA4jMeCfZ6KfHQcaHATmgfNpaGO8pS4LPzHzQ DiErAVLK8v01d3KAL+LxpUM8RsLZElxflXIYMiPQW8Vvd+/aoTGs2PCTC6Dc/3VrovE4 3E/PrtSAcwDzliIfciny9Ww1szIYLWEC+IC4vB6KNDK4xWmxRI6cRY0Zr8zwpVItJMxW oaip0q1hwC6Nu0g/vv8XDrV9njFakhtK+NQzABH4r6rlMSa1gZ6PY+67mUxK+bbQrfDq v6dQ== 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=9V0ns6kQek9bEszeuwrBo7dbvXGm4qDRMhmfQ+gvZ4M=; b=iYSPcHr+U7x8LR4+EHC2FgWKJzicOffleHAZDD1D4eWwk+wUT57IuMXIkyJ1jrAesM X6sU5Pcl/o6oC7aWRe963/al54E0NzCoBMHD3wt0J/Pz4TrZmFbXDPUcSaoNTyCMBqus IFRKQUqokyDDDwTHmmyRAYQ7VfCw05bhyn4ZPY6kd0e0LIF4J7gpAAXKIj49LJrm+r5X +iXnKKf/LJrdEOGRKiTk8gTVXH8mPp0Wb5SupqyJVeHgOx4qD1aD5wkeG7pSaoYeUYjn U+Yg9OEcTrPmf0W9DvE/qNI/9H+H0ue8BsDa4h0aek/fD4FQYSEell7eZS/3WypWyOgU UIoQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail5.uqam.ca (mail5.uqam.ca. [132.208.246.108]) by gmr-mx.google.com with ESMTP id a205si868033vsd.2.2020.05.04.09.16.29 for ; Mon, 04 May 2020 09:16:29 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) client-ip=132.208.246.108; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.108 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: WrhZFsZDOi6Qlo38FIAo44Iz4GJJ5TzB04wOu322Eb/7NirRllTeEJjQYfkzibUYASRPa5FEdN VwfxzVSBL/frMgg39rRLvit65OzkbwBDmn8zTE7eo7mB1dYXdF2KngDKcBjxKySv00LKevlcmo +6IVjEGuAjleHahkYjCTAa7W653AjAtcCM6yIRfcADG6gPOvAowJjYnvtwlRgmdg0svBNA9azI PfGs6ai19AOMaKOi2gGkYE444515Q56omdlFtdj5NTPXuqJz1H4ptg+ZdkZmMh0o/WkrndbQuz aEQ= X-IronPort-AV: E=Sophos;i="5.73,352,1583211600"; d="scan'208";a="11340061" Received: from unknown (HELO Avis.gst.uqam.ca) ([132.208.216.75]) by mail7.uqam.ca with ESMTP; 04 May 2020 12:16:29 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Avis.gst.uqam.ca ([169.254.2.247]) with mapi id 14.03.0439.000; Mon, 4 May 2020 12:16:28 -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//+9Qrk= Date: Mon, 4 May 2020 16:16:27 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F3F0F@Pli.gst.uqam.ca> References: , In-Reply-To: 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 Dear all, I am tempted to add my grain of salt to this discussion. I like the word "identification".=20 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.