@PeterLeFanuLumsdaine done

No, it gives you the infinite delooping of the free symmetric infinity group on the underlying space. It's just like taking the free group on the underlying set of a group never gives you back the group you started with. (To begin with, you got a new neutral element.) As another example, consider the 0-sphere with one of its two group structures. The infinite suspension gives you the sphere spectrum, i.e., representing the free symmetric infinity group on one generator, and this is not a 2-element group.

HoTT+Propositional Resizing should fall roughly in the same bucket as Power-CZF, Power-KP, CZF+negative powerset, and (I)Z+<Bachmann–Howard many levels of the cumulative hierarchy, as in Thm. 15.1 of Rathjen's Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions.

Would it ease your discomfort to notice that this equivalence doesn't commute with the maps that takes underlying sets? So as abstract types, they can be identified, but not as types together with a notion of underlying set?

This modality is briefly discussed in Example 6.1 in Cellular properties of nilpotent spaces where they show that $S^3$ is not $K(\mathbb{Z},2)$-connected.

Without propositional resizing, unique choice is a scheme over the universe level of the relation $R$. (It is in any case a scheme over the universe levels of the types (they don't have to be sets!) $A$ and $B$.) Your version follows from the stronger principle, given types $A$ and $B$ and a (proposition-valued) relation $R$: $(\prod_{x:A}\mathrm{isContr}(\sum_{y:B}R(x,y))) \to \sum_{f:A\to B}\prod_{x:A}R(x,f(x))$ given by taken the center of contraction.

Just formulating GCH in HoTT doesn't imply it's consistency. But as Zhen Lin commented, we have the simplicial sets model and that gives an equivalence of the category of sets in the model with the ambient category of sets, so if GCH holds in the ambient set theory, it holds in the simplicial sets model of HoTT.

Girard has put Proof theory and logical complexity II on his site here: girard.perso.math.cnrs.fr/Archives4.html

You picked about the most complicated case possible, because we need subset collection (or strong collection + fullness). In any case, looking at Rathjen's proof, you obtain the description by combining Aczel's sets-as-trees interpretation of CZF into a version of Martin-Löf type theory with one inductive type of trees, together with a recursive realizability interpretation. (The Cauchy reals also form a set and would be easier to represent directly via codes for recursive functions.)