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.2 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-x33f.google.com (mail-ot1-x33f.google.com [IPv6:2607:f8b0:4864:20::33f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id f7577a31 for ; Mon, 11 Feb 2019 06:58:13 +0000 (UTC) Received: by mail-ot1-x33f.google.com with SMTP id j23sf10250754otl.6 for ; Sun, 10 Feb 2019 22:58:13 -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=Wtu5kH3E0jvb5LdxyS18F4ue/NxZF2kWLNGIub8w46U=; b=Af1MvlQ+6EUyeB4qvVXsN/x7nMMNzDt/MSs20zT5The5Wfg6rLkMLK1w1nGINCponl d7jqrqLlycYF1vri47qR2J2KEWoH27BsDgGDkhgUpI982VpI6WGLkpT6Tq6Ao2atPgw8 nsVnlpCmGs7vJQWFKF8aURGf/v6BNAzWzQMKImyP6rWIAjQuPtHy72vNYnDhjJUbuktf Rqml0FyD6yCEdWpvWAotf47t6whpaXBJkde9OA9+jVXODrMhNLUJML4qp8s+m3jtnJeX k1fFyKwwt82fLh6LYnEKU40vuYnUupSeJkPVKBGcQoWCqAgn6wbI4Siu780znvOC95qr dqzA== 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=Wtu5kH3E0jvb5LdxyS18F4ue/NxZF2kWLNGIub8w46U=; b=UKA5wgwhh+kpSmLjyHdi4Nu6GGfyzGeB2dTyw7Adcu/wSsiBP61vJhsygoYrzAWmqx pkbwhWUDVk0AN2VwM91o4hLCZPG92Q8VlWPz/yg0WH6/z4JPQuvJWeI4aiJkiHXB/qWM zvDM0pkrTwqmvZ0olcdVEln75NB1Aq0P+wI3KgngnQlA8oPsLqhPXXUIr4PagSXIVnsc P08+bwzcsmBMPT+/fGcYGeZ6yRxiFy3eOTf/yWFJgWj9hj3Fe9omXZEh6svdmI136Yta WfZOkl3IAWS0Wr5Iik1USaGFnn4wa1yhP7voJAXV+usuOlG3NpDdbvagxTT8Igqzejwl 20Ew== 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=Wtu5kH3E0jvb5LdxyS18F4ue/NxZF2kWLNGIub8w46U=; b=aPDPOP6pw0RLlZmdl8xyRbpjbtx+XdM3qAOvL48ijmf24rulVGS+0UhpmAxyijH//S 0oigN0RaK6V0iWXh2KoBYILP1L9iECZfs4y1fH2V9s1qVo3aXgAyoluDfg5HZfHEWLt2 HnTNmKelk1f5U/tLsF5WQG7vqzE0YtPmcoIeC6mkpa4QRbOZ7U3bqzay8Fyj5b7LroJp IZ6h3t/QycLEPZPSGc+5wRzmpXNjdGKNphg/v6MPrFSA/Kf85/yBFS8x02PGiDAIyqgJ D1+G38HL9T2wdJ2QkvxIlRa4uq0mi1iG/Bhrb6nx3C+aiJflGIc8VaOVeyyFF7hasLeS cZVg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaTG5U5LsiZWJBYVSnsaE4W/lBsX+UO6+BYDNUJZHyobCpjFaz2 rRP7TiQBhWZp5dcDfoyKOzc= X-Google-Smtp-Source: AHgI3Ib7DRfAvCPZqaoxU3GGcyKc9M3MbtH0XXKGFv1vxJQTdTswYaRbJYFEhBa/foP37qNW7OVQEQ== X-Received: by 2002:aca:df55:: with SMTP id w82mr5254oig.6.1549868292182; Sun, 10 Feb 2019 22:58:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls4987278oip.0.gmail; Sun, 10 Feb 2019 22:58:11 -0800 (PST) X-Received: by 2002:aca:df55:: with SMTP id w82mr5253oig.6.1549868291844; Sun, 10 Feb 2019 22:58:11 -0800 (PST) Date: Sun, 10 Feb 2019 22:58:11 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <47ad1443-4359-43ca-8a8d-2cf7bc6aa7b5@googlegroups.com> 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_1048_801624903.1549868291151" 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_1048_801624903.1549868291151 Content-Type: multipart/alternative; boundary="----=_Part_1049_1978017938.1549868291151" ------=_Part_1049_1978017938.1549868291151 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable If the stronger type theory is not conservative, you generally can't draw= =20 mathematical conclusions on the basis of those computations, though. On Saturday, February 9, 2019 at 6:57:51 AM UTC-5, Felix Rech wrote: > > On Friday, 8 February 2019 22:19:24 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=20 >> interested in constructive mathematics (like I am) then they are useful. >> > > I agree that the ability to compute canonical forms for terms is essentia= l=20 > but one does not need to integrate computation into the type system to do= =20 > that. At least, one can alway interprete terms of a type theory without a= n=20 > equality judgment in a stronger type theory that has judgmental equalitie= s=20 > and do the computations there. > --=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_1049_1978017938.1549868291151 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
If the stronger type theory is not conservative, you gener= ally can't draw mathematical conclusions on the basis of those computat= ions, though.

On Saturday, February 9, 2019 at 6:57:51 AM UTC-5, Fel= ix Rech wrote:
On Friday, 8 February 2019 22:19:24 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 intereste= d in constructive mathematics (like I am) then they are useful.
=

I agree that the ability to compute canoni= cal forms for terms is essential but one does not need to integrate computa= tion into the type system to do that. At least, one can alway interprete te= rms of a type theory without an equality judgment in a stronger type theory= that has judgmental equalities and do the computations there.
<= /blockquote>

--
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_1049_1978017938.1549868291151-- ------=_Part_1048_801624903.1549868291151--