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-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c5ab0476 for ; Sat, 9 Feb 2019 12:39:48 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id n22sf5740293otq.8 for ; Sat, 09 Feb 2019 04:39:47 -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=5uld7cLY5ACmBOM6Pq+THPNKXM4PTuoH12RVTSmj9s0=; b=cqqbUSkOVAhhzYAJhaA/GGYMkvQ5LuJv/DyCZZ+qy4ek29iXnSEkhX9nxvLYbofAxi Z9DtGad89tZD8Lbta910lJrc6pzdQTD674zmYJ5oKXrVHXd4hW2w/R9gvuwmmCe7XJQ2 WPz6sDsvY393tN5ena4P055t2ov4qY2kUK1MJpU7HW2R5ivFWWqNiO9/oK8KPPzErsc6 ITNIM1hLXMSE5m1iJ7LZ9bal9ZrBSUmTw+xpmedqrYmpYg15J4VIrgL7SGEQKS1tRFYL GIyFhPEidwweVDvU7K2+i9I0F3V3ASmZGJWalyTcZ05Q1Q7mU1If3hghtcagKqGEDbXp 0BQw== 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=5uld7cLY5ACmBOM6Pq+THPNKXM4PTuoH12RVTSmj9s0=; b=p4jdxQz50E/E/miVJrzWulTrdA8jlYjxnaH+HXXj7cHrI58G5xPnlPpcmkBcRiegyN YRi9LMZSsXlmZeNWgRG+i33TKx1df81kYO/f4Ql1wH29qb3xjh9hqRVdWG+90bDZe4mx Dpma8J+N+9guOe0DKKdM/hkElx3DU0Haq2BJgdJ/qzUfrRvMEdfqtJ+i7FqkQdWmkr1a nfFH15j2IIcSeJO4p0GgmAlFItq+LRLisx8Hd9Ab5Er88m/sP8+m/9P1Sdm8IUH6c/sx yp6bYB5QaaQpcJrojT/pKV0nm7h+DIDE7zbyt1e6GlMqQ/HBtynIek/a7cIwdRa6ffSF CZjQ== 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=5uld7cLY5ACmBOM6Pq+THPNKXM4PTuoH12RVTSmj9s0=; b=IXMp4h+1MX8x5/Ee8usEQZQ7rStd/md98DEfxJlhQHZ8yKkSwOjquPcMKAt1RYgLOr v0oq3QdBN4i7ZL9nTcwKLyLd08uwi4P0gM2EMdaQHUXPBsMaaumnSbDzKRdwyU12LNp0 SDZ9uiWL1zdHRl81hJzPWmPwlOwibiJ49lDDKeGpJOY/CKpHswz/zq51N1dvd7Heq3wi kbyDDIoWRPzhg3MfM8PTC9bkb4LJ5OOQk+FyXP/C2kItLXT7u5sTtJ2tcdXYTStAXpzx X5+FyuHLz4eZ0HzgiWnZ9ncjRAoW1hunbIv0bUwqpUSmVYUXJKyouY9BXd2N+gyLwylF 5HJA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZXZcjIbMskkPWrpZlxmIFnS/++YhLdoKXVCEjGjOEtiHtHfAAA ThMrum3ky2dItYxQF+ED8BI= X-Google-Smtp-Source: AHgI3IZwtfuD216UY7u32IMK/MTkGQqqP6d8OvvCATwKaqKanb3/EhzPMA8rqyuZ+fO5tijUaFnX5g== X-Received: by 2002:a9d:3476:: with SMTP id v109mr45275otb.7.1549715986967; Sat, 09 Feb 2019 04:39:46 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4d98:: with SMTP id u24ls3605083otk.7.gmail; Sat, 09 Feb 2019 04:39:46 -0800 (PST) X-Received: by 2002:a9d:da3:: with SMTP id 32mr346741ots.3.1549715986387; Sat, 09 Feb 2019 04:39:46 -0800 (PST) Date: Sat, 9 Feb 2019 04:39:45 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: In-Reply-To: <971e73a5-da33-4793-bf18-63e15bc80c28@googlegroups.com> References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> <971e73a5-da33-4793-bf18-63e15bc80c28@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_682_1602001501.1549715985849" 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_682_1602001501.1549715985849 Content-Type: multipart/alternative; boundary="----=_Part_683_1376490278.1549715985849" ------=_Part_683_1376490278.1549715985849 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 09/02/2019 11:57, Felix Rech wrote:> On Friday, 8 February 2019 22:19:24= =20 UTC+1, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: > > I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are=20 useful. > > > I agree that the ability to compute canonical forms for terms is > essential but one does not need to integrate computation into the type > system to do that. At least, one can alway interprete terms of a type > theory without an equality judgment in a stronger type theory that has > judgmental equalities and do the computations there. Yes, this is what I meant by the sentence that follows the one quoted above, which I quote below. Also, you don't need to compute by reducing equalities. In fact, most functional languages (e.g. Haskell) when compiled *do not* compute by unfolding definitional equalities. On 08/02/2019 21:19, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:> (I do und= erstand that=20 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 --=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. ------=_Part_683_1376490278.1549715985849 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On 09/02/2019 11:57, Felix Rech wrote:> On Friday,= 8 February 2019 22:19:24 UTC+1, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote= :
>
>=C2=A0 =C2=A0 =C2=A0I do understand that the= y are used to compute, and so if you are
>=C2=A0 =C2=A0 =C2=A0= interested in constructive mathematics (like I am) then they are useful.
>
>
> I agree that the ability to comp= ute canonical forms for terms is
> essential but one does not = need to integrate computation into the type
> system to do tha= t. At least, one can alway interprete terms of a type
> theory= without an equality judgment in a stronger type theory that has
= > judgmental equalities and do the computations there.

Yes, this is what I meant by the sentence that follows the one quot= ed
above, which I quote below. Also, you don't need to comput= e by
reducing equalities. In fact, most functional languages (e.g= . Haskell)
when compiled *do not* compute by unfolding definition= al equalities.

On 08/02/2019 21:19, Mart=C3=ADn H= =C3=B6tzel Escard=C3=B3 wrote:> (I do understand that they are used to c= ompute, and so if you are
> interested in constructive mathema= tics (like I am) then they are useful.
> But, again, in princi= ple we can think of a dependent type theory with no
> definiti= onal equalities and instead an existence property like e.g. in
&g= t; Lambek and Scott's "introduction to higher-order categorical lo= gic". And
> like was discussed in a relatively recent mes= sage by Thierry Coquand in
> this list,)

<= div>Martin


--
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_683_1376490278.1549715985849-- ------=_Part_682_1602001501.1549715985849--