idle equiv question

Stream: general

[Kevin Buzzard]

universes u v
def αu (X Y : Type u) := X → Y
def αv {X : Type u} {Y : Type v} := X → Y
def αuv {X Y : Type v} := X → Y

[Kevin Buzzard]

Which of those types are related by equiv?

[Kevin Buzzard]

equiv is my new toy

[Kevin Buzzard]

and I realise I don't understand universes

[Chris Hughes]

none of them? equiv has nothing to do with universes.

[Gabriel Ebner]

All of them? Given X and Y, all of αu X Y, @αv X Y, and @αuv X Y are definitionally equal (and hence equiv). You cannot even state that αu ≃ @αuv (as they are not types).

[Gabriel Ebner]

Since you're worried about universes, let me annotate the first example with universes: Given X : Type u and Y : Type u, all of αu.{u} X Y, @αv.{u u} X Y, and @αuv.{u} X Y are definitionally equal (and hence equiv). The only potential way to even write down this statement is by using the same universe variable for both X and Y.

[Gabriel Ebner]

(deleted)

[Gabriel Ebner]

Maybe it's useful to think about the interpretation of equiv in the set-theoretic model: there, two sets are equiv iff they have the same cardinality. And Type u is the u-th inaccessible cardinal. So you're asking when two function spaces are equinumerous.

[Kevin Buzzard]

The question that remains, which is not particularly well-defined, is whether it is somehow possible using ulift to have {X : Type u} and {Y : Type v} and (maybe using ulift here) making some kind ofalphau X Y which is equiv to alphauv X Y

[Mario Carneiro]

sure, U -> V is equiv to ulift U -> V or U -> ulift V

[Mario Carneiro]

(not sure why you are writing it with the funny notation, but that's just the arrow type)