In a topos ${\mathcal{A}}$, given a group object $G$ and a subgroup $H$, the object $H\backslash G$ of right cosets is the coequalizer of two maps $G\times H\rightrightarrows G$, namely the group multiplication and the projection onto $G$. Denote the coequalizing map by $H\backslash -$: $$G\times H\rightrightarrows G\xrightarrow{H\backslash -}H\backslash G$$

Say that a map $f:X\to Y$ is a *product projection* if it is part of a span $Z\leftarrow X\xrightarrow{f} Y$ that writes $X$ as a product of $Y$ and $Z$. One can show that $H\backslash -:G\to H\backslash G$ has a section if and only if it is a product projection. If so, then in fact $G$ is the product of $H$ and $H\backslash G$:
$$G\simeq H\times H\backslash G$$

In the topos ${\mathcal{FinSet}}$ of finite sets, the external axiom of choice holds, which is to say that every epimorphism has a section. The map $H\backslash -$ is an epimorphism, hence has a section if $G$ is a finite group, hence $G\simeq H\times H\backslash G$. This is (a strong form of) Lagrange's theorem.

Say that a topos ${\mathcal{A}}$ *satisfies Lagrange's theorem* if, for each group object $G$ and a subgroup $H$, the map $H\backslash -:G\to H\backslash G$ has a section (or equivalently, is a product projection). ~~For example, the topos ${\mathcal{Top}}$ of topological spaces and continuous maps does not satisfy Lagrange's theorem as the Hopf fibration $S^1\to S^3\to S^2$ is a counterexample. ~~

The external axiom of choice implies Lagrange's theorem. Hence the topos ${\mathcal{Set}}$ satisfies Lagrange's theorem. The internal axiom of choice, namely that exponentials $-^X:{\mathcal{A}}\to{\mathcal{A}}$ preserve epimorphisms, is weaker than the external axiom of choice. My question is:

Does there exist a topos that satisfies the internal axiom of choice but not Lagrange's theorem?

category$\mathbf{Top}$ is not a topos: it is not cartesian closed, it has no subobject classifier, etc. etc. I'm also inclined to say your formulation of Lagrange's theorem is wrong: even in $\mathbf{Set}$, the bijection $G \cong (G / H) \times H$ is highly non-canonical. $\endgroup$ – Zhen Lin Oct 29 '13 at 18:03