From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.46.14.17 with SMTP id 17mr4047751ljo.4.1491558249734; Fri, 07 Apr 2017 02:44:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.31.203 with SMTP id f194ls101729wmf.19.canary-gmail; Fri, 07 Apr 2017 02:44:08 -0700 (PDT) X-Received: by 10.28.34.6 with SMTP id i6mr942301wmi.7.1491558248612; Fri, 07 Apr 2017 02:44:08 -0700 (PDT) Return-Path: Received: from sun61.bham.ac.uk (sun61.bham.ac.uk. [147.188.128.150]) by gmr-mx.google.com with ESMTPS id k74si215014wmd.1.2017.04.07.02.44.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 07 Apr 2017 02:44:08 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) client-ip=147.188.128.150; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.150 as permitted sender) smtp.mailfrom=escardo...@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from [147.188.128.127] (helo=bham.ac.uk) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cwQR6-0004zZ-N7; Fri, 07 Apr 2017 10:44:08 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1cwQR6-0003E0-DK using interface smart1.bham.ac.uk; Fri, 07 Apr 2017 10:44:08 +0100 Received: from dynamic200-118.cs.bham.ac.uk ([147.188.200.118]) by mx1.cs.bham.ac.uk with esmtp (Exim 4.51) id 1cwQR6-0008U2-2L; Fri, 07 Apr 2017 10:44:08 +0100 Subject: Re: [HoTT] Conjecture To: Thomas Streicher , Jon Sterling 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> <20170406115247.GC25210@mathematik.tu-darmstadt.de> From: Martin Escardo Cc: HomotopyT...@googlegroups.com Message-ID: <4c10260c-cde9-a1e9-8ed1-f8b19610e059@googlemail.com> Date: Fri, 7 Apr 2017 10:49:57 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: <20170406115247.GC25210@mathematik.tu-darmstadt.de> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes Dear Thomas, Sorry it took so long to answer, but I needed to find time to be able to write my reaction to your remarks. (1) Indeed, I do like to think of the fragment of univalent type theory consisting of function extensionality + proposition extensionality + propositional truncation as essentially the same thing as topos logic, provided we have propositional resizing. (But, as discussed, much can be done without propositional resizing (but not all), and one way of looking at HIT's is as a mechanism to avoid resizing.) This is good: this fragment leaves us in familiar territory. (2) I don't see univalent type theory as simply the extension of type theory with univalence (and hence function and proposition extensionality). Before we extend dependent type theory with any axiom, we can start to think "univalently". In particular, the notions of h-level, proposition, contractibility, equivalence, the distinction of existence as proposition or structure, so as to be able to define e.g. embeddings, surjections, and many others correctly, can be formulated and understood before we bring univalence. In this way "univalent type theory" is a different way to understand good old type theory. Of course, with univalence we get more, and what you are saying, and I don't disagree fundamentally, is that this "more" are types of higher h-level and theorems and constructions with them (such as the type of categories, if we want to avoid homotopy in the discussion). Although we don't use univalence in our paper, we formulate our notions in the light of this new, alternative understanding of type theory. One example, already mentioned in the above answer to Jon, is something that kept Cory and I working for an afternoon, but perhaps is not adequately emphasized in the paper. In topos logic, you define (for the dominance of all propositions) Lift(X) = { A:X->Omega | (exists(x:X), A x) & forall(x,y:X), A x -> A y -> x = y } If we want, in univalent type theory, this to work for types of higher h-levels, how should we define this? The above definition works well and can be kept as it is if X is a set. To generalize it to types of higher levels, we need two modifications: (i) Change Omega to the universe U. (ii) Reformulate the condition on A as isProp(Sigma(x:X), A x). When X is a set, the reformulation (i)-(ii) makes no difference. However, in the general case, it is (i) and (ii) that give the right definition. For instance, with the right definition, we always get an embedding X->Lift X, whereas if we had taken the original topos-theoretic version of Lift, then Lift S^1 would be a singleton and hence wouldn't embed S^1. We would get the wrong notion of partial function. Thus, although we haven't used univalence, we took care of formulating the notions so that they are not restricted to the realm of sets, and in this sense what we are doing can be considered as univalent type theory. (3) We should have cited Andrej's and Bernhard's references below, and we will (and many other things, to reflect the amount of work done about this in the context of topos theory). Of course we are aware of them, but thanks for mentioning them in this list! (4) A last point is that, as opposed to most of the work in the topos literature for dominances in realizability toposes as in (3), we deliberately don't use Markov's principle or countable choice in our internal development of computability in univalent type theory (Section 3 of the paper). Moreover, we are *not* looking at synthetic computability. We are looking at plain computability. Best, Martin On 06/04/17 12:52, Thomas Streicher wrote: >> 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 — a logical approach. (English summary) > Math. Structures Comput. Sci. 9 (1999), no. 2, 177–223. > > 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 > -- Martin Escardo http://www.cs.bham.ac.uk/~mhe