type resizing

Stream: general

[Reid Barton]

Suppose I have a type α : Type (u+1) and I know ∃ β : Type u, nonempty (β ≃ α). Is there a "canonical" (= without choice, I guess?) way to obtain a type α' : Type u and an equivalence α ≃ α'?

[Simon Hudon]

I think you would be able to prove the axiom of choice if you had that

[Simon Hudon]

Sorry, I take it back, you could pick α and α ≃ α' as the identity equivalence

[Mario Carneiro]

You could use ordinal to give it a kind of canonicity, but that doesn't really avoid choice, it's nonconstructive all over the place.

[Mario Carneiro]

Also that doesn't provide the equiv itself, just a proof of existence; only the type is canonical