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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e6b2785e for ; Wed, 6 Feb 2019 04:13:37 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id r15sf5080278ota.0 for ; Tue, 05 Feb 2019 20:13:37 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=iINdXTKy4QZd4wVopYscXvocHp2iAbJSW5d48YptqvU=; b=Sc32pDmwpjJbeUD4W31DuQhNNZHJmoIe7+siSpqtn3E4AZejIMnybAhotlwJlXwAZP MRCrlITCEAO+fKmVbWr7G65ZVxlWDB3Yfwg+UIHbN6kiC3M/eP7Pp3dqGviikW8dUvvH 38ZZAbKxyBtr+m0jRAHRuZnZZ+5DdFl9dXfEpdZM+4IXWwF2vk+X6rJEXpZMxEe0o8nn NssC6Y4G7QwE+rIOATx6SQjjASWWSIgogPXtLE23ZnjGmR7eePzo3eExfFORDNKwDDKd L+aBN/8mCJ01qiuuQcXOoKmpaOorOCZdwCUSIyPKk4ihTcOx6q8F3JFHPZ3xm/2LldrD bWcQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=iINdXTKy4QZd4wVopYscXvocHp2iAbJSW5d48YptqvU=; b=RKDBr4d5XwlqR65b5dszOFV2yF0m90xFVvFhyAkHH/xw3/MmnabPqM/mwAYR3HtlkO HpMkfjdphPVfSEMSrVHFu1ZJBi7F9voogrjV/zbUN4rSQWuNrvPGeZrLe1BH8+sTHxFk uQW0YFsasIEkAbIP2fG171UXwaLGC3dEcsaQSG3UberuIW1NtSAb/axYt+VpQZgqjd5C C7WxLI7yMKJxYWM3oQzndC8dj1jrZPKt1ZhvYQSGk2Ai8X0OBmvLG2f3M6CVh7CVQVRl oKDUtjxLJeZjTZspYcogYALatbaBjw/+NJerf5XbxLma7psEeNSKwDjHk/sKsIUWlNAP zCMw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=iINdXTKy4QZd4wVopYscXvocHp2iAbJSW5d48YptqvU=; b=m2ll/zdAixq4F+tDouhFtdm37bxDVo0xW8Y3nFY1Hh4NxyhyKVfO+2xFJkYY8IrX21 eUFdnVjZKWwgXKFU3gtl8IaP0K17OzeRXWt3zSPZOaPfDLb4oZSDURMd9Ym4cSOMyBCg g4mTw63dAcj8NDMP8frK/z6EeMLhGmP9ksDV8gpOvFqlETwc4G+6wiTamFUhrvo6xK8S wz5IbhkNicLFSr6Sj2uEQwGyYvhK29r12xaxDy2nqwi+nLHrbrQBgB7U0bswZz9sdkE1 GZH3oXR1FmUU4nrQYxVLz22OipeebJbGN1Th1Zb1lecWUHveHeK6SjYEdbmfXxS2ZcMV 1v0Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYbImLeulKNoLB+C/6k/l/+00o0w1eYY7RVA+oyLn6AllpVMQ9I uSiZKZ1NFguM97BMDkabIaw= X-Google-Smtp-Source: AHgI3IYWdx627Nb341hxULO8CIQ+r6W91wJUJTWjvLgnDmDLRZLcbEAXG4Xs29qSGy1BctGOycWDrQ== X-Received: by 2002:a9d:117:: with SMTP id 23mr39783otu.5.1549426415966; Tue, 05 Feb 2019 20:13:35 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:5412:: with SMTP id i18ls1758325oib.5.gmail; Tue, 05 Feb 2019 20:13:35 -0800 (PST) X-Received: by 2002:aca:c703:: with SMTP id x3mr98205oif.5.1549426415531; Tue, 05 Feb 2019 20:13:35 -0800 (PST) Date: Tue, 5 Feb 2019 20:13:34 -0800 (PST) From: =?UTF-8?Q?Anders_M=C3=B6rtberg?= To: Homotopy Type Theory Message-Id: <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com> In-Reply-To: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> References: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1955_1644256269.1549426414910" X-Original-Sender: andersmortberg@gmail.com 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: , ------=_Part_1955_1644256269.1549426414910 Content-Type: multipart/alternative; boundary="----=_Part_1956_1793140638.1549426414911" ------=_Part_1956_1793140638.1549426414911 Content-Type: text/plain; charset="UTF-8" Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type. -- Anders On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote: > > The type checking rules are nonlinear (reuses metavariables). For example, > for function application, the type of the argument needs to "equal" the > domain of the function. What equality is that? It gets called judgmental > equality. It's there in some sense even if it's just syntactic equality. > But it seems really really hard to have judgmental equality be just > syntactic equality, in a dependent type system. It would also be unnatural, > from a computational perspective; the judgmental equations are saying > something about the computational behavior of the system. > > On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote: >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could, in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is there a >> fundamental reason why the equality judgment is still necessary? >> >> Thanks, >> Felix Rech >> > -- 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. ------=_Part_1956_1793140638.1549426414911 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Note that judgmental equality is not only a convenien= ce, but it also affects what is provable in your type theory. Consider the = interval HIT, it is contractible and hence equivalent to Unit. But it also = lets you prove function extensionallity which you definitely don't get = from the Unit type.

--
Anders

On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote= :
The type che= cking rules are nonlinear (reuses metavariables). For example, for function= application, the type of the argument needs to "equal" the domai= n of the function. What equality is that? It gets called judgmental equalit= y. It's there in some sense even if it's just syntactic equality. B= ut it seems really really hard to have judgmental equality be just syntacti= c equality, in a dependent type system. It would also be unnatural, from a = computational perspective; the judgmental equations are saying something ab= out the computational behavior of the system.

On Wednesday, January = 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote:
In section 1.1 of the HoTT book it says &= quot;In type theory there is also a need for an equality judgment." Cu= rrently it seems to me like one could, in principle, replace substitution a= long judgmental equality with explicit transports if one added a few sensib= le rules to the type theory. Is there a fundamental reason why the equality= judgment is still necessary?

Thanks,
Felix Rech

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
------=_Part_1956_1793140638.1549426414911-- ------=_Part_1955_1644256269.1549426414910--