Can an object be considered the same if we change its type?

[marcbezem]

I struggled with this question when modifying intro.tex, with the object being the square and the ambient type (not exactly the type of the square) the plane or the oriented plane. I think Bjørn formulated a similar question yesterday, just before we wrapped up because of HoTTEST. (Bjørn: correct me if I misunderstood.)

Technically, in type theory, I think the answer is almost always "no", with the following two possible exceptions.

1. If T_P is a subtype of T, then we consider (x,!) : T_P the same as x : T. However: (x,!) has the same symmetries in T_P as x has in T. So, considering (x,!) : T_P the same as x : T is very convenient and appropriate, but one cannot exclude, e.g., reflections as symmetries of the square by taking a suitable subtype. One has to add structure to the type (e.g., order the base vectors), and this ought to change the object as well, for the very reason that the purpose is to change the symmetries of the object.
2. Less obvious to me is the case where the object is a type A in a universe U which is small in a universe V. Then also A : V. However, UA gives an equivalence between A =_U A and A =_V A. So, yes, A can be considered the same object in U and in V.

Also non-technically, I think the square with rotational symmetries is different from the square with other symmetries as well.

Any opinions? And, in particular, any ideas how to convey this idea to the reader of the introduction?