How would I go about modeling theories and doing math in a general topos, instead of just Set.
For example, in Set, I might define a groups as "a set which satisfies the following conditions: ..." and then work onwards from there, prove theorems and such.
Now, in a topos, there are Mitchell-Bénabou language and Kripke-Joyal semantics to model formulas, of course. I'm interested, if possible, to learn how to think in terms of topos theory. So I could take an arbitrary topos and, for example, study group theory there, by defining a group and using internal logic to prove theorems.
I assume, the definition would be more or less analogous to set-theoretic, I'd take an object $G$ and morphism $*:G \times G \to G$ and define a group $(G,*)$ such that for any generalized elements the following holds: $a,b,c:G$, $(a*b)*c = a*(b*c)$, there exists a generalized element $e_G:G$ such that, for any $a:G$, $e_G * a = a * e_G = a$, etc.
Now, when looking at more complicated formulas, using quantifiers and logical connectives, I should be able to use theorems about the internal logic of the topos to know that there exists an object $\{ (\vec{x}) |\varphi(\vec{x}) \}$, analogous to (sub)set of objects satisfying a formula. But how do I actually use the internal logic to describe and talk about the theories.
But for more complicated formulas, how would I prove or disprove, say, a theorem which says something about those subobjects generated by formulas? For example, if I had formulas which use morphisms and I want to prove or disprove that $\varphi_g \varphi_f = \varphi_{gf}$, similar to how one would show in Set that $(g \circ f)(A) = g(f(A))$, where $A$ is a subset of the domain of $f$, so $f:\mathcal{P}X \to \mathcal{P}Y$ is a function that is constructed using $f:X \to Y$?
