From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x840.google.com (mail-qt1-x840.google.com [IPv6:2607:f8b0:4864:20::840]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 99889226 for ; Tue, 12 Feb 2019 17:54:25 +0000 (UTC) Received: by mail-qt1-x840.google.com with SMTP id m37sf3492786qte.10 for ; Tue, 12 Feb 2019 09:54:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549994064; cv=pass; d=google.com; s=arc-20160816; b=DxMBb3qcFEwGoYSY8B7Wpb1jBEQAzak9Mg//gQDQpSSu3o/+WEJNPiRcQ3CUdrSHcD iHY1Xbfrkuo0WmAc7U7zVY4rhj9nger/5KqhWz4cgFDwcgmKuScsEOEBTmjfZsamJ2TS dynOQUn+AoXyUAn2q4MSaWwRY3r0+66t029ODn/0hd3Qi9X2j8xXNEGBLGktmGjixOyN SjGyXm1FkScvO7lk6/81V1ymECcbH9eZBLog/OBPHiZRsMQ3+ytqf1g2kGLKkuxOasNQ hiHankZUvj7IZIQIRxl9v1+kwTdPTkNBSST0p/lg+y5iR3170S9o1HpjkyewzGfsy6c3 gTew== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=MU7hU9rIiHc+a69SoydAXsjya0sVRDc+Qz7SqCMfkDo=; b=YSJq+EUFyAZtiVgoJnuTtT437+lW5Pkl8Zd3qCTcVgcbT8ChcllJrMWs3CoA8kCh++ YC3ncmirVEva2NQMZEAEEr6ANbG32I9wNfo37Q+/MtGM2uZCCSxBN0R4Q+Q4fdXq6g1e Z5HwXppym/oMCEf7Pua4VbXiQ+kR3wncskH4nefnlF0JsBUve8uLd+NHIC9ZmRKMQOl7 JdTMQuQG1SKHNqlze0QAXWeJVTWQkVj6JmIZESmrL9b6m33Vmo2GEctZBivTlFGNGuUy AXzXzw2BW5rffC7y855Vxo71h0YssgTqfbaZE4fUioQdOTtBfas7EZyC83UhW29vasO7 IEPA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=cV6DwAVA; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=MU7hU9rIiHc+a69SoydAXsjya0sVRDc+Qz7SqCMfkDo=; b=HwmQSLMxNYkNLkhTyOf2XjErEPJJQepOW+SZnuiXxZytiFSB/650HdNCC3pFBUSEpp aaJR0XQkNWA2c0ie6OXXTtnnPFkHWCTbv8TI6hqNroqcvRhJwJf/mD0E86J0X5x7VbHM RJWuWp3jfVxUJuyDVtBM2dMX/Ba6HvtLARNi3zB59nYZDcN97WD8OwgxQxT64GEHKbde GAStXNXwdGu87//wFgMUlCPZbpI3xWxSLEbh0RkVC0m6FV0w8JyOpauqMExABpdpDPKD 74g+ESOMnVgkU5dY2mF8iocD52wldrpefJlEeR69gqhl0sDHee7Rki36mKw9EJ996kCs h/Kw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=MU7hU9rIiHc+a69SoydAXsjya0sVRDc+Qz7SqCMfkDo=; b=VmsyZenzknHPMAc+izTzoZH0Hge4q/Ull3BIqua0uBhQR1dU1+LhrSaqJTNvBMWhqp Mv5Gw0jDAHrYCBd1eMRA2tOBf9D/2zZjXZChRuiNPlw1HQzDTfZz/MJyIaZhYedtw2H+ w98XwO/lkT7MSjfsygb2qBjhAnWVUab8nxPZJ8v9xOkj310hw5r/m7tkFogRAbMn7Njw xoCQzet42kFElsSaWxZGrelJhucqOCVKj88J9Vg3iDQB8cfKXLIjY86JDAoRFpY+kUnm 461eVRolKxwj8FqaLq4eegshmQNp/wvCcw2p6iinp4SIHVmvjGZ+cwttuVt9QXdGTP+c IDOA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZXDsiPb0xYMRtGY2EWHzBiviSEsUq2vKE3cWdQ2jMTbFZ63bsy ziQq0y43+KLNALQtCNLyTCo= X-Google-Smtp-Source: AHgI3IYAPRtBcJMcWENhcVJWZURnmxJiddRssUSu8EZteJuqBUxZSiCjMLcKwCjDDG2XVfhWqintVw== X-Received: by 2002:a37:77c5:: with SMTP id s188mr58797qkc.0.1549994064614; Tue, 12 Feb 2019 09:54:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:4dc1:: with SMTP id a184ls8149279qkb.4.gmail; Tue, 12 Feb 2019 09:54:24 -0800 (PST) X-Received: by 2002:a37:c094:: with SMTP id v20mr2638275qkv.23.1549994064292; Tue, 12 Feb 2019 09:54:24 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549994064; cv=none; d=google.com; s=arc-20160816; b=ka0KZeegeG6h6xduuByT72yocc/ZemBIyyds5yE5meeKXeKXkAAd4acQHJ9dTZsjAU lrSdhnvn6KZNVQKMrd+Qv1iRBXLZBGpnDop0z9uiSw0lGN94mO8Zsbsm7wepVTv+izEt cYuiDEuIZUTB/jWRqPvgm0GlK6d9QkDbbPcenrxM7PVPTXsbhiXFLKCWQ23IDL0QEfnW fmeSRRC/+jRH2zojj/YBrxtu94oqtc3WN//xDPudixIrJv1gvdg75S1MWCJdtIZJ/jCr rwXv7v7a1q8y6BpD0DTeSOWvHQN00V1Dwo+1tMCBy0MBMQhS6XQDoDOztBnsgnM176Hd +NxQ== 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=1f8S0dCRCNKyHpJgy3vfv28PiWwaOkChFEVhuTWJs9E=; b=Pwsk7Rz1ZMRL6Tmouj3y0H27vEBU/tfFVFy4p7uiAZD2c0+mqIEN5RPFvwdxgm3Md7 +6r+gdBiypTu6coxWeh+zNcJvGb8VdUen9emSU0xKJ9uzPNrnh7DLePyxIirlAsbhCH+ ZzgIheZnEX7P2F8GcbBUTfOf1GeCYA45qsNqAOc3yfll74A4J0opAXppU+/VP7Chu6sy 5cJTUCmXcu7UrYlM64g5x0lmIfSyK+9GgD4TpOiT/A0lkaQAt2na1LuMc2OTA+62gtRQ s2cOizEpscfx5DyoehOSEYxvJIOegm4GlnU0B9pZCVeUBaK3gkRJy44F4Uc0n0wiuSiE nXgA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=cV6DwAVA; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2f.google.com (mail-yb1-xb2f.google.com. [2607:f8b0:4864:20::b2f]) by gmr-mx.google.com with ESMTPS id u124si760615qka.4.2019.02.12.09.54.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Feb 2019 09:54:24 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) client-ip=2607:f8b0:4864:20::b2f; Received: by mail-yb1-xb2f.google.com with SMTP id x13so1376771ybm.7 for ; Tue, 12 Feb 2019 09:54:24 -0800 (PST) X-Received: by 2002:a25:7284:: with SMTP id n126mr4147012ybc.504.1549994063806; Tue, 12 Feb 2019 09:54:23 -0800 (PST) Received: from mail-yb1-f177.google.com (mail-yb1-f177.google.com. [209.85.219.177]) by smtp.gmail.com with ESMTPSA id o4sm2543678ywe.102.2019.02.12.09.54.22 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 12 Feb 2019 09:54:22 -0800 (PST) Received: by mail-yb1-f177.google.com with SMTP id s5so1379548ybp.6 for ; Tue, 12 Feb 2019 09:54:22 -0800 (PST) X-Received: by 2002:a25:d4d:: with SMTP id 74mr3989912ybn.357.1549994062236; Tue, 12 Feb 2019 09:54:22 -0800 (PST) MIME-Version: 1.0 References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> <58de3e94-fee9-405c-ab18-5a35cb90eb68@googlegroups.com> In-Reply-To: <58de3e94-fee9-405c-ab18-5a35cb90eb68@googlegroups.com> From: Michael Shulman Date: Tue, 12 Feb 2019 09:54:10 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Matt Oliveri Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=cV6DwAVA; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , For sure definitional equality doesn't have to do with models. Like all the kinds of equality we are discussing, it is a syntactic notion. Actually I would say it is a *philosophical* notion, and as such is imprecisely specified; syntactic notions like judgmental equality can do a better or worse job of capturing it in different theories (and in some cases may not even be intended to capture it at all). > what's the difference between "denoting by definition" and regular denoting? x+(y+z) and (x+y)+z denote the same natural number for any natural numbers x,y,z, because we can prove that they are equal. But they don't denote the same natural number *by definition*, because this proof is not just unfolding the meanings of definitions; it involves at least a little thought and a pair of inductions. For a more radical example, "1+1=2" and "there do not exist positive integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same proposition, namely "true". But that's certainly not the case by definition! Same reference; different senses. -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.