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-x337.google.com (mail-ot1-x337.google.com [IPv6:2607:f8b0:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 95c307b1 for ; Fri, 8 Feb 2019 21:19:26 +0000 (UTC) Received: by mail-ot1-x337.google.com with SMTP id q16sf4372963otf.5 for ; Fri, 08 Feb 2019 13:19:26 -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=ejkjDPVau6ihMWPrS54SBkC1aEUXEJO6dfbp6OyX6BE=; b=ep330tWM3Dum2fMacD7PM5XqjDOksIh5mLT94SzhzJDbeg9wIdN8jb6RhzrX9R3+D3 jAR/nSvlJ34GPTIQBiPO1/x7pIUMiv6xB2wfQsxlG3KcyHo7nuAdo1zdMkGCCwiq9NEI z8dmhzwXhRov1uYF02PkUVH7lEgcComHA87djsf6vioxpxREbnDEcJydJ/1y5+p3elPS WUUqsSMqNbeA9TOlP3zlm/ngowUP7njevikTOULQC9N92z2tuAoWOlWStdysueYPNNqv 1DoFAy34Fp+GODroAHvM9VIFJFlP4QBkccNrM8l5NUdVLvmqk1g9CHsGB+xw79zAk+21 wN9w== 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=ejkjDPVau6ihMWPrS54SBkC1aEUXEJO6dfbp6OyX6BE=; b=fwdRyxgRDpwzaPNIUrAZy4Elfo1dxYkRG3b+qJ26S4nQmkVPMRLhoW35UGjl29nBz2 jsp7Pti3CR5xrzspfozln6aT3lHVex0HQVXuMtDnGCbgbzpNq1PUCyKWHKQn0K9Lzf3A 2K2gvf6wv8qS551E/iNaroQLJBKWtizJJoqCorOLIknrPpF+frozFQf1vO1wXLAnW2JL /mFnN8nvbZscreAd+i1T5WPcgQgWVhEKewHS7Bx3xO/+KCksq8xLVDXjbuovDl+BW45z hM7ZBeBNqnPxOG+kExPRaIiyoEf6HG9nTP7qD99IOfJ7Sl1WBG4L4CWdd3PBKh0U48o+ 7aPA== 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=ejkjDPVau6ihMWPrS54SBkC1aEUXEJO6dfbp6OyX6BE=; b=qXqfNtcfl8XI+zgDczpHktyNZmyl7SD8PVJKBQjio8vpkBrlLhMrIliuN81Y6d+ne9 BCrg/YhTY6g4788VUlbTkAUfKzq7Dssec0KYFSU5L31tEJUfE/9vdHNbVMz4pMfBiF+G 0nZRqWoIpUfRAPeDYlhef1n8Zpqv+M49dZgKk6JI6auDvNf8uMRVU1mrMKtoqhlVVYS7 wMuIAYBRzI5KbBMASCvW5RwpXpp5rsrIvVcf7mBjTC7n1MuxuCJUuEaSCgHU+ukJSWsf c4B786EPXM2DvJbXMeNSJZRK97ahGF5md3NzWepam/04yfu23PGa6CfWCHSzX9+1Mv7Z WefA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZgrFSay3DQlQf5XFDqU5Y0gmK6U6roAKdHmkmv0GRZfSKUpO5f mX5oNGf+vcV9VB6u64ZdEF0= X-Google-Smtp-Source: AHgI3IZNq6K4IGORk9RAKuByBv4fJ3XxvzmkkVyXIyEJI4RSAsbIaV1nBLWN4VbaWH37f5PqIeP+NA== X-Received: by 2002:a05:6808:1cd:: with SMTP id x13mr22239oic.0.1549660764927; Fri, 08 Feb 2019 13:19:24 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2c62:: with SMTP id f89ls4280446otb.2.gmail; Fri, 08 Feb 2019 13:19:24 -0800 (PST) X-Received: by 2002:a9d:2c22:: with SMTP id f31mr304609otb.4.1549660764384; Fri, 08 Feb 2019 13:19:24 -0800 (PST) Date: Fri, 8 Feb 2019 13:19:23 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@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_478_1810909438.1549660763861" X-Original-Sender: escardo.martin@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_478_1810909438.1549660763861 Content-Type: multipart/alternative; boundary="----=_Part_479_137548224.1549660763861" ------=_Part_479_137548224.1549660763861 Content-Type: text/plain; charset="UTF-8" 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 purpose of serving as a foundation for univalent mathematics) that doesn't mention anything like definitional equality? If not, why not? And notice that I am 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 that 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 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_479_137548224.1549660763861 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I would also like to know an answer to this question. It i= s true that dependent type theories have been designed using definitional e= quality.

But why would anybody say that there is a *need= * for that? Is it impossible to define a sensible dependent type theory (sa= y for the purpose of serving as a foundation for univalent mathematics) tha= t doesn't mention anything like definitional equality? If not, why not?= And notice that I am not talking about *usability* of a proof assistant su= ch as the *existing* ones (say Coq, Agda, Lean) were definitional equalitie= s to be removed. I don't care if such hypothetical proof assistants wou= ld be impossibly difficult to use for a dependent type theory lacking defin= itional equalities (if such a thing exists).

The q= uestion asked by Felix is a very sensible one: why is it claimed that defin= itional equalities are essential to dependent type theories?

=
(I do understand that they are used to compute, and so if you ar= e 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 de= finitional 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=C2=A0


On W= ednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote:
In section 1.1 of the HoT= T book it says "In type theory there is also a need for an equality ju= dgment." Currently it seems to me like one could, in principle, replac= e substitution along judgmental equality with explicit transports if one ad= ded 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 &= 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_479_137548224.1549660763861-- ------=_Part_478_1810909438.1549660763861--