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:


$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'.$$

  • $\begingroup$ Hm, yes, I see... I now realize that this contradiction can also be seen by regarding Lemmas 3.8.2 and 3.8.5 (of the HoTT book). $\endgroup$ – Daniel Gerigk Feb 6 '17 at 14:14
  • $\begingroup$ Actually, if we restrict $\Xi$ to sets, then it still implies AC, and this argument shows that it still contradicts UA. $\endgroup$ – Valery Isaev Feb 6 '17 at 14:45
  • $\begingroup$ 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. $\endgroup$ – Daniel Gerigk Feb 6 '17 at 18:19
  • $\begingroup$ Ah, yes, you right. I edited the post, so the proof applies to $\Xi_0 : \prod_{A : Set} \| A \| \to A$ $\endgroup$ – Valery Isaev Feb 6 '17 at 18:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.