From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.22.16 with SMTP id w16mr3510538ljd.18.1491479571116; Thu, 06 Apr 2017 04:52:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.215.94 with SMTP id o91ls2748924lfg.16.gmail; Thu, 06 Apr 2017 04:52:49 -0700 (PDT) X-Received: by 10.25.153.74 with SMTP id b71mr4532936lfe.23.1491479569874; Thu, 06 Apr 2017 04:52:49 -0700 (PDT) Return-Path: Received: from lnx503.hrz.tu-darmstadt.de (mail-relay15.hrz.tu-darmstadt.de. [130.83.156.239]) by gmr-mx.google.com with ESMTPS id a126si35538wmd.2.2017.04.06.04.52.49 for (version=TLS1 cipher=AES128-SHA bits=128/128); Thu, 06 Apr 2017 04:52:49 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of stre...@mathematik.tu-darmstadt.de designates 130.83.156.239 as permitted sender) client-ip=130.83.156.239; 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.239 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]) by lnx503.hrz.tu-darmstadt.de (8.14.4/8.14.4/HRZ/PMX) with ESMTP id v36Bqm3Z028788; Thu, 6 Apr 2017 13:52:48 +0200 (envelope-from stre...@mathematik.tu-darmstadt.de) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.12.3/8.12.3/Debian-7.2) with ESMTP id v36BqmES024625; Thu, 6 Apr 2017 13:52:48 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 2FD291A0BBE; Thu, 6 Apr 2017 13:52:48 +0200 (CEST) Date: Thu, 6 Apr 2017 13:52:48 +0200 From: Thomas Streicher To: Jon Sterling Cc: HomotopyT...@googlegroups.com Subject: Re: [HoTT] Conjecture Message-ID: <20170406115247.GC25210@mathematik.tu-darmstadt.de> References: <1cd04354-59ba-40b4-47ce-9eef3ca3112f@googlemail.com> <2445fdca-d1bb-08c8-6061-e4a7e0faffa7@gmail.com> <98e87128-34a8-63a6-a055-8402498ef8b2@googlemail.com> <6767f0e2-a1e3-9d27-602c-8b81d8579893@googlemail.com> <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> User-Agent: Mutt/1.5.23 (2014-03-12) X-PMX-TU: seen v1.2 by 5.6.1.2065439, Antispam-Engine: 2.7.2.376379, Antispam-Data: 2017.4.6.114817 X-PMX-RELAY: outgoing > This looks like a very interesting paper, thank you for sharing. I look > forward to reading it in more detail. > > I am curious, does this development use univalence except to establish > functional extensionality and propositional extensionality? The reason I > ask is, I wonder if it is possible to do a similar development of > computability theory in extensional type theory and get analogous > results. Additionally, I am curious whether you have found cases in > which univalence clarifies or sharpens this development, since I'm > trying to keep track of interesting use-cases of univalence. For synthetic domain theory a formulation in extensional type theory has been given in MR1694130 (2000f:68069) Reus, Bernhard; Streicher, Thomas General synthetic domain theory ¡X a logical approach. (English summary) Math. Structures Comput. Sci. 9 (1999), no. 2, 177¡V223. There is no need whatsoever to use univalence or something like that. The only benefit would be to solve domain equations up to equality which even computer scientists find unnecessary (for good reasons). Andrej Bauer has written on Synthetic Recursion Theory, see math.andrej.com/data/synthetic.pdf. So I tend to the opinion that theer can't be an intrinsic use of Univalence or HITs. But if there is I am curious to learn which one! Thomas