From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 2002:adf:ed86:: with SMTP id c6mr10158142wro.124.1589049798439; Sat, 09 May 2020 11:43:18 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:1bc2:: with SMTP id b185ls24012413wmb.3.canary-gmail; Sat, 09 May 2020 11:43:17 -0700 (PDT) X-Received: by 2002:a7b:c5d3:: with SMTP id n19mr15291067wmk.21.1589049797222; Sat, 09 May 2020 11:43:17 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1589049797; cv=none; d=google.com; s=arc-20160816; b=rUIAtUwujpE9DV0bJ6lxTxQDQV5RWKFZAIbzOuDemSwvPu0btk1A8AIUznfZ0kR/r8 6xr93687ZlOHcPRSDVhlzmT+d7G2P92W5lf7ZppJGBsXLa4F7xuBVzybxnPcDUeq3WYG 2wCj0zRJFu0c3aH5S00hCm8EiqjQ7Kx0yI5S9S4sJOnfybPNxYDTV3BEsKFcwkWAdRqU Z0dwxMqUv67RAHLYGZfAB7Udzx8QAgWhiDu37LLBJBk6w4/d2vneCcQBXnZhhYn9O5Fp RhodaADyBTHZASIJTOpr8mfFrJY9IyAarea+XbSdW4j5YpZ/qcUFiLaDnOc505L2kjUp 11sw== 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=4r51gmj7o1dPRiqXKVXgSfZs4EWj0i3UxC0a3+Y6ypw=; b=0C5eqQym+OzzoeELbGpcxE9bPZBpj9IivG0IdGv9o4EtU6ScAXLa3DBeVnAMlmYW7S ty9UYqyFngK9KP6/M+tF88CGYeRbEWwzNWOa83u6fQHhh9TMSAp+wYh6ukXuVcGW63/1 tbgx7QBcIaUDKo8CMZAEwqCGiXBGJGJJt6m7NRps2fFLGHS7bXYgU1f4mCHDYmVIUOWt SG2b8YxGUkTW1fg0SNWH0UXmqlfZxog6CqsK6yGPim0Fiu4bbN2bvDr6ncV5iifnA3q+ j6xrd8fEDDPpbe9UmTYS3B0P51QlnHxjwarEIjT0JmYiVAXmsCYsxiR3NS1er5iQoKgS axSA== 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.230 as permitted sender) smtp.mailfrom=stre...@mathematik.tu-darmstadt.de Return-Path: Received: from mail-relay230.hrz.tu-darmstadt.de (mail-relay230.hrz.tu-darmstadt.de. [130.83.156.230]) by gmr-mx.google.com with ESMTPS id a2si352342wrv.4.2020.05.09.11.43.17 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 May 2020 11:43:17 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.230 as permitted sender) client-ip=130.83.156.230; 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.230 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-relay230.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 49KGKv15Ryz43W5; Sat, 9 May 2020 20:43:14 +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 049Ihu0U017694; Sat, 9 May 2020 20:43:56 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id C0320C2878; Sat, 9 May 2020 20:43:13 +0200 (CEST) Date: Sat, 9 May 2020 20:43:13 +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: <20200509184313.GB28841@mathematik.tu-darmstadt.de> References: <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> <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F55C8@Pli.gst.uqam.ca> User-Agent: Mutt/1.5.23 (2014-03-12) Dear Andr'e, > By the way, if type theory is not very effective in practice, why do we insist that it should always compute? > The dream of a formal system in which every proof leads to an actual computation may be far off. > Not that we should abandon it, new discoveries are always possible. > Is there a version of type theory for proving and verifying, less > for computing? In my opinion the currenrly implemented type theories are essentially for proving and not for computing. But if you haven't mechanized PART of equational reasoning it would be much much more painful than it still is. But that is "only" a pragmatic issue. > The notations of type theory are very useful in homotopy theory. > But the absence of simplicial types is a serious obstacle to applications. In cubical type theory they sort of live well with cubes not being fibrant... They have them as pretypes. But maybe I misunderstand... Thomas