Define an (elementary) topos to be a cartesian closed category with all finite limits and subobject classifiers. I'm looking for a proof of the fact that a topos also has all finite colimits.
I know that there is a proof by Paré using monad theory; but I do not know yet how a monad works, and I would like to see an explicit construction. For example, how can one construct an initial object from the axioms of a topos ? Or a coproduct ?
I have some vague ideas coming from the example where the topos is $\mathbf{Set}$, for example trying to construct $A\coprod B$ as a subset of $\Omega^{A\prod B}$, but I haven't managed to make any of them work.
For each object $X$ the singleton subobjects $\{x\}:\Omega^X$ are minimal inhabited subobjects. Call the elements of the limit $\lim_X\Omega^{DX}$ inhabited if the disjunction $\bigvee_{d\in D_0}(\exists y: Dd.x_d(y))$ is valid--here $D_0$ is the finite set of objects of the diagram $D$. Now the colimit $\mathrm{colim}_x Dx$ is isomorphic to the subobject of minimal inhabited elements of $\lim_x\Omega^{Dx}$.
Edit: I assume that if you want to learn topos theory and do difficult things like defining colimits, you will figure out the details of the construction yourself. I will add some spoilers below just in case.
Thanks to their internal languages toposes are like parallel universes of mathematics whose logic can be constructive and which can contains things of different types than sets. So instead of $x\in y$ ($x$ is in $y$), I write $x:y$ ($x$ is of type $y$), instead of 'non empty' I say 'inhabited' and instead of 'true' I say 'valid'. It is a more accurate wording that sets the internal language of the topos apart from the external language of set theory.
The precise meaning of inhabited in toposes is subtle. Each morphism in a topos factors as a monomorphism following an epimorphism. For each object $X$ the unique morphism $!:X\to 1$ factors as the mono $\mathrm{supp}(X)\to 1$ after the epi $X\to\mathrm{supp}(X)$. The object $\mathrm{supp}(X)$ is the support of $X$. When the mono $\mathrm{supp}(X)\to 1$ is an isomorphism, $X$ is globally supported or inhabited.
For each object $X$ a morphism $\chi: X\to \Omega$ characterizes some subobject of $X$ and this subobject can also be inhabited. Parallel to the support construction, there is a morphism $(\chi\mapsto\exists x: X.\chi(x)):\Omega^X\to \Omega$, and when the subobject that $\chi$ characterizes is inhabited, $\exists x: X.\chi(x)=\top$, the greatest element of $\Omega$. Other ways to say this are that the proposition $\exists x: X.\chi(x)$ is valid and that $\chi$ is an inhabited subobject of $X$.
Minimal means the same thing here as it does everywhere. If $x$ is a minimal inhabited subobject and $y$ is a smaller inhabited subobject, then $y=x$.