Principal bundle if and only if trivial quotient

Lemma 6.36.

Let $p\colon P \twoheadrightarrow B$ be an effective epimorphism equipped with a $\Gg$ -action over $$B$$ , and let $P\quot\Gg \in T_{/B}$ denote the quotient. Then $$p$$ is a principal $\Gg$ -bundle if and only if the canonical map $P\quot\Gg \to B$ is an isomorphism.

Proof

This is an instance of Lemma 6.33 applied in the slice topos

T_{/B}