According to Axiom 3.5.5 of the HoTT book, we have propositional resizing if there is a some f and H such that
f : Prop$_u$$_{_i}$ $\rightarrow$ Prop$_u$$_{_{i+1}}$
H : isequiv(f)
The idea is that p and (f p) are in some sense 'equivalent' for any p : Prop$_u$$_{_i}$, and similarly for q and (f$^{-1}$ q) for any q : Prop$_u$$_{_{i+1}}$.
Now here is my question: given two propositions that are equivalent by propositional resizing, does truth of one necessarily imply the truth of the other? In other words, can we assume the following lemmas?
lemma1 : $\Pi$ (p : Prop$_u$$_{_i}$), p $\rightarrow$ (f p)
lemma2 : $\Pi$ (p : Prop$_u$$_{_i}$), (f p) $\rightarrow$ p
lemma3 : $\Pi$ (q : Prop$_u$$_{_{i+1}}$), q $\rightarrow$ (f$^{-1}$ q)
lemma4 : $\Pi$ (q : Prop$_u$$_{_{i+1}}$), (f$^{-1}$ q) $\rightarrow$ q
On one hand it seems plausible that moving from one equivalent form to another should preserve the truth of a proposition. On the other hand, I have no idea whether/how they can be derived, or assumed consistently as axioms. Are lemmas 1-4 admissible in HoTT with propositional resizing?
Axiom 3.5.5 actually says that the map Prop$_{U_{i}}$ $\to$ Prop$_{U_{i+1}}$ is an equivalence. As discussed in section 3.1, it is assumed that the universes are cumulative. So if P : Prop$_{U_{i}}$, then P : Prop$_{U_{i+1}}$. It's this map that's an equivalence, according to Axiom 3.5.5.
So lemma 1 is true even without propositional resizing. The type (P : Prop$_{U_{i}}$) $\to$ (P : Prop$_{U_{i+1}}$) lives in $U_{i+1}$, and it is inhabited by the identity map P $\to$ P, appropriately typed. If you would like the type (P : Prop$_{U_{i}}$) $\to$ (P : Prop$_{U_{i+1}}$) to live in $U_{i}$, then you would need to assume propositional resizing. Then to give a term of type [(P : Prop$_{U_{i}}$) $\to$ (P : Prop$_{U_{i+1}}$)] : Prop$_{U_{i}}$, you would apply propositional resizing to a term of type [(P : Prop$_{U_{i}}$) $\to$ (P : Prop$_{U_{i+1}}$)] : Prop$_{U_{i+1}}$. And this is the aforementioned identity map. Lemma 2 is similar.
For 3, the type (P : Prop$_{U_{i + 1}}$) $\to$ (f$^{-1}$(P) : Prop$_{U_{i}}$) lives in $U_{i + 1}$, so we're tacitly applying f to the codomain. So we need a map P $\to$ f(f$^{-1}$(P)), which we have because f is an equivalence.