Deje que $ \mathscr C$ ser una categoría cartesiana con clasificador de subobjetos $ \Omega $ y subobjeto genérico $ \tau :I \to\Omega $ . Considere el siguiente cuadro de retroceso:
$ \require {AMScd} \begin {CD} P @>{ \bar f}>> C \\ @V{ \bar g}VV @V{g}VV \\ A @>{f}>> B \end {CD}$
Probé que para cualquier $p:A \to\Omega $ la declaración $ \exists_ { \bar f}(p \circ\bar g) \implies \exists_f (p) \circ g$ es cierto.
¿Qué hay de lo contrario? $ \exists_f (p) \circ g \implies\exists_ { \bar f}(p \circ\bar g)$ ?
Mis intentos de probarlo en tal categoría fracasan. Por otro lado, parece ser intuitivamente cierto en un topos.
¿Qué supuestos son necesarios para que sea cierto?
Obsérvese que una cuestión similar se plantea para el cuantificador universal. En particular, $ \forall_f (p) \circ g \implies\forall_ { \bar f}(p \circ\bar g)$ es cierto. Por otra parte, encontré una prueba para el contrario $ \forall_ { \bar f}(p \circ\bar g) \implies \forall_f (p) \circ g$ cuando $g$ es monica.
