From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aa7:990f:: with SMTP id z15mr19167677pff.132.1588608006283; Mon, 04 May 2020 09:00:06 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:ff0f:: with SMTP id k15ls15207800pgi.3.gmail; Mon, 04 May 2020 09:00:04 -0700 (PDT) X-Received: by 2002:aa7:9689:: with SMTP id f9mr16970044pfk.24.1588608004499; Mon, 04 May 2020 09:00:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588608004; cv=none; d=google.com; s=arc-20160816; b=SPvJw4IXXePyqWVSq+EpH3XhKY0XUyHPQ4zqvVDyUKA0jfFwnjB0GmaCk0X8drncHI Pf5S1LzNCCPiUzrf4XrZj+eNrbwIKV6/9/4Wq2hCKMt//rpAdpH9U0XkDqQICi/YWMVh M8YDddV3NvYqPp8RyhtwNDRXJdH9AkAs7Tx7YJus+NXG7wDw35aKnxj4+rY0ESLmWpF7 LSOEm82NnbF6gRd+XWVXu18HbZpoHiSWr7UlfNhBhRlFZHjaNkNQ/9vWL59PK4hNLRXU QI8LyJvVSWWRgi9ygTbc5yeT5Wa5QeS17uj5Mx3ZW3jFZFhkHSBOMTYbs45PMxffDjkg Ms+A== 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=TH2Z5a/+TOiNJbjONzEhJmHsqqYqwMso8YtgbcKTjGg=; b=AcleXHuE7vnkPurPHK3Ad3tyIWhpGVdF7BDqzZ3qc3S+0NDNEDd06sYup01IPK2UHj 3utI3WTLyuYrP9Kdpw7iQPMJKnNNUUdDnsrrK5Yewun1K8FzGprISEQHN8InZlpzWvxg 7/3mIat6ZZWQ6iqGFAwOdMK56Ix4MLANuKmdZV1a1XCEJnfQwynJpYXIHU4NV+b7w2d3 U/1PBsSFLCMFmWQW4tmjdECsZfKa+792+WU8s1bWqGRB6QUBrIgpBotQ9vzb9nnKDIkl jCCU6DSo76MDgH8RkGqvql/LKN5E05GmkTmoB5c/DdUxBsTREjs5+LBBTBzWmNxH1iK9 uF0A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Vgz8BjCN; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32a 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-x32a.google.com (mail-ot1-x32a.google.com. [2607:f8b0:4864:20::32a]) by gmr-mx.google.com with ESMTPS id gn24si40794pjb.2.2020.05.04.09.00.04 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:00:04 -0700 (PDT) Received-SPF: pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32a as permitted sender) client-ip=2607:f8b0:4864:20::32a; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Vgz8BjCN; spf=pass (google.com: domain of shu...@sandiego.edu designates 2607:f8b0:4864:20::32a as permitted sender) smtp.mailfrom=shu...@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: by mail-ot1-x32a.google.com with SMTP id 72so9363878otu.1 for ; Mon, 04 May 2020 09:00:04 -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; bh=TH2Z5a/+TOiNJbjONzEhJmHsqqYqwMso8YtgbcKTjGg=; b=Vgz8BjCN++/zC9f8IbpbPCvEoiowsvMVurWJpyCTXdlHXx360GpES21saxD1Wb9tJX SAnbwO8fHI6CmIdRRXaP4T+nGrhnPvIgsbROSxmZrGn30sUUzQV8IsiDixQY1+cE2/88 VxH/vbYsasNe1mcdGxOhtJg4BT4Cq/1d6cfaUqKh7c2uMv2ysrqfSZhLj895iRxFsZ5E rzFsJgrm+TiApiyic56j9RmBHKNYLeIVuhShUYOzIDM6orK0z+9KGJ2hm+SnWYE/VPf9 ExXkBd3DWHoATXlxvH9n4y7YJtWhEgOamMXdqabzjetI4RmVRxBuh9HUMaLljH6k+Idu zR9Q== X-Gm-Message-State: AGi0PuZF0A/F8SvA74kSGpn7Eo+iJyF1RpSgbQvxeCULt6ZIo8r56Gcy EhTELc/Ok7mrjBd9PJN3XRQkOHUYxFGSVJ+4aA//YQHDimGz9cw+MLwymwIZi+VKZfzB4LYobUF zSMx4IiQJgeJwGwat8YAFZNc0aJfRLNdjal/38F2L38Fgyj7qtKkvjCsOcmK3PqirDqqh6lUU3I sfYl/CWI4/ X-Received: by 2002:a9d:810:: with SMTP id 16mr14398901oty.56.1588608003275; Mon, 04 May 2020 09:00:03 -0700 (PDT) Return-Path: Received: from mail-ot1-f49.google.com (mail-ot1-f49.google.com. [209.85.210.49]) by smtp.gmail.com with ESMTPSA id y22sm2471816oih.57.2020.05.04.09.00.01 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 09:00:01 -0700 (PDT) Received: by mail-ot1-f49.google.com with SMTP id j4so9300171otr.11 for ; Mon, 04 May 2020 09:00:01 -0700 (PDT) X-Received: by 2002:a05:6830:1e96:: with SMTP id n22mr11214332otr.96.1588608001202; Mon, 04 May 2020 09:00:01 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Mon, 4 May 2020 08:59:47 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] "Identifications" ? To: Stefan Monnier Cc: Thorsten Altenkirch , "homotopyt...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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 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 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" >