Re: [HoTT] Conjecture

[Vladimir Voevodsky <vlad...@ias.edu>]

[-- Attachment #1: Type: text/plain, Size: 2283 bytes --]

I looks like like you would also need the resizing rule to place hProp into a lower universe. Is it so?

Vladimir.

> On Apr 6, 2017, at 1:55 AM, 'Martin Escardo' via Homotopy Type Theory <HomotopyT...@googlegroups.com> 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.


[-- Attachment #2: Message signed with OpenPGP --]
[-- Type: application/pgp-signature, Size: 507 bytes --]