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-ot1-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 9a2e288d for ; Sat, 9 Feb 2019 20:34:23 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id n22sf6520494otq.8 for ; Sat, 09 Feb 2019 12:34:23 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549744462; cv=pass; d=google.com; s=arc-20160816; b=O22yXml1r79XIlspuIqfJCKB///A220RGxxUlz44CyKNmFrCzZ2ZAGj4BOuZSFDUDm UbQX4w1vm74rhYKQQSGgBXZJPvzRzn2ZGDU00iLpMrtf+d5rtQG7TecJ/ji3In86Z1xM wx6857Hj3BqG/34TfoP8VljbaRhsHqduXWXkQ8ZGqxYOjBvFc3XMXIA/sz8Mu3wBqEFZ eVgzs7YGvcZ1+I05XOCuhfcvO9lzVQemGBFD8J2OYfe6Dr+kjcOEy4FDJGmhbcXO3yvX kd/HlS1sUzbkfMIKxjSUavEhLQYWF7aVLiAqO57Xj/T/rPn+8DdQS/VWBqzWUsT2K18q ksbA== 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:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:dkim-signature; bh=/BiibycOKwwsHFNbtWymeiyuymZWSGJu5tUsVuQRVJk=; b=AkRmVd2WP9gbWMu2tYMuqMh1HjVmWbAlTvh2A6jPR1IIcOlTz3JO3Qs1PkNITzY17W TPu+2h6VHcEvi10dsRyehkYqS+aNodHCOwX46fSe0AfsAS9tdtDQLBvUzfTJ4308jPMH Ri5WYrlIRKuWy0f77RFJl9n1TYcK7/5e3oq1wvxC/NrOkkS6Jb+HEpmUn3Dsy4waJKpc 9Bmqb8IW6SMf+JGbLwNwA63gfen+w6gSNX4wxPDd+XVKQfECv4b9yj7kZNYAP1HwxBc+ kgLelxDV3DOI0uDj+Osxa82zA8yTR5Q7pmyVS6Mg0pTb3vqt7D4lXfOamRotbPd4kz6m SG7Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=r5JiwoCF; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2a 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=/BiibycOKwwsHFNbtWymeiyuymZWSGJu5tUsVuQRVJk=; b=Ww2kodxoC0CX1C6ozNy7i62hpeXBM0HKZi2YIY437gwzIT09xJWprCEjBviTgUNzyk JbhiueD7riQC0d1sC7Se1TaW6O08koTgzXgmCB/85/hOSX5rVCTH1YCPrVuYQZg4J6HO 3MiyeF8lMf8IpEonoSKEdK2aMol2m87e0VHGh99QgHMvTTKzUoMUx0fXDsy6e9KDvDMu S8pC4rt3GithTxoQ6nqUo5EqXe+751qGXUByfG8jQhw6xWWOVYng+dbUXnK9sX7w1pF5 fQo9a9pnQASpg0vrEDNmzOUmlG8OZnUtRY+KsNaENCQJkXmpulvaEvKzctuP2psaWu3u SZxQ== 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: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=/BiibycOKwwsHFNbtWymeiyuymZWSGJu5tUsVuQRVJk=; b=O5gFohbr1evVUPPl4qeaYteLUUS0vuHAzcsHJY2F0I9zgVCnT9FYSAk69Nzg4fiNLr 49XR+x5+wHo6mz1c9wbSA0ieFcpYGxj5Iuf33uT4vbPB72w7mNXzlzIKsAdUepESYLEc QD4X61bWQF6G0kcAh1AaeQH4TKdOe0GRlfIqt1QkEEzyEHVxjoRPt/npzcBJ/HLYxoqo GIosUx/4/Bp9HdXtiCkDiTbOTKWZmEm/ugi+S7zXX4iY9OaIIfdCMoqHuPRp9nIkfVXt rMI5lX6rix8X70M3RUfyZreGcFvrnaCPwXvo/s5suiBbRqYsgC+PkQYsuHPi3LDVbHo9 gDqQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZHqsgGAlBbRfCcCqprwrGsXx3dI35qfy5qEBUE+Of5ZJAJRvxQ lZgv7eKDGoNp63P25mxXID8= X-Google-Smtp-Source: AHgI3Ib3gZIh53oQugQK4JnW71EtDJP/YysFjEBmBlCPYk05juxEXB6yQpOuw8pKFFWsge36GSVBCA== X-Received: by 2002:aca:8c7:: with SMTP id 190mr60527oii.1.1549744462175; Sat, 09 Feb 2019 12:34:22 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:75d0:: with SMTP id c16ls5573622otl.3.gmail; Sat, 09 Feb 2019 12:34:21 -0800 (PST) X-Received: by 2002:a9d:758c:: with SMTP id s12mr11638078otk.10.1549744461840; Sat, 09 Feb 2019 12:34:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549744461; cv=none; d=google.com; s=arc-20160816; b=rzy56fddwzdu4/ro7iJumMsG9WpxWS8mL/DzA6llxjjWJThOi/DRG319TCzA4UtmTL b250NsXmdB0xHwdCbxdFUEvWayhcH/NAHORRs4s/5u8hQrhF6pfgTrZ8PypSDhUiYDm3 nSenLuINdG9tJUJUU4fryKSk1lx7jD69nTC0/2bQreJ9l5VF+QEPi1H5hAyGvqQ9M2yE kyULmHCPxv5xlZ9KNz3VwMEWZArakbi01iyUIuCLZSZS/QXGtpvaU0/DV0jsXszuxVn9 HhqW3auUILPTwAqm0xHtDasomTXLIKSiMLt2ioAbzyEJpy0Um19meNrEdAU/9Z7RUSuD zvXA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=Ge/qCvZlZqaA3hIdx4OGQ4GCWeY/4zTV+kkt7x//IQE=; b=wpPdVqqCJxUqKBWuyUfY1oYL+crftaSJRT3wRfTi5YEYRbSQvfSXhbahBZP+S+6ooT 410wW6bpqQH7Nd7xDebsFL0j2p5KrwlGqFoSbc0ky6FYSGQw8PJvvvQ6prs8TXu1cxRe R5A+b2w0VUqMz0qguoDGMcRPC2jgWkYhBTWZE5kLSQjsHb+cjS5dUH8X75enMgL+PRBG oD7vS5L3JrNx4kFOY+9r2n4CkwdPnuwiQYi/cIoDzspeAEXEoY1zRU3Jt2Nwqe+RTsKp I4RDaDXcNOMy6eLgQP7xTlKbX8ekGTLwwKt/Yoq1+e+qyl/kMh5ih4tgEVqmy2nf8nep BiFg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=r5JiwoCF; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2a.google.com (mail-yw1-xc2a.google.com. [2607:f8b0:4864:20::c2a]) by gmr-mx.google.com with ESMTPS id c13si162711otm.1.2019.02.09.12.34.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 12:34:21 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2a as permitted sender) client-ip=2607:f8b0:4864:20::c2a; Received: by mail-yw1-xc2a.google.com with SMTP id k188so2734257ywa.6 for ; Sat, 09 Feb 2019 12:34:21 -0800 (PST) X-Received: by 2002:a81:a196:: with SMTP id y144mr10957294ywg.270.1549744461252; Sat, 09 Feb 2019 12:34:21 -0800 (PST) Received: from mail-yw1-f46.google.com (mail-yw1-f46.google.com. [209.85.161.46]) by smtp.gmail.com with ESMTPSA id f62sm2170665ywd.68.2019.02.09.12.34.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 12:34:20 -0800 (PST) Received: by mail-yw1-f46.google.com with SMTP id p17so2748075ywg.0 for ; Sat, 09 Feb 2019 12:34:19 -0800 (PST) X-Received: by 2002:a0d:c182:: with SMTP id c124mr22531642ywd.190.1549744459516; Sat, 09 Feb 2019 12:34:19 -0800 (PST) MIME-Version: 1.0 References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> In-Reply-To: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> From: Michael Shulman Date: Sat, 9 Feb 2019 12:34:06 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: "HomotopyTypeTheory@googlegroups.com" 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=r5JiwoCF; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2a 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: , >From a semantic point of view, I agree that judgmental equality is about convenience and usability. But that shouldn't be regarded as making it any less important. Indeed, the whole *point* of using type theory as an internal language for a category, rather than simply reasoning about the category directly, is... convenience and usability. Of course there are degrees of convenience, and even type theory without judgmental equality might be slightly more convenient than reasoning directly in categorical language. But I think we need judgmental equality if we really want to get some substantial benefit out of type theory as an internal language. The problem of course is to bridge the gap between the type theory and the category theory, and for that purpose intermediate structures may be useful: categories that are more like type theory (such as tribes and contextual categories) and type theories that are more like category theory (such as ones with fewer judgmental equalities). But I don't think I would want to regard the intermediate structures as fundamental, rather than tools to get from one side to another. >From an implementation point of view, I agree that in the long run we should have proof assistants that don't hardcode a fixed set of judgmental equalities. But I don't think that means eliminating all judgmental equalities; it just means making the logical framework more flexible, such as Agda's ability to postulate new reductions or Andromeda's framework with equality reflection. In particular, the new equalities that we postulate should still be *substitutive* (as Jon says, allowing to perturb a judgment without altering the proof object) rather than *transportive* (requiring the proof object to be altered) -- I think Vladimir was the one who suggested words like those. >From a computation point of view, of course some kind of reduction is necessary, and it makes sense to consider an object to be "equal" in some sense to the result of computing it. This would presumably be a stronger sense than typal equality inside the system, whether or not it is actually substitutive. Conversely, in order to implement a substitutive equality it seems very useful to have some algorithm that can at least go some part of the way towards deciding it, and computation is likely to play an important role in such an algorithm. >From a philosophical point of view, I think definitional/substitutive equality is very important: as Steve Awodey pointed out some time ago, it represents the intensional "equality of sense" rather than the extensional "equality of reference". This explains why it is substitutive: if two terms have the same sense, there is no explanation necessary for why a statement about one also applies to the other, while if they only have the same reference, then some explanation may be required. If I say "I saw the morning star this morning" and you reply "yes, and I saw it last night", it sounds weird because there is a transport necessary along the equality of reference "morning star = evening star", in a way that doesn't happen if instead you reply "yes, and I saw it yesterday morning". Foundations for mathematics based on first-order logic, like ZFC, have no ability to talk about equality of sense; the only equality they know about is reference. A type theory without definitional equality would have the same limitation. Judgmental, definitional, substitutive, and computational equalities are not exactly the same thing. But the fact that there are so many different but related points of view on similar and overlapping concepts, and so many different but related uses and applications for them, suggests to me that there is an important underlying mathematical concept that should not lightly be discarded. On the other hand, the proof of the pudding is in the eating, and this whole discussion would be much more concrete if we had some actual references working out what type theory without judgmental equality looks like, with proofs of whatever properties it may be claimed to have, and perhaps even an implementation of it; so I don't mean to discourage anyone from trying to develop such a thing. -- 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.