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-vk1-xa3f.google.com (mail-vk1-xa3f.google.com [IPv6:2607:f8b0:4864:20::a3f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id def1f597 for ; Mon, 11 Feb 2019 13:04:36 +0000 (UTC) Received: by mail-vk1-xa3f.google.com with SMTP id t192sf5260717vkt.9 for ; Mon, 11 Feb 2019 05:04:35 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549890275; cv=pass; d=google.com; s=arc-20160816; b=exuPwK5RHZn4op6wewJ7u8/+/npZxUu/bw0RkSJt0cthkpoAGeAu5kRUxGeQULYIL+ OqMGylW/5I8RdOcEporaRL1TJHbS/P5rF4W+87DptSMEAJuPj+zIwQ7AbQvOh88Y+CQ8 fD1RnnX0nUqfw40MmrMQZorWGqY5KUU2XQbg1WBkllbmDqbRZjN4A2gsDgDGEA6At624 6M0B6b9+fCHHdbwBgjuqGNDdcILEShcFf4Hsm8isaJ805STS3BzoSuhVD5roDsGdPzG9 YY5sRwniaLg9L5MNDshTuowS6xi4GjQEGFBVoPL4QWEaqGYkUDzgiBTBM215jWk57URd qAAw== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=yh3rykhET39OYCTg2CSZcDZi7pgyYblxmB9FHu5ANM0=; b=kUKWb+QnVkQ5ydnmIa5V45K8flg0JylUcSVn0mDDnvcuRPe7ShbqSDQBZyTrTTqxI5 fOVyaIo3088ZWezmSfCNdh2lh4vFuhk1wdncdjgRzv9YHedbPREauA2h8IroQWp3qGV3 cm/DRwHInHkXUONvR9Pr+a4ccPAy7NOR0jdv5P45bYpQ6Eo4whznxWyd36OosUX+gZBG 8EFTV+ydQ6qiqH8ylfBnfw6rozvSz9WQbPlEEqJ4o/DBlBGkchjyAlEJpJ5ErZ9UlzO7 3X5H0KSHJrdza3oH2brMTXHlO23z2oIFY4fnpjnNRVY2h69D1Fi4zABEFSVEsN4VOQ0g /CIA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1ZHA7aXC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b41 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=yh3rykhET39OYCTg2CSZcDZi7pgyYblxmB9FHu5ANM0=; b=ZHM5h6Q0OXScFxgiXLUHvBRmggrckAzgjWI/I0UUQ067ACzRpuyfyJCrtD7f/2Cr4N nGxvorL10r2Lm+rxUyC60GB/+IfnDOa+fFIbM2QP/2R/0G7iWKRxtcg4Onhee3AkdxAt +AHstVlPClAWCf+i8JfnAMHG7y0X2DncggQ+49tcLLypW4uj/0MzsAWiGCKndFby4BaB 64v+GaRpHeiL8nYfGkrOIKoWokA2AmjB640Pvk6knZ8ICKOwUuBUHKeu5MtbhYpbdSBo +BSa4hfWkqBU1u9f1jYF3Pm4ABfROIH6ZojjPUaYvJKvB66mncISI4qwzWkniOq1dX22 HWHg== 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:content-transfer-encoding :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=yh3rykhET39OYCTg2CSZcDZi7pgyYblxmB9FHu5ANM0=; b=EK0IvQ4anruNXf1mttk/YT1++io292gtlg3B7R1M42J9pDf2pzU5ErArPpGcL3/3Tc Le/04JbcXrb9rHeRLICN10NhU2eSStX77BHWLQS5V7yDsruJCAJeX8NGSSwsOn2vN3gg T4jkE8XrEiFoIjvf+3hLiRQVccfek3T230HODf0p5fcmjeyciodUnVEaRYApsr21QJ8N CbFC8kGFH4arsFxZLWuOeDeCro2/kGpnc9qmDfB+2Js8pTbaF5oVkknaT2WLvrCTH4CB QuSyKOhhXJRD2BDdJ2x5l431ku8p5OJBLLf5BjWrctOYVZu6HJCteKJ9yu8Urd6jXhUf lSeQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubmnNisqpahFL3BF6MY7Jog6S1PZFjp9fWbX3J64woDN7yV66nM yv4LQbR/9kjk7buiJd42G6U= X-Google-Smtp-Source: AHgI3IaFlhPQ5Phk3iy0Hk2Y3UfMmC9DgpHk4ZTZymFirukPeW/Q4IMbjts6tXHgoiz2br2JuhjKGA== X-Received: by 2002:a1f:9d46:: with SMTP id g67mr98650vke.6.1549890274954; Mon, 11 Feb 2019 05:04:34 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:8442:: with SMTP id g63ls2725499vsd.5.gmail; Mon, 11 Feb 2019 05:04:34 -0800 (PST) X-Received: by 2002:a67:8707:: with SMTP id j7mr24464938vsd.30.1549890274614; Mon, 11 Feb 2019 05:04:34 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549890274; cv=none; d=google.com; s=arc-20160816; b=AbvW3CJg9XaA1kzJATUQha2YQn5mF1oN0yvwvQqm8MpidrhRxRyRp8qXSW+7lCSVbY UQ+okYfavEQcHvC2x0aXiX8fe1uT7/kWTg+NSfMYRpuriRqmgvQIVRESNZTIfKMGArdQ OIi2IaZwkyJm1Mmd14q7dTkgo1hY9JfsueRhpc9vUeJOo6xOemMUO93UN/K24OJBYbrV O7L4L1FSfLXEdQ9jRzcfaysFTW6HQhb0WYj/WSg4s/uAn24m2DxG8srB9t/5vnBF//nT lroodtJbVMnKcfY8QDI+s3e+zOzCYV84riq+dck/dYO+JfAmeBX8U1CvWSjapf71/V3y D/2A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=d3IwsWa3hlgVTCbF70sk+vIdQI6JNlX6xtO5p5iyCPk=; b=jndmsIzUXx4viQ/QuBJr2jPOBvZzduWBfQF8za4FFXfEt41ZHGtAhjl6HBXiUio0c+ alWYtnXYNptD+v6Bbi0N9n0o6fY+BlSxRhFH2fz/twxtCZPlEMU4UWsmppSlTWHaqAaE PV8AMS46/xhGzsDm+LxqLAhisyWtxaMWQw9z+wCGmGvFSnFP5CQNt9FYFjdy/RfgOW9t eWiRZgE9F6RJ9wewUjGzStPOnqevKsXHy9zF7LQHh24eMIaILDidxmBnQ+fW6tTTdBf5 x80pNjPpfkn0E76fphWUd2L8Xvk0tH1WyxfeVfYD1wqTRSF5xupNgXMt4U2Yhb07qSF+ gKFA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=1ZHA7aXC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b41 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb41.google.com (mail-yb1-xb41.google.com. [2607:f8b0:4864:20::b41]) by gmr-mx.google.com with ESMTPS id 191si649360vkj.4.2019.02.11.05.04.34 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 05:04:34 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b41 as permitted sender) client-ip=2607:f8b0:4864:20::b41; Received: by mail-yb1-xb41.google.com with SMTP id j189so4113960ybj.9 for ; Mon, 11 Feb 2019 05:04:34 -0800 (PST) X-Received: by 2002:a25:4d2:: with SMTP id 201mr9968841ybe.196.1549890273824; Mon, 11 Feb 2019 05:04:33 -0800 (PST) Received: from mail-yw1-f44.google.com (mail-yw1-f44.google.com. [209.85.161.44]) by smtp.gmail.com with ESMTPSA id 139sm4036895ywt.78.2019.02.11.05.04.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 11 Feb 2019 05:04:32 -0800 (PST) Received: by mail-yw1-f44.google.com with SMTP id x21so4121902ywx.11 for ; Mon, 11 Feb 2019 05:04:32 -0800 (PST) X-Received: by 2002:a81:31c1:: with SMTP id x184mr28428685ywx.496.1549890272232; Mon, 11 Feb 2019 05:04:32 -0800 (PST) MIME-Version: 1.0 References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> In-Reply-To: <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> From: Michael Shulman Date: Mon, 11 Feb 2019 05:04:19 -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" Content-Transfer-Encoding: quoted-printable 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=1ZHA7aXC; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b41 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: , On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri wrote: > As a form of extensional type theory without any "built-in" implementatio= n proposal, it seems like HTS has no notion of "proof object" in Jon's sens= e, which seems to be formal, checkable proofs. It's not that you couldn't c= ome up with one, it just isn't specified. So I don't think HTS has any "def= initional equality", in Jon's sense. But it seems like HTS' exact equality = was considered substitutive nonetheless. In fact, it seems to me like what = Vladimir meant by "substitutional" was that it doesn't cause coercions. Eit= her because it's definitional, or because it's subsumptive (my term, from a= nother message in this thread). > > So I think you're misusing those terms. Well, after many years I still have not managed to figure out how NuPRLites use words, so it's possible that I misinterpreted what Jon meant by "proof object". But if you interpret what I meant in ITT, where I know what I am talking about, then it makes sense. In ITT the relevant sort of "witness of a proof" is just a term, so "not perturbing the proof object" means the same thing as "not causing coercions". > You seem to be downplaying the differences between these notions. Why? Maybe things are different in computer science, but in mathematics it often happens that there are things called "ideas" that are, in fact, vaguer than anything that can be written down precisely, and can be realized precisely by a variety of different formal definitions with different formal properties. The differences -- even conceptual differences -- between these definitions are not unimportant or ignorable, but do not detract from the importance of the idea or our ability to think about it. Indeed, the presence of multiple formal approaches to the idea with different connections to different subjects make it *more* important and provide us *more* options to work with it formally. I am thinking of for instance all the different constructions of a highly structured category of spectra, or all the different definitions of (oo,1)-category. --=20 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.