The axiom [SVC](https://ncatlab.org/nlab/show/small+violations+of+choice) (for "small violations of choice") asserts that there is a set $S$ such that for every set $X$ there is a [choice set](https://ncatlab.org/nlab/show/choice+object) $A$ such that $X$ is a subquotient of (i.e. admits a surjection from a subset of) $A\times S$.


The original formulation of Blass ([Injectivity, projectivity, and the axiom of choice](https://doi.org/10.1090/S0002-9947-1979-0542870-6)) took $A$ to be an ordinal and the subquotient to be a surjection, which are equivalent in the presence of excluded middle; but the above version seems arguably more natural in intuitionistic logic. Blass showed that many models of set theory satisfy SVC, including permutation and symmetric models, $L(T)$, and ${\rm HOD}(T)$, but that SVC is not a consequence of ZF because it can fail in a class-forcing model.


In [Avoiding the axiom of choice in general category theory](https://doi.org/10.1016/0022-4049(95)00029-1), Makkai remarks (p171) that "direct topos-theoretic translates" of SVC do not hold in all Grothendieck toposes. This is intriguing because Grothendieck toposes are a rough category-theoretic correspondent of (ordinary, set-based, intuitionistic) forcing models; and if SVC can be violated in an ordinary forcing model, why did Blass have to recourse to a class-forcing model to prove its independence? Unfortunately, Makkai gives no examples or explanation.


So: what is an example of a Grothendieck topos (defined over a base model of ZFC) in whose internal logic the SVC fails? (An ordinary forcing model in which it fails would be interesting enough, although since a forcing model doesn't necessarily coincide exactly with its corresponding topos it might not quite answer the question yet.)



Failure of SVC in Grothendieck toposes
It seem to me that the problem that Makkai has in mind is that the existence of non-trivial choice objects is in conflict with non-booleaness. 


The core of the arguement, is the following lemma, which essentially follows from Diacunescu's proof that $AC \Rightarrow LEM$:


**Lemma:** Let $A$ be a choice object in a topos, then internally:


$$ \forall x,y \in A, \forall U \in \Omega, (U \Rightarrow (x=y)) \cup U $$


**Remark:** that is basically a rephrasing of lemma D4.5.11 of P.T.Johnstone sketches of an elephant.


**Proof:** Let $A$ be a choice object and $x, y \in A$. Let $U$ be any proposition, consider the set $1 \coprod\_U 1$ and the relation that send the first component to $x$ and the second to $y$ (and to both for element that are in both component). It is an entire relation to $A$, so there is function $1 \coprod\_U 1 \rightarrow A$ included in that relation, in particular which takes values in $\{x,y\}$. I'm calling $a$ and $b$ the "two" elements of $1 \coprod\_U 1$, I have four case to deal with regarding the values of $a$ and $b$ by this functions, but in each of them you can either prove $U$ or $U \Rightarrow (x,y)$:


* $a \mapsto x$ and $b \mapsto y$ then $U \Rightarrow (x=y)$
* $a \mapsto y$ then $U$
* $b \mapsto x$ then $U$
$\square$


Geometrically speaking, this is a pretty rough restriction on what can choice objects be ! it means that if $A$ is a choice object in a topos $\mathcal{T}$, and $a,b$ are two section of $A$ on $X$, then the closed complement of $(x=y)$ in $\mathcal{T} / X$ is Boolean. So either $A$ is very close to be subterminal, or the slices of $\mathcal{T}$ have some large boolean closed subtoposes. (this is the conflict I was referring to at the begining)


But one can do better:


**Proposition:** Let $\mathcal{T}$ be a Grothendieck topos which:


* Is nowhere boolean, i.e. no non-degenerate slice of $\mathcal{T}$ is boolean,
* satisfies SVC,


then $\mathcal{T}$ is degenerate. For example, $Sh([0,1])$ do not satisfies SVC.


Note that a nowhere boolean topos is a topos where LEM is internally false, in the sense that the interpretation of "$\forall U, U \cup \neg U$" in the internal logic is $\bot$ (the initial object).


We start with another lemma:


**Lemma:** In a nowhere boolean topos, if $A$ is a choice object and $D$ is decidable object (i.e. internally $\forall x,y \in D, x=y \cup x \neq y$) then one can internally show that:


$$ \texttt{Any partial map $A \rightarrow D$ is constant} $$


Indeed, consider internally a partial map $f:A \rightarrow D$, for each $a , a'$ in the domain of definition of $f$, either $f(a)=f(a')$ or $f(a) \neq f(a')$, but $f(a) \neq f(a')$ implies $a \neq a'$, which internally implies LEM by the previous lemma, which is false as $\mathcal{T}$ is nowhere boolean. Hence the result.


One can now prove the proposition: If one assumes further that $\mathcal{T}$ satisfies SVC, it means that every decidable object of $\mathcal{T}$ is a subquotient of the object $S$ (as the lemma above implies that the partial map $S \times A \rightarrow D$ is constant in the $A$-direction). But if $\mathcal{T}$ is non degenerate, for $\kappa$ large enough (larger than the size of the site and the size of $S$), the object $p^\* \kappa$ is locally decidable and of size $\kappa$, so it cannot be a subquotient of $S$.


**Edit:** *My apologies for the needlessly non mathematical and complicated first answer. I think I found the theorem I was after.*


