From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.53.2 with SMTP id a2mr11582475qte.16.1491438220942; Wed, 05 Apr 2017 17:23:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.2.76 with SMTP id 73ls1562091itu.13.gmail; Wed, 05 Apr 2017 17:23:40 -0700 (PDT) X-Received: by 10.99.170.73 with SMTP id x9mr12663151pgo.1.1491438220003; Wed, 05 Apr 2017 17:23:40 -0700 (PDT) Return-Path: Received: from out1-smtp.messagingengine.com (out1-smtp.messagingengine.com. [66.111.4.25]) by gmr-mx.google.com with ESMTPS id h35si3117474ywk.0.2017.04.05.17.23.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 05 Apr 2017 17:23:39 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.25; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com; spf=neutral (google.com: 66.111.4.25 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 8DBBA20A96 for ; Wed, 5 Apr 2017 20:23:39 -0400 (EDT) Received: from web2 ([10.202.2.212]) by compute2.internal (MEProxy); Wed, 05 Apr 2017 20:23:39 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-me-sender:x-me-sender:x-sasl-enc; s=fm1; bh=spJQLE kc39GiVk2bpaZ9tyqPmtFoFaSbKJJW/SjAE8A=; b=A4x7zDFNRbDy394q+5unjS orIjo+wQTNxpSIzbxwOzVjq0XmbCYauaUG1JzrIz4AKYQdcVRpZ1dboZBt3H6EiN GdzCA36A6LeB2QtWOFmf0Exj+SYHaSrD9Qp5mduvxKHMxZCb09xL09rqRLwjixqG nZho1EYxPKATbmXK2lGo41baUB/Wee4jX6RJtQPEYXvvv+IL4B+LDLxePWR4loNF FHr49wUeFqaVhlm+yl5NUWCqCjOgpivIkjNiP3FGNlEaFYeJFWdj5LsCwhEarl4f zLmMqAivJ2ihld4fkCA7CofeoyWOyIx445cVu0aTqDVcbFyXWuu+H/abWCB0l/fg == X-ME-Sender: Received: by mailuser.nyi.internal (Postfix, from userid 99) id 612DE62737; Wed, 5 Apr 2017 20:23:39 -0400 (EDT) Message-Id: <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-8e6aa83c Subject: Re: [HoTT] Conjecture In-Reply-To: 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> Date: Wed, 05 Apr 2017 17:23:39 -0700 Martin, 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. Best, Jon On Wed, Apr 5, 2017, at 12:37 PM, 'Martin Escardo' via Homotopy Type Theory wrote: > > > On 31/03/17 17:09, 'Martin Escardo' via Homotopy Type Theory wrote: > > > > > > On 30/03/17 23:49, Nicolai Kraus wrote: > >> Interesting construction by Cory and you! And I think I can help > >> you with the factorisation that you asked for, as follows: > > > > Thanks for this, Nicolai. > > > > Cory and I a battling against the clock to get our submission ready for > > a conference. I'll continue the discussion after that. > > I may as well give a link to the paper now that we have finished and > submitted it, which is about partial functions in univalent type theory: > http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf > > The conjecture in the initial message of this thread goes well beyond > this, and is even unrelated. But I am still very interested in the > conjecture independently of any use of it. > > Martin > > -- > 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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.