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 7e0adc1e for ; Sat, 9 Feb 2019 11:57:53 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id m52sf5761611otc.13 for ; Sat, 09 Feb 2019 03:57:53 -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=A9qzVjdvAW545Tkg5CNx2noFoLTH7b2NcnkAbDX5PUE=; b=YtI7MSjcQzgDEo5CrbBxMtX0y1l5SzrlVa7q61Cz2TipFA+1LXuB6xJM22X+HUEoCL MDwgvcau1GRmdxoX0yOhMv3o1dr3o9I42fodyunvKnyMwg+kXNKPbpfuYp8bQ1MPl1az ECD7xQ78kkEoPfcoKCg4Zuuid3zhMFpXgyfvMKAGnxymC4qJ32PtR85JKBf2lqvqWI8g 5M3LEmxt3MftIvqS2Pg8KR31oUXtGjaE4oodFv5lB6Oj53g5RJQNkKLC7rat1dczP4tV gkySbwe5tdv648Npl+c+VDasjHvJXgPNBcEpbik1jdmT+Ft7ErAD+nL/FzOK08jORpO0 +iog== 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=A9qzVjdvAW545Tkg5CNx2noFoLTH7b2NcnkAbDX5PUE=; b=EETrD0WHyQYEnS6TUILctYkr0x7Mjbp6IiSONtascCaPOnD6ZhMb4hT9JYs32r/6Lp OSpE7hZKWIj4HvomVEk0EI3TArRKmYwO5GBxAAFKW06wn7f5WmR5b/rU7z3cWCq+4zHA O1Hf1bj8C2y4etkg87usa9E/cP6KgZeoNNAAgA52xl4VREiwc6MpwiYFNdnuf3ID3h+E ueO3L5qoQ66Yp/SGt60Qe99+qVZC/nQ78WZRSCQB6vsZgJCaZqCUBE45fRysh9vNvhpk P8SwR/yJsY5xc9yUGfbFhj+R+K5GYiKj1Q9FhERIB7O2lGvQCNDoseC/GudImkXRbWT4 fcYQ== 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=A9qzVjdvAW545Tkg5CNx2noFoLTH7b2NcnkAbDX5PUE=; b=meinqF8jp+40ipuTWsSL1rL0QDu+ywonDmV8eN1MGzWT3jyCi6bGH3K55qt/TnjP2H 4+HoWzVDSni36FCoISSyWq7rmfpKwVn552pQfSMLejl9YVQvHdyS1Dl9FftfbNWN0uGt 1uPhLNLzRbgkd6RmyYw1Tc16SVsTFDr2Sv5ariz+5Y1zgu9mOcKevkGsEpNg8wYLdpDB 5+OsjNKF8L06vnBbYtUW3+Yxhjj7K0/RVvXnBSOpeCNhVxGIPtBXF0cQ1MoLF+ubuaWv l1gfzp0dOPeKS4/bKFBORmDWzUoVg7bv56fLQWSByXYRtd3dF9c0YJpaP8502oD1rPDQ V73A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAubSZ/avsJKjAPGB637lU0tCJlyqyMnwh6Lqdz8UrGSgyUULzlH+ 71tEiGVPQZsgIWx2Q7cQiMI= X-Google-Smtp-Source: AHgI3IYFp9wlN0sBlbePNxOzKz5rvEWo+wvL1LgfsQJZPj2opRRR2GJ18RIBvUOYhemynJkUqbZBuQ== X-Received: by 2002:a54:4d86:: with SMTP id y6mr21613oix.0.1549713472442; Sat, 09 Feb 2019 03:57:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3183:: with SMTP id x125ls3271016oix.1.gmail; Sat, 09 Feb 2019 03:57:52 -0800 (PST) X-Received: by 2002:aca:df55:: with SMTP id w82mr23765oig.6.1549713471899; Sat, 09 Feb 2019 03:57:51 -0800 (PST) Date: Sat, 9 Feb 2019 03:57:51 -0800 (PST) From: Felix Rech To: Homotopy Type Theory Message-Id: <971e73a5-da33-4793-bf18-63e15bc80c28@googlegroups.com> In-Reply-To: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_655_1978312062.1549713471333" X-Original-Sender: s9ferech@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_655_1978312062.1549713471333 Content-Type: multipart/alternative; boundary="----=_Part_656_100734855.1549713471333" ------=_Part_656_100734855.1549713471333 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 essential= =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 an= =20 equality judgment in a stronger type theory that has judgmental equalities= =20 and do the computations there.=20 --=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_656_100734855.1549713471333 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 s= o if you are interested in constructive mathematics (like I am) then they a= re useful.

I agree that the abi= lity to compute canonical forms for terms is essential but one does not nee= d to integrate computation into the type system to do that. At least, one c= an alway interprete terms of a type theory without an equality judgment in = a stronger type theory that has judgmental equalities and do the computatio= ns there.=C2=A0

--
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_656_100734855.1549713471333-- ------=_Part_655_1978312062.1549713471333--