From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6402:17c4:: with SMTP id s4mr15646383edy.348.1588607206126; Mon, 04 May 2020 08:46:46 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:db4a:: with SMTP id n10ls3230198edt.4.gmail; Mon, 04 May 2020 08:46:44 -0700 (PDT) X-Received: by 2002:a05:6402:17ef:: with SMTP id t15mr15105619edy.10.1588607204728; Mon, 04 May 2020 08:46:44 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588607204; cv=none; d=google.com; s=arc-20160816; b=ojPPVrAuKbc5I/em34TQBm9B/LMp/XJpXeJxcfAG9hKKTtfRsZ4/RWXKRXz3PU0xDs 50yb7hZ6pWHwMQF9g6EFhgVC2VOn1b2MpgBSwM/hWGAHawTboQBLFlUUio16i8w0npUv 3RBby8rjyWVppYA/E6P5L7sy/OuJOWBjZarFivLO3HYcAf/Fcd+iRjU4csrsROT29cES n/RJCaVDPVajAWOK1mEtKwdO3mzHcFjN/RJKjm9j1N0toZwR5zidW4buyPuq2KU8U4vC N8LPtVsW9ueoLCSzRZcrRnJqmwFenAXE5y3NJLkgtVbaOte/GFfrVUeGswJE0dd+vjRb nyLw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=WBWDGWFqTMQ9i4MjDyyyqaUse61gJ5j4eRgEJprF9Nc=; b=bcb+opS/x/Qr8cf/7O62Ayb20W3fjxayb7FtszF1fQUwK6xSNpcFW6y3k7LyUI7yA2 orSRRb/hh4GQr4YpC7Mjg3rxPlzttR0xu3Ar0EuuK9xXay4r7vNj/BSwUbsmns0AQgnw CcdnsTOvv4ONZJO3K7ElZphLksKuUcesKtZy1dUYjO92Ds6MWUxxi6SmxHXOa0JP0bDw zRLnPYoK5P9O1QIt/QW4qEjxKjr64mKwKDTu2vFs0DmYHE1NaVYAZco262Nl+E8cla5A CyljcVwXr4sr8EcOddsRWHGyfMQNyUbApxfvxi6GSlUl5zPOCCWpQf//6Qd2KIRCSTxd Dq+A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b="pfYqhT/w"; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-wm1-x335.google.com (mail-wm1-x335.google.com. [2a00:1450:4864:20::335]) by gmr-mx.google.com with ESMTPS id v18si456685eju.1.2020.05.04.08.46.44 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 08:46:44 -0700 (PDT) Received-SPF: pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) client-ip=2a00:1450:4864:20::335; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b="pfYqhT/w"; spf=pass (google.com: domain of nicola...@gmail.com designates 2a00:1450:4864:20::335 as permitted sender) smtp.mailfrom=nicola...@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: by mail-wm1-x335.google.com with SMTP id k12so9002543wmj.3 for ; Mon, 04 May 2020 08:46:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language; bh=WBWDGWFqTMQ9i4MjDyyyqaUse61gJ5j4eRgEJprF9Nc=; b=pfYqhT/wFUEbS/zKQtFxZ0BFw6YYKp4KipbKlSW0o7ixLBonaFwLByF+FVcE0pp3HA LsHsLnW5KIB5gcwlYZKRSdU3BfUHyY7Y+QCqHiIroE4cHK3oKmw42XTXMokwybsDaUf4 bAZ4Uz2N1dBmKOfpICh0TqJX1dZZoY9lbVB2vprxShEUCuMSXSIJx5vzgFlza1of4pER MYjMfqLL8mpv1+txYQ/G8zzdT5POyQa0/hzLFIumarmGD7X+cCfa9g4a5321zZ2nvoNm fHa0XEze/HDi6FcahhFL9A2D5irvfD8SB7A+DPXlsIdrh8gtFsrMHUgs+Bk8vAS/iBLV 5WpA== X-Gm-Message-State: AGi0PuZnD0oyE038QUCM7tzksd47DpO2vEqcMiTMjoASmshJa2DI1n4T l4/HoQR95TNwciGN8TBAUVpgZXYOY3c= X-Received: by 2002:a05:600c:da:: with SMTP id u26mr15645436wmm.48.1588607204141; Mon, 04 May 2020 08:46:44 -0700 (PDT) Return-Path: Received: from [192.168.1.67] (37.67.90.146.dyn.plus.net. [146.90.67.37]) by smtp.gmail.com with ESMTPSA id o3sm19324355wru.68.2020.05.04.08.46.43 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 04 May 2020 08:46:43 -0700 (PDT) Subject: Re: [HoTT] "Identifications" ? To: HomotopyTypeTheory@googlegroups.com References: From: Nicolai Kraus Message-ID: Date: Mon, 4 May 2020 16:46:40 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US For what it's worth, "identification" is much closer to Per Martin-Löf's original terminology ("identity type") than "equality" or "path" are. Nicolai On 04/05/2020 15:48, 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" >