My question is whether the following has been considered as an axiom, and if so, where I may find a discussion of it:

$\Xi : \prod_{A : \mathcal{U}} \|A\| \to A$.

For example, using this axiom, we can define the $n$-truncation of a type $A$ in the following way:

Let

$P(A) :\equiv \sum_{X : \mathcal{U}} \sum_{\alpha : A \to X}\sum_{\beta : X \to A} (\alpha \circ \beta = \text{id}_B) \times (\text{is-}n\text{-type }X)$.

We easily find that $P(A)$ is inhabited ($X :\equiv \|A\|$, $\alpha :\equiv |\cdot|_A$, $\beta :\equiv \Xi_A$, $\dots$):

p : P(A).

Using $\Xi_{P(A)} : \|P(A)\| \to P(A)$, we obtain a term

$\Xi_{P(A)}(|p|_{P(A)}) : P(A)$.

My impression is that the $X$ that may be extracted from this last term behaves like the freest possible $n$-type with retraction from A on it, which in turn should behave just like $\|A\|_n$. Is that true?