From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.210.6 with SMTP id z6mr129017itf.24.1491585130562; Fri, 07 Apr 2017 10:12:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.108.208 with SMTP id w199ls384859itb.10.gmail; Fri, 07 Apr 2017 10:12:09 -0700 (PDT) X-Received: by 10.107.9.90 with SMTP id j87mr15188510ioi.86.1491585129724; Fri, 07 Apr 2017 10:12:09 -0700 (PDT) Return-Path: Received: from mail-yb0-x230.google.com (mail-yb0-x230.google.com. [2607:f8b0:4002:c09::230]) by gmr-mx.google.com with ESMTPS id f9si888444ywh.6.2017.04.07.10.12.09 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 07 Apr 2017 10:12:09 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com; spf=neutral (google.com: 2607:f8b0:4002:c09::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x230.google.com with SMTP id m133so18516203ybb.1 for ; Fri, 07 Apr 2017 10:12:09 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=Cba0W1y2wtXaeE0WytCVuzUxnSfiWukFSrk3riOSKSk=; b=rZpaOibfQMHZkcWTjZau+JsrzDYbN2X3X3l43zE4iMjVc2ZO7t9Q4Zak4JGEeyegPr nx0ehcj1imRjwAASxmpWfQHg7RsClnHSAw47tLeH3panjUvbAjJIvhQAK+xbO0ms4NSW 3LVbzKPkqqZJDrt2sk1e2XFhXlcjusT0B1lyFanF3GRa+Prt5PiPDrDUOvXtj8exC1qt UiE3kjrTr53TZVTzauC6l5+3cHBrCfGLCzElBbyaEqjpbF9cYPtZFEJvNXtdaNaun1a0 VXtjo0QdonZvKbA6/3S/JlPLI5Q7x/6fD5mzClUrfu1vPonHkVRM3X585D6kslV4Oh5o mKGg== X-Gm-Message-State: AFeK/H1GSDSraruMp2xMbSSt81teI6csXjPU2S2Ff8Oue9gZ1A6U/i+XBBOvDusL8bzqljUY X-Received: by 10.37.55.74 with SMTP id e71mr16340248yba.164.1491585128893; Fri, 07 Apr 2017 10:12:08 -0700 (PDT) Return-Path: Received: from mail-yw0-f180.google.com (mail-yw0-f180.google.com. [209.85.161.180]) by smtp.gmail.com with ESMTPSA id j10sm2224187ywa.21.2017.04.07.10.12.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 07 Apr 2017 10:12:08 -0700 (PDT) Received: by mail-yw0-f180.google.com with SMTP id p77so37350586ywg.1 for ; Fri, 07 Apr 2017 10:12:07 -0700 (PDT) X-Received: by 10.129.121.1 with SMTP id u1mr2048456ywc.296.1491585127350; Fri, 07 Apr 2017 10:12:07 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.36.138 with HTTP; Fri, 7 Apr 2017 10:11:46 -0700 (PDT) In-Reply-To: <4c10260c-cde9-a1e9-8ed1-f8b19610e059@googlemail.com> 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> <4c10260c-cde9-a1e9-8ed1-f8b19610e059@googlemail.com> From: Michael Shulman Date: Fri, 7 Apr 2017 10:11:46 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Conjecture To: Martin Escardo Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Fri, Apr 7, 2017 at 2:49 AM, 'Martin Escardo' via Homotopy Type Theory wrote: > (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.) I would say that to really be talking about (elementary) topos logic, one should also do without universes other than hProp. Of course, elementary 1-toposes also validate UIP. If we also omit hProp and propositional resizing, but include nonrecursive HITs as well as ordinary inductive types, then it ought to be basically Pi-W-pretopos logic; right? > 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) =3D { A:X->Omega | (exists(x:X), A x) & > forall(x,y:X), A x -> A y -> x =3D 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 =E2=80=94 a logical approach. (English s= ummary) >> Math. Structures Comput. Sci. 9 (1999), no. 2, 177=E2=80=93223. >> >> 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 > > -- > 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.