# The axiom $\Xi : \prod_{A:\mathcal{U}} \|A\| \to A$ and the $n$-truncation of a type

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?

This rule contradicts the univalence axiom. Indeed, first note that it implies the axiom of choice: $$\prod_{x : A} \| B x \| \to \| \prod_{x : A} B x \|.$$ $\Xi$ implies that $\prod_{x : A} \| B x \| \to \prod_{x : A} B x$. Hence, the axiom of choice holds.
The axiom of choice implies the law of excluded middle: $$\prod_{P : Prop} P \lor \neg P.$$ This implies that for every set $A$, $\| A \| \lor \neg A$. It follows that for every set $A$, $\| A + \neg A \|$, and $\Xi$ implies that $$\prod_{A : Set} A + \neg A,$$ which contradicts the univalence axiom.
Also, consider the following weakening of $\Xi$: $$\Xi' : \prod_{A : \mathcal{U}} \| \| A \| \to A \|.$$ The law of excluded middle implies this axiom. Indeed, apply LEM to $\| A \|$. If $\| A \|$ holds, then $\| \| A \| \to A \|$ also holds. If $\|A\| \to \bot$ holds, then $\| A \| \to A$ holds. Thus, we have the following implications: $$\Xi \to AC \to LEM \to \Xi'.$$
• Actually, if we restrict $\Xi$ to sets, then it still implies AC, and this argument shows that it still contradicts UA. – Valery Isaev Feb 6 '17 at 14:45
• But I think you mean $\prod_{X:\mathcal{U}} X + \neg X$ instead of $\prod_{P:\text{Prop}} P \vee \neg P$, am I right? Because the latter would be just LEM ( - if your $\vee$ is interpreted as a $+$ - ), which doesn't contradict the univalence axiom. – Daniel Gerigk Feb 6 '17 at 18:19
• Ah, yes, you right. I edited the post, so the proof applies to $\Xi_0 : \prod_{A : Set} \| A \| \to A$ – Valery Isaev Feb 6 '17 at 18:29