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-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0c676827 for ; Tue, 5 Feb 2019 23:00:27 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id w24sf4347809otk.22 for ; Tue, 05 Feb 2019 15:00:27 -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=/wm86tBZZaPGjhKZdDfn6H/K875FBDWuVeEZtRv9jE0=; b=YxHIH6QFK8txELxSyf3RQZSGrXi2ybCmIDcNko8Kt99u08TSYCDzdjpbOQWleEb9K3 /vcwozr+Iz9y7cwOQeQKYDyGAggoNDCGZDhbd5OZjf9nH0v4cfj0l8MvFD/mlga07vD9 zjFK+lP+0ivAEbMRcBBDKKvjaWPtgghCyNDUWIT1qSIFQqpSiaPZkhP+lQy/oKyj4QGm /mA/xwp7m8sM/XLb+2QPACaRZ0uU5B1Gc3oaCAs8T5QYgPxNxiWOggp6Q7q0krsv0ZTQ 8LBG3cIZ0wFLGuf/P7TVISAoa7/K4uR0fFNd9ct758SoyMmrOt9RBsvj94s+o2Q8QVaO POsw== 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=/wm86tBZZaPGjhKZdDfn6H/K875FBDWuVeEZtRv9jE0=; b=Wzjxn8MB1P1QM0aMLq1SI+RgMTwCadnjBnUUORHfWfUxcGpTt8pkWYpCkkMhl2QVSu /5eytrBWadY2FY/r50+fGHp5S2Q1TbRZDg58TSXFV4tjoO2u0qNNjbDgwzHDkpmZ6lne wTLH4Rg5MUWOJNZYk3hCF09ds6LUurVfvqbmdizUAR+k8MlwLvjK/UEbnLRKC5g8o0Ej a3wnALqU9snM9hpAV6T4fm2wUtL5TovZxkvnnwMWpbabLh6N4BWWOPKwES64X92qOZQQ TcbWvCiHDKI1LN1Xh9YCeQtCbLXSKw6Hpv1jht62SsiBqJGkBtuXYVkGgGvf6J6XqmfG VdDQ== 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=/wm86tBZZaPGjhKZdDfn6H/K875FBDWuVeEZtRv9jE0=; b=VZjfTd0G5OogGcGnc2anAI8V73dWtp8fsK9O7RPBhKgAj9lMIOnKc6wlGDdxCOWuVQ O2+Cv8KijP8qKUSlwsTNlO/YBkfkPo0zrosreGXGyVrd4epLoRTJNCu8K1DrqlSY46/T Blv1MhoZbm0XoEVsWb9/7TRRqhSygokKKZet/ewhcB+8dId+/0xPWe7hg1V4dRJApcFD LWRwMWTDcXoisYdyHgw+tqxH97DUbIaLHqNNB9KVOOzgTy88YFrt5shwTCQfYgTXKYyr J78OeVgORTSBsAj6KIgpjcTKLUbarzuVRiRTJWw268W+/fHB5w1OU78+hEGkfF+LouHY ptSw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubOHQvVxca5T+wK2K0d5mLhiXjJfo5ZHTuX0fO3ZZUsAMpbu9Id q+G1+EuuL1v6l9xrNr08+ZM= X-Google-Smtp-Source: AHgI3IYcQ7yRq0bP5nfsI4HAy1fxEY/qxGMqcsWx1PJ2kgoEfmr442/4R4G2PAV21/Omg6HwCVYU7A== X-Received: by 2002:a9d:6f9a:: with SMTP id h26mr83171otq.0.1549407625173; Tue, 05 Feb 2019 15:00:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls1479963oip.0.gmail; Tue, 05 Feb 2019 15:00:24 -0800 (PST) X-Received: by 2002:aca:308d:: with SMTP id w135mr90033oiw.0.1549407624712; Tue, 05 Feb 2019 15:00:24 -0800 (PST) Date: Tue, 5 Feb 2019 15:00:23 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <6f42d617-be71-4ce2-89e2-8c9a27c178c9@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1894_1914707173.1549407623910" X-Original-Sender: atmacen@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_1894_1914707173.1549407623910 Content-Type: multipart/alternative; boundary="----=_Part_1895_111182834.1549407623911" ------=_Part_1895_111182834.1549407623911 Content-Type: text/plain; charset="UTF-8" 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_1895_111182834.1549407623911 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
The type checking rules are nonlinear (reuses metavariable= s). For example, for function application, the type of the argument needs t= o "equal" the domain of the function. What equality is that? It g= ets called judgmental equality. It's there in some sense even if it'= ;s just syntactic equality. But it seems really really hard to have judgmen= tal equality be just syntactic equality, in a dependent type system. It wou= ld also be unnatural, from a computational perspective; the judgmental equa= tions are saying something about the computational behavior of the system.<= br>
On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote= :
In sect= ion 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 tr= ansports if one added a few sensible rules to the type theory. Is there a f= undamental 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_1895_111182834.1549407623911-- ------=_Part_1894_1914707173.1549407623910--