From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:a05:6830:22f8:: with SMTP id t24mr6274090otc.148.1589039635826; Sat, 09 May 2020 08:53:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:1b0d:: with SMTP id l13ls1122006otl.5.gmail; Sat, 09 May 2020 08:53:54 -0700 (PDT) X-Received: by 2002:a05:6830:90:: with SMTP id a16mr6645215oto.282.1589039634473; Sat, 09 May 2020 08:53:54 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589039634; cv=none; d=google.com; s=arc-20160816; b=yRkSs/uObYxMS/Zjuu5LIzlDDn4g9XR47mm6tybgte2JKY11R7YY0bi+OttyIOTEJM DcUCt8D9k+l0AkUFTampjNRuswCuUSSPFDPXVuLSh9Y/uV5g19ERRkpbtSw3g8xVoylP TO8Oe3Ln+IFDhLH4iYUFOi1SOvxLK831g/O3SlnHy3fABlaJGwZxlVd+xR+nnHG4i/pM VzsvN+zcVNiwMDOI7FB3uTGgTAaCibluuiY7F8LKGP1PFgm/qYDc1rybRuxw3KkAm8w7 V3VBVP7BS2i+wiqiPR2jFm4euVP/35+tL50iCiM9EJI7SgTWfAQg2JFkpT4ekZf49G8d v+sQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-sdr; bh=nUhO/N++kvZALGDSSDW2F16vDKebNLJptB1E7FZwJEQ=; b=NEESPCH2hHANSTwaPWbBYtO+YRyVpwp/s8I+y/yUScLPJN0nUxRwFE2bjUea8nS4me eXKPg9HCu02cmsOOD7bQUrScTclmGlomwPSbK0F4tISXDje/XStA82YODibUDE11jA9I u2onR2xmJqecmeKucDIl+rJBAUTOHVI6D6KmCRrUEQ0vcALf47gQ3NPajLJPwI5NVGi4 ndxYlLDDwQlf7hvwWpESeL+2LNC6nvQu1Jsq/EkuzSWJVIUND6v2HUQYXZUVSjqZ0ufW SyXe39wSQdUi2yTrVhtrHFX+/7l0jcnxw29tKDJIA1MEGX5mhp7y89dIbDcm70d9PPBN anFw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca Return-Path: Received: from mail6.uqam.ca (mail6.uqam.ca. [132.208.246.231]) by gmr-mx.google.com with ESMTP id f139si1199088oig.5.2020.05.09.08.53.54 for ; Sat, 09 May 2020 08:53:54 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) client-ip=132.208.246.231; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal...@uqam.ca designates 132.208.246.231 as permitted sender) smtp.mailfrom=joyal...@uqam.ca IronPort-SDR: mlFKbCLrXZVu2xNpguWcQCdmLenQE2s3B78CeW3WE3CM36++DajHxtFHxYYOK17c1UCco5lFnT jwRttEPNGjlVoeujqUzT2t3bxpdZYdwD+nwPnNZfzrNoLG/GEZAfmbn/mf9G3mQB4HcaYELAid CO3EPUtlZ0zsDkzE00z7z9n609wqDN9PXLlAAePFQ+vTYbrEHCimVNDxuZ4Ozh2TQxKhZMrZA7 q9PWUH8Rgr8BiLyMpqvmZBQUH+/H39btcW07TjjefHHqPtQKs7sw772O8sdRlrYeOd5Dne+OPP 8W0= X-IronPort-AV: E=Sophos;i="5.73,372,1583211600"; d="scan'208";a="10573135" Received: from unknown (HELO Message.gst.uqam.ca) ([132.208.216.70]) by mail6.uqam.ca with ESMTP; 09 May 2020 11:53:54 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.153]) by Message.gst.uqam.ca ([169.254.1.218]) with mapi id 14.03.0439.000; Sat, 9 May 2020 11:53:53 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Thomas Streicher CC: David Roberts , Thorsten Altenkirch , Michael Shulman , Steve Awodey , "homotopyt...@googlegroups.com" Subject: RE: [HoTT] Identity versus equality Thread-Topic: [HoTT] Identity versus equality Thread-Index: AQHWIrnt2rpL+UtjL0e4oihqoDCB+qibJxGOgACIG4CAAAS1AIAAPFAA//+/ZaSAAMfxgIAANUUAgAAO4LWAALJlgP//xKOFgABhQICAAHDSgIAAmhfJgAEWX4CAAC1BFA== Date: Sat, 9 May 2020 15:53:52 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> 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>,<20200509082829.GA8417@mathematik.tu-darmstadt.de> In-Reply-To: <20200509082829.GA8417@mathematik.tu-darmstadt.de> Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Thank you Thomas, Jon and Steve for answering my question. You are very generous to an old man. Let me pretend that I still have enough time to study the computational asp= ects of type theory. By the way, if type theory is not very effective in practice, why do we ins= ist that it should always compute?=20 The dream of a formal system in which every proof leads to an actual comput= ation may be far off. Not that we should abandon it, new discoveries are always possible. =20 Is there a version of type theory for proving and verifying, less for compu= ting? The notations of type theory are very useful in homotopy theory. But the absence of simplicial types is a serious obstacle to applications. Best, Andr=E9 ________________________________________ From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de] Sent: Saturday, May 09, 2020 4:28 AM To: Joyal, Andr=E9 Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homo= topyt...@googlegroups.com Subject: Re: [HoTT] Identity versus equality 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