Re: [HoTT] Conjecture

[Martin Escardo <escardo...@googlemail.com>]

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 <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.
>>>
>>
>