Re: [HoTT] Conjecture

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

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