From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:e791:: with SMTP id n17mr7900076wrm.217.1589012913240; Sat, 09 May 2020 01:28:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:4088:: with SMTP id n130ls23310335wma.2.canary-gmail; Sat, 09 May 2020 01:28:32 -0700 (PDT) X-Received: by 2002:a7b:cc0f:: with SMTP id f15mr21415144wmh.78.1589012912155; Sat, 09 May 2020 01:28:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589012912; cv=none; d=google.com; s=arc-20160816; b=0YIDuJtz7sgKponsUQqVMDT5OZJ6KC1nKALE0JlnZ9MlrfGYTCXRy0ODun8QP1SgmH +wd9FiWPXJt0gXtgxduIDA8r3nW3f4HVaLeUnEbqjRtK1h2fI/C6TDFjQ1SHGbqkT2Tw BpcDtwTET/nYoLXaKRkraceAmb1WZydRv3ZJm4AMDKhXowqDVGkSbcLwjaRygAFkfBod 9NWdDi4+9X+gxkqZFw3JKytOWEkyd9Laae1QdPXlBzceOFwjxouEQ8K9JmNRo2r3+3H/ O0s4/Jj6MsPQyOIFMwdMFTngL+a0EwZJJxbHM/RB1U3VAUa+bVTmuD00uBy9GSo1ZK57 C5Hg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=+16jy/x1AcHvYX+CTXhTkFQKA+s/Ev8G/MLoafcujUk=; b=nzrVGOVarzR5l75jO4oHTAN0fwonFaXPTqsonm/5+LyrYf+z7OYYGX00iEC1bKroAT 1HVdJAyylQBK8zcQ+GgGVwhQeqs43tblCdd3dn2rNVRXqnqYso8qROVWhYBtFiNThp/c MpilvuLBCAFilgKBmXk13dH3COe8r92Si65sqaCNhDcXMbjTfCqgYNPP/I6SNF7SwLfZ xmq8BmgHA9hwDxckIcjyeU5MZBLiaCHM5oPKfGKeQjwmXoyVfrepujdh3S3UFg0u10Pz Itt9BkV/sCniQifQenJuyZ9k2JdEDSiBgTmf2r0FaoYiJ75FMgLAv+vOGe9rY7nThEI+ cE5g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay232.hrz.tu-darmstadt.de (mail-relay233.hrz.tu-darmstadt.de. [130.83.156.233]) by gmr-mx.google.com with ESMTPS id y12si98029wmd.1.2020.05.09.01.28.32 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 May 2020 01:28:32 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) client-ip=130.83.156.233; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.233 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client CN "mail.mathematik.tu-darmstadt.de", Issuer "DFN-Verein Global Issuing CA" (verified OK)) by mail-relay232.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49K0hZ2Fz1z43hJ; Sat, 9 May 2020 10:28:29 +0200 (CEST) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id 0498TBPX010622; Sat, 9 May 2020 10:29:11 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 1B48FC0061; Sat, 9 May 2020 10:28:29 +0200 (CEST) Date: Sat, 9 May 2020 10:28:29 +0200 From: Thomas Streicher To: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= Cc: David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: Re: [HoTT] Identity versus equality Message-ID: <20200509082829.GA8417@mathematik.tu-darmstadt.de> References: <952EF822-FD92-404C-A279-89502238BCDC@nottingham.ac.uk> <8C57894C7413F04A98DDF5629FEC90B1652F526C@Pli.gst.uqam.ca> <67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9@nottingham.ac.uk> <20200507100930.GA9390@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F5334@Pli.gst.uqam.ca> <8C57894C7413F04A98DDF5629FEC90B1652F53A3@Pli.gst.uqam.ca> <20200508064039.GC21473@mathematik.tu-darmstadt.de> <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F54CC@Pli.gst.uqam.ca> User-Agent: Mutt/1.5.23 (2014-03-12) Dear Andr'e, in most models of HoTT judgemental equality is equality of morphisms and propositional equality is being homotopic. But that is very different from its appearance in formal systems where judgemental equality is much more restricted and just serves the purpose of computation. There are artificial versions of type theory with excessively few computation rules (only mere lambda calculus). I fully understand why you find judgemental equality puzzling: it is of very subjective nature. Mathematicians are typically interested in equalities which are not decided by a rewrite system. Judgemental equality has a very subjective nature because it identifies a computational fragment of mathematics and there are many different such. In Book HoTT one is as computational as traditional intensional TT is and then adds univalence which lacks any computational meaning. This is at least frivolous from the perspective of a traditionalist type theorist... But it is ok and was implemented in the NuPrl system. Now for people who use type theory as a way of doing homotopy theory synthetically the computational aspect is absolutely irrelevant a priori. When one does ordinary math (including homotopy) computability is a gimmick and no one would insist on everything being computable. So if one has shown that the homotopy group of some pointed space is Z_n for some n and one wants to know what n is then in Book HoTT you have to guess n and then show that n equal your guess. In cubical type theory in principle the n can be computed but it may take a very long time (or the normalization proof is faulty :-)). The main problem is that programs extracted from proofs are typically not very efficient (well in rare cases they are but you have to be lucky). Anyway, my brief answer to the question you raise is: (1) conceptually judgemental equality is absolutely redundant and hopelessly subjective (2) systems with a bare minimum of judgemental equality are not suitable for the various proof checkers in use since then every computation has to be done by hand. Thomas