From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:aca:c3cd:: with SMTP id t196mr9228382oif.58.1588603714966; Mon, 04 May 2020 07:48:34 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6e97:: with SMTP id a23ls2659112otr.2.gmail; Mon, 04 May 2020 07:48:33 -0700 (PDT) X-Received: by 2002:a9d:1441:: with SMTP id h59mr14732619oth.192.1588603713283; Mon, 04 May 2020 07:48:33 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1588603713; cv=none; d=google.com; s=arc-20160816; b=kqFG6Z+AZnjgpkPeFu6YlBkIhaffgxBrkUVY+TqKI7GR0VqPkMYRnVLYVoSA2ZMAhk aL31gXCOiN6sJwCH9zbCggbEgmd1XHZDgo9W0eCB5C2YHMUBUkOYzpXpLgOON4EC1du+ r0mXaGxh72C6VjCrSloUBaJiC2a/OkdHbJ24beki6LriPavLiEWfhixm6/ByqAKc++UW mH8KGKRXbMK/XS40/i5JV/SfZYKQxfjWs5EtpPR9d+2GmgmL06dnTKlTWX5B8juKOTnu VBQqfTiC0UVAgYHKDDESi/MXwyO2VLPQQ34ZoYPGVK8s3HnVhsd/83mFKSyN2ge9q7jm 6T/Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:user-agent:in-reply-to:date:references:message-id :subject:cc:to:from:dkim-signature; bh=Pkj0wH33QAXMb9kc5DKUYintJxOi8wT7eH1hResLGLI=; b=EXwenI7PVWgnTkhxGE6JbOTYJrAQC9Cv0yuAyH4ZYRyWLpO/vU6RTFyrKNFgJKwYgm VNEHUiezWFyH7/7r6gFPa6lhq0/uc7olXETjztIRDUAJ5eo9EK22x22glJt1nttDvMd3 e//uFV8YbhEvIBXCPPDRVNmgGpVFyZvAsLcBERXONMpHXmXv2v6e79qjcYOTom8vmgpG UNufEO521fKzm7jsVAEpJSlmxi+hQkZNDti8DxGQ65FuqFH8MMLHJGkCDsPGWfOsFv5K 6XoGfO1Htry7vrzXNVKbDD/g9kzVeuHW9waGvpC6ETyfnG9f1vbSOXOmdc2otZV2n6Et 6qdw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@iro.umontreal.ca header.s=mail header.b="FpnGy/YT"; spf=pass (google.com: domain of mon...@iro.umontreal.ca designates 132.204.25.50 as permitted sender) smtp.mailfrom=mon...@iro.umontreal.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=iro.umontreal.ca Return-Path: Received: from mailscanner.iro.umontreal.ca (mailscanner.iro.umontreal.ca. [132.204.25.50]) by gmr-mx.google.com with ESMTPS id h17si57552otk.1.2020.05.04.07.48.32 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 04 May 2020 07:48:32 -0700 (PDT) Received-SPF: pass (google.com: domain of mon...@iro.umontreal.ca designates 132.204.25.50 as permitted sender) client-ip=132.204.25.50; Authentication-Results: gmr-mx.google.com; dkim=pass head...@iro.umontreal.ca header.s=mail header.b="FpnGy/YT"; spf=pass (google.com: domain of mon...@iro.umontreal.ca designates 132.204.25.50 as permitted sender) smtp.mailfrom=mon...@iro.umontreal.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=iro.umontreal.ca Received: from pmg3.iro.umontreal.ca (localhost [127.0.0.1]) by pmg3.iro.umontreal.ca (Proxmox) with ESMTP id D10834508DD; Mon, 4 May 2020 10:48:31 -0400 (EDT) Received: from mail01.iro.umontreal.ca (unknown [172.31.2.1]) by pmg3.iro.umontreal.ca (Proxmox) with ESMTP id C34704508DB; Mon, 4 May 2020 10:48:29 -0400 (EDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=iro.umontreal.ca; s=mail; t=1588603709; bh=XcuzysDlf4gjqDO6DvovffPkICnQiSACh/JzMT/ObhU=; h=From:To:Cc:Subject:References:Date:In-Reply-To:From; b=FpnGy/YTfn2oe0z9H5/40bdEPSpgUy1BHRm4BYyYbi3Z9ApU1juuUjMXkcXxUoWQT CTBLny9MUTC5FhGUnNarV6BCBiSaJ3z7Drb4X7Mzz97LcjErLZxq1N49XKHoycqbFL rThl5aH3ly529lSGvTecRoRT9tsnDAKoS+TjzeAvUxGSBoeKisqqUKqiIw62q744uS EdLnYHasQaztAlGaBVHAO8SqHjugXo58RsTVru0x9njPPxRZju1Vnh0o00KY9+Y3h9 Td/ExDholvKawlIs2IYrgRNsr+9E29t0EihMNagh3Y0k7PfkpCFfAHjBWowbR/Aqq/ o1zDckhRzHLRw== Received: from alfajor (unknown [216.154.3.202]) by mail01.iro.umontreal.ca (Postfix) with ESMTPSA id 37B88120235; Mon, 4 May 2020 10:48:29 -0400 (EDT) From: Stefan Monnier To: Michael Shulman Cc: Thorsten Altenkirch , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] "Identifications" ? Message-ID: References: Date: Mon, 04 May 2020 10:48:28 -0400 In-Reply-To: (Michael Shulman's message of "Mon, 4 May 2020 06:16:57 -0700") User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain X-SPAM-INFO: Spam detection results: 0 ALL_TRUSTED -1 Passed through trusted hosts only via SMTP AWL -0.067 Adjusted score from AWL reputation of From: address BAYES_00 -1.9 Bayes spam probability is 0 to 1% DKIM_SIGNED 0.1 Message has a DKIM or DK signature, not necessarily valid DKIM_VALID -0.1 Message has at least one valid DKIM or DK signature DKIM_VALID_AU -0.1 Message has a valid DKIM or DK signature from author's domain X-SPAM-LEVEL: > 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"