From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.25.199.66 with SMTP id x63mr4621561lff.4.1491494628447; Thu, 06 Apr 2017 09:03:48 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.28.28.10 with SMTP id c10ls2687313wmc.9.gmail; Thu, 06 Apr 2017 09:03:47 -0700 (PDT) X-Received: by 10.223.164.151 with SMTP id g23mr922027wrb.17.1491494627592; Thu, 06 Apr 2017 09:03:47 -0700 (PDT) Return-Path: Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id p144si89641wme.2.2017.04.06.09.03.47 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 06 Apr 2017 09:03:47 -0700 (PDT) Received-SPF: softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo...@googlemail.com does not designate 147.188.128.137 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 sun60.bham.ac.uk with esmtp (Exim 4.84) (envelope-from ) id 1cw9sx-0001OQ-Ne; Thu, 06 Apr 2017 17:03:47 +0100 Received: from mx1.cs.bham.ac.uk ([147.188.192.53]) by bham.ac.uk (envelope-from ) with esmtp (Exim 4.84) id 1cw9sx-0006gN-Dq using interface smart1.bham.ac.uk; Thu, 06 Apr 2017 17:03:47 +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 1cw9sx-0004BS-72; Thu, 06 Apr 2017 17:03:47 +0100 Subject: Re: [HoTT] Conjecture To: Martin Escardo 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> <28122de4-b334-8c92-5281-81da31ecb50b@googlemail.com> <9A3B1ACD-63F0-4115-BEDB-EF1B0ECD25D2@ias.edu> <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk> Cc: HomotopyT...@googlegroups.com From: Martin Escardo Message-ID: <7f1d3c6e-2084-7388-0de3-b353b4e895c8@googlemail.com> Date: Thu, 6 Apr 2017 17:09:32 +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: <81c0782f-9287-4111-a4f1-01cb9c87c7e8@cs.bham.ac.uk> Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-BHAM-SendViaRouter: yes Another remark about size is that if the propositions in your dominance are in the first universe, then all universes except the first one are closed under lifting, and hence we way as well just work from the second universe onwards as an alternative to resizing. Martin On 06/04/17 17:08, Martin Escardo wrote: > Another remark about size is that if the propositions in your dominance > are in the first universe, then all universes except the first one are > closed under lifting, and hence we way as well just work from the second > universe onwards as an alternative to resizing. Martin > > On 06/04/17 14:50, 'Martin Escardo' via Homotopy Type Theory wrote: >> >> >> On 06/04/17 13:40, Vladimir Voevodsky wrote: >>> I looks like like you would also need the resizing rule to place >>> hProp into a lower universe. Is it so? >> >> I think that this is most natural way. >> >> But, to convince myself that often resizing is not needed, I wrote in >> Agda examples of similar "monads" T (e.g. the propositional truncation >> defined by ||X|| : (P : U) -> isProp P -> (X -> P) -> P) with universe >> juggling, by decorating the occurrences of U with indices. Although TX >> will live in the next universe, and hence so will the unit and the >> multiplication, and the monad laws (can be written down and) hold. >> >> Here I show the types only, where "i" is the level of the propositions >> you are considering: >> >> T : {i j : Level} → U j → U (j ⊔ lsuc i) >> >> η : {i j : Level} {X : U j} → X → T {i} {j} X >> >> T-extend : {i j k : Level} {X : U j} {Y : U k} >> → (X → T {i} {k} Y) → (T {i} {j} X → T {i} {k} Y) >> >> kleisli-law₀ : {i j : Level} {X : U j} >> → T-extend η ≡ id >> >> kleisli-law₁ : {i j k : Level} {X : U j} {Y : U k} >> (f : X → T {i} {k} Y) >> → T-extend f ∘ η ≡ f >> >> kleisli-law₂ : {i j k l : Level} {X : U j} {Y : U k} {Z : U l} >> (f : X → T {i} {k} Y) >> (g : Y → T {i} {l} Z) >> → T-extend(T-extend g ∘ f) ≡ (T-extend g) ∘ (T-extend f) >> >> μ : {i j : Level} {X : U j} >> → T {i} {j ⊔ lsuc i} (T {i} {j} X) → T {i} {j} X >> >> T-functor : {i j k : Level} {X : U j} {Y : U k} >> → (X → Y) → (T {i} {j} X → T {i} {k} Y) >> >> This works for the above example, and for lifting too. >> >> (Of course all this universe subscripting is ugly.) >> >> But I would prefer that somebody proved that propositional resizing >> (is consistent and) doesn't destroy normalization (e.g. in cubical >> type theory), and just use resizing. Or just keep my fingers crossed >> and work with propositional resizing. :-) >> >> Martin >> >>> >>> Vladimir. >>> >>>> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory wrote: >>>> >>>> >>>> >>>> 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 >>>> >>>> -- >>>> 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. >>> >> >