From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.28.105.80 with SMTP id e77mr1113740wmc.23.1491458116960; Wed, 05 Apr 2017 22:55:16 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.25.145.80 with SMTP id y16ls2556635lfj.10.gmail; Wed, 05 Apr 2017 22:55:16 -0700 (PDT) X-Received: by 10.25.77.149 with SMTP id a143mr4309329lfb.26.1491458115993; Wed, 05 Apr 2017 22:55:15 -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 a126si493882wmd.2.2017.04.05.22.55.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 05 Apr 2017 22:55:15 -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.54] (helo=mailer3) by sun61.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cw0O3-0002PY-Ni; Thu, 06 Apr 2017 06:55:15 +0100 Received: from 128.172.125.91.dyn.plus.net ([91.125.172.128] helo=[192.168.1.93]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:DHE-RSA-AES128-SHA:128) (Exim 4.84) id 1cw0O3-0008WM-DZ using interface auth-smtp.bham.ac.uk; Thu, 06 Apr 2017 06:55:15 +0100 Subject: Re: [HoTT] Conjecture To: Jon Sterling , HomotopyT...@googlegroups.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> From: Martin Escardo Message-ID: <28122de4-b334-8c92-5281-81da31ecb50b@googlemail.com> Date: Thu, 6 Apr 2017 06:55:14 +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: <1491438219.730556.935704416.05FD6770@webmail.messagingengine.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:DHE-RSA-AES128-SHA:128 via 147.188.128.21:465 (escardom) On 06/04/17 01:23, Jon Sterling wrote: > 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. Currently the only place that uses univalence is the equivalence of (X->Y) with the type of single-valued relations X->Y->U. (This was proved by Egbert in his mater thesis.) But another point, compared with previous developments in topos logic an extensional type theory, is that a number of things work as they should for types more general than sets by replacing subobject-classifier-valued functions by universe-valued functions. An example is this: Consider the lifing in its representation with subsingletons L(X) = (Sigma(A:X->U), isProp(Sigma(x:X), A(x))). If we replaced U by Prop in this definition, this wouldn't work well for types that are not sets. For example, if X is the circle, any function into a set, and hence any function into Prop, is constant, and so L(X) would be contractible. However, with the definition as it is, with U, we always have that X is embedded into L(X), even if X is not a set. The same phenomenon applies to the equivalence of (X->Y) with the type of single-valued relations X->Y->U discussed above, but this additionally requires univalence. Martin