Definition 7.9 (Topos). A topos is a regular category $E$ for which the embedding $E\to Rel(E)$ sending $f$ to $f_{\bullet }$ has a right adjoint. We write the effect of the right adjoint on objects by $A\mapsto PA$, and the unit $A\to PA$ as ${\{\}}_A$, and the counit $PA\looparrowright A$ as ${\exists }_A\rightarrowtail PA\times A$.