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-vk1-xa3b.google.com (mail-vk1-xa3b.google.com [IPv6:2607:f8b0:4864:20::a3b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0938b447 for ; Fri, 8 Feb 2019 23:32:16 +0000 (UTC) Received: by mail-vk1-xa3b.google.com with SMTP id d123sf1755484vkf.23 for ; Fri, 08 Feb 2019 15:32:16 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549668735; cv=pass; d=google.com; s=arc-20160816; b=k4ArD5GltBXmQhln+bPlbeJkfyj71Zqs+SIAUXinkzIoWXAX+XLpi4uXo38spsw0QM gpj+n8DzXcHpmcZpJxfvsWXB4uwKGQ/gPmBOshNGBwSUjkgkD+t3uuiCEWo9cXzmF123 9vjck0jUQF53Mx5RjXuDKCrd5jv76QgDGxbYAhHzF6MnJ45u0fEHusWZeJYtr/Mnl4NB LYSm/padyaUkjIg9ucVtwaPbKH7uY0rZk8dAyp3lIRwJgeYalOv/lGNJOZHBYFNSanyy WiL/+9PVgGlugK+MugJiWPiaa6SnAwRI/5xpmUFTnyvjp67i8Oz8iXyUC9S55TsOfegQ VKyw== 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 :dkim-signature; bh=mBdLAiU7vHdOE87cK8661GxooDRqJc91ojWKNd+1qxQ=; b=IqTTCcJQeBJW7NiXa9fiAhcajuBEKMeRy8cu46qwi7GCs47BHnNMC5cGkouVXxJ971 1RfvqhDnpp3KEhN3B8mDK7KcSoNHhHmZfRT+yyCZmsQ2nG9Fovp7L9K+NakoqZgNH3k/ xw/Oi6cxOUoUL6oTzrlatT9BI1c2x4nqvzp3FTNsfPHznXpHWHxRekpm/sYARVgsOWTM VR1i5X6/S3KrQQKmgGfLCPf8Xh9ghP9a+Co983QvZwpxvJZIzv0Fa+X9+OkcXWXSi8bf MSmWF0NFR3ZCaE1ey7rQmCjlyO8jKtPRNjnWaravJGpfiEVEWumaIf9bL9Jzat1XW13a tzug== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DvS/+xb9"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::133 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=mBdLAiU7vHdOE87cK8661GxooDRqJc91ojWKNd+1qxQ=; b=li0ZA+lAKvwfBotE64ON3mjY3vioFzz3YJNXWbeMh8ptH+TOSas9mqtvMoWi/2q0i1 KAkIDMyKZsNJsjVCdlKKwX8APvPDG9YnD73OrOQpdfThxxQCUTZT1a2JKnMu/qzZ6vMF 1bvjowZY3KhaKuwtcC4pMjSKXsvav8pua1ryEsM8tG/hzG2UFNy2BWm3sOAxxg8909M6 vNS50veUWnPlOF4g0FArW1KuG91zaJEN9snWSA+SIqSSCZqt3bEIzYN5Qti7aw2Ha5d5 vZo9N7G4TYZaaU7ZeieDDVaB2DQ3AW84epESlK+gvHR7SdE9szIShpkg1wRGHkFIx+s3 IlRw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=mBdLAiU7vHdOE87cK8661GxooDRqJc91ojWKNd+1qxQ=; b=Q/jBM3Htxi4JP9RUSqdXUt+W2pSQQPazgfgQtgZyEr67Te4wkZITi+0IYbizeMF4yN wozEFI+mSoY648BZn0sDrMAQCqC0U6sw7mWJwlaeyj8m1VUULrlaxzFfDoe6K7wSTgmY 1+l3NoKQAkkJgSF5dUFvuLnueOu896V/6ZsSEiL4n1nWsyJCxeHpB7Bt1mwrUq+lAO4M HO+iR9aFJvdS6K13KiATipvDgJSM4zuesOqRO9ih0DbI0R/MsGFikPbHibLbUOAnvaOB EUjeuUVRTFj1Wa6Ud9adU0DPD5a/hfE7mYdopIfKgAiIXhE3xnUWmD5Z6b/o/tiNV+Ql 4Y4A== 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=mBdLAiU7vHdOE87cK8661GxooDRqJc91ojWKNd+1qxQ=; b=L2974vO8OSvrN6PseyWOKG3LCJ1XKd0/2t/XVUbINkGLbCKy9JhhLYBviVi6gFfkBS 4Ud2Ip4OxJ15mfCRDx8bMjmxqmMLipAwyCHPfqrvRckVTZKiYmhGfrJYNkIQ32xRtRvr 5CUtg3z77/fN1329rSGqKHnQoKTz0hqY/QRMuzkP8ZRP3l68prAkfOquaJUXc3NwBIt9 9hR118BKZpY6E5zwRDR0MJK1gYAO/utURtGmj7A5sUTGjJzN+t85M5RJqMDirSsFZM2D 7ynhgd54nhuogM9WyTlOTSgolI/DGjZUGd1hoWFF72fX1zBSAuB+tEOgBmexWASoYVSD 1dMQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYczDJNNNWMRXmqwwspjeIRm2iRHcJgalEa4FROnQpRBHx5S9EH C7ZMF01dCDMKeGTAs+P0Jp8= X-Google-Smtp-Source: AHgI3Ian4b4lnvwA/2gQZ/pI8cSFJzVPem59KpHmtxf8L8u2cSP+4jUyb/cJQD2LjMehsqX31em53g== X-Received: by 2002:a1f:9793:: with SMTP id z141mr32382vkd.7.1549668735465; Fri, 08 Feb 2019 15:32:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:9d0f:: with SMTP id g15ls1270908vke.1.gmail; Fri, 08 Feb 2019 15:32:15 -0800 (PST) X-Received: by 2002:a1f:9b4e:: with SMTP id d75mr15945406vke.10.1549668735126; Fri, 08 Feb 2019 15:32:15 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549668735; cv=none; d=google.com; s=arc-20160816; b=M9Lr2RpuejGsw16VioMnGcNBPiO0BmQRpyuop3rZpYAwgiaBXAw6Xo3D6jJdL3qHDp i97ZDHmPH7hvphl2bhlnpd5owwhAfk/7sLESXQ9ihho4vUInyxh8K1imHAldzJo94OAH 6y4yNLcxK4/gWtXs8uWDV4jt69imWkuMZUfKZgtXjWstzu5FedzhMVRm/hXwkZ6tlFYq W/cPuA447wlLhtozgLM/F46XNR0G6nTx79/kgI0D4krz/kAK9Zx301jyi+jCHQiWkMl4 IDqFqWKiaugjmfaE/3J6opYOLpigMzok49/9UQWhZc2Oe0G4tDIdzIvBcPu1RnsSjqju r7WQ== 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=sZb6ImIcPMIdY3iwTxFPJRRONnHTOaA3Mj1iJkxX3uk=; b=QzL4e9P315VmdB171NUzVmW/RlePX1V4ZqxbqlOzf1DRVPDqlQR4YLGJNT1G2KsgTU K0TkxGFjaliKKJqgyjVyvqM5UTsg795derGP8h+krLyLPFlXd/ihoXUR5R0Ow92ocYsr J6igFk0fWHdVdxAuZvoju21bsdek7IhlIm7L0iig4Y/4jQw7ldYiIOxVLkRbJ3ir8Dx6 NLxAttibBNjJohveF5jk8SgqfJDEKHS+Svz8MrQwG8WDrGHY8611GtFyVp53hPYmq8tN wCeA3kpECevmgZcyQVs89McMV1LV7OUNBjAoXa/zxoUKYjtVmZEGdEAnsYE8QOTkG5dI Vmyw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DvS/+xb9"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::133 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x133.google.com (mail-it1-x133.google.com. [2607:f8b0:4864:20::133]) by gmr-mx.google.com with ESMTPS id v188si247811vka.1.2019.02.08.15.32.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Feb 2019 15:32:15 -0800 (PST) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::133 as permitted sender) client-ip=2607:f8b0:4864:20::133; Received: by mail-it1-x133.google.com with SMTP id i145so13054589ita.4 for ; Fri, 08 Feb 2019 15:32:15 -0800 (PST) X-Received: by 2002:a6b:6305:: with SMTP id p5mr3733550iog.92.1549668734744; Fri, 08 Feb 2019 15:32:14 -0800 (PST) MIME-Version: 1.0 References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> In-Reply-To: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> From: Valery Isaev Date: Sat, 9 Feb 2019 02:31:38 +0300 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000743e5005816a5e8d" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="DvS/+xb9"; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::133 as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000743e5005816a5e8d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable If you are not interested in computations and convenience of your type theory, then the definitional equality is not essential in the sense that every type theory T is equivalent to a type theory Q(T) with no computational rules. Now, what do I mean when I say that type theories T and Q(T) are equivalent? I won't give here the formal definition, but the idea is that Q(T) can be interpreted in T and, for every type A of T, there is a type in Q(T) equivalent to A in T and the same is true for terms. This implies that every statement (i.e., type) of Q(T) is provable in Q(T) if and only if it is provable in T and every statement of T has an equivalent statement in Q(T), so the theories are "logically equivalent". Moreover, equivalent theories have equivalent (in an appropriate homotopical sense) categories of models. Regards, Valery Isaev =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 00:19, Mart= =C3=ADn H=C3=B6tzel Escard=C3=B3 : > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpos= e > of serving as a foundation for univalent mathematics) that doesn't mentio= n > anything like definitional equality? If not, why not? And notice that I a= m > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > The question asked by Felix is a very sensible one: why is it claimed tha= t > definitional equalities are essential to dependent type theories? > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > Martin > > > On Wednesday, 30 January 2019 11:54:07 UTC, 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 ther= e 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. > --=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. --000000000000743e5005816a5e8d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
If you are not interested in computations and convenience = of your type theory, then the definitional equality is not essential in the= sense that every type theory T is equivalent to a type theory Q(T) with no= computational rules. Now, what do I mean when I say that type theories T a= nd Q(T) are equivalent? I won't give here the formal definition, but th= e idea is that Q(T) can be interpreted in T and, for every type A of T, the= re is a type in Q(T) equivalent to A in T and the same is true for terms. T= his implies that every statement (i.e., type) of Q(T) is provable in Q(T) i= f and only if it is provable in T and every statement of T has an equivalen= t statement in Q(T), so the theories are "logically equivalent". = Moreover, equivalent theories have equivalent (in an appropriate homotopica= l sense) categories of models.

Regards,
Valery Isaev


<= div dir=3D"ltr" class=3D"gmail_attr">=D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1= =80. 2019 =D0=B3. =D0=B2 00:19, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 <escardo.martin@gmail.com>:=
I would also like to know an answer to this question. It is true that dep= endent type theories have been designed using definitional equality.
But why would anybody say that there is a *need* for that? Is = it impossible to define a sensible dependent type theory (say for the purpo= se of serving as a foundation for univalent mathematics) that doesn't m= ention anything like definitional equality? If not, why not? And notice tha= t I am not talking about *usability* of a proof assistant such as the *exis= ting* ones (say Coq, Agda, Lean) were definitional equalities to be removed= . I don't care if such hypothetical proof assistants would be impossibl= y difficult to use for a dependent type theory lacking definitional equalit= ies (if such a thing exists).

The question asked b= y Felix is a very sensible one: why is it claimed that definitional equalit= ies are essential to dependent type theories?

(I d= o understand that they are used to compute, and so if you are interested in= constructive mathematics (like I am) then they are useful. But, again, in = principle we can think of a dependent type theory with no definitional equa= lities and instead an existence property like e.g. in Lambek and Scott'= s "introduction to higher-order categorical logic". And like was = discussed in a relatively recent message by Thierry Coquand in this list,)<= /div>

Martin=C2=A0


On Wednesday, 30 Ja= nuary 2019 11:54:07 UTC, 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.&qu= ot; Currently it seems to me like one could, in principle, replace substitu= tion along judgmental equality with explicit transports if one added a few = sensible rules to the type theory. Is there a fundamental reason why the eq= uality 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 https://groups.google.com/d/optout.

--
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.
--000000000000743e5005816a5e8d--