I'm reading Sheaves in Geometry and logic and the authors mention that the a filtered diagram comprised of logical morphisms has a topos colimit and the legs are logical as well.
I know the authors prove a special case for the filter-quotient construction but I haven't looked at it and instead I'm attempting to prove the general version myself.
I wanted to ask if the approach I'll outline works so I can work on the details.
First of all (IIRC), a coequalizer of categories is a free category of "compatible" sequences in the sense domain and codomain are equivalent w.r.t. to the relation (that relation in that case being $F(A) \sim G(A)$), modulo the same relation ($F(f_n) \cdots F(f_1) \sim G(f_n) \cdots G(f_1)$).
Because of that, I'm guessing based on the case of sets that an arbitrary small colimit of categories is also a "free category modulo relation" of the direct sum of all categories but with the relation being that of being connected (for objects and morphisms as well). Now since the diagram is filtered, we can instead say they get equalized by some cone under.
Now, if I consider each of these "compatible sequences" of morphisms $f_n \cdots f_1$ in our colimit, with domains $A_i$ and codomains $B_i$, I can find a category below all categories containing morphisms so all morphisms are in the same category, and moreover the cone equalizes all $B_i$ and $A_{i+1}$, so every equivalence class of compatible sequences can be represented by a legitimate composition in some category.
Firstly, for limits, given $A$, $B$ I go to the category below with both, construct a product, and then for any C with arrows (compatible sequences) to A and B in our colimit, we use reasoning above to consider a pair of legitimate arrows in some category, and since logical morphisms preserve the property of beong a product, we get an induced arrow. Equalizers are treated similarly.
For subobject classifiers we pick some subobject classifier $\Omega$ of a category in the diagram, then we take a look at hom sets in our colimit category. Since it is filtered, so our compatible sequences between objects are legitimate arrows in some category, my guess is that thus $Hom(A, \Omega)$ can be described as the colimit of such hom sets for all categories with representants for $A$ and $\Omega$ (with functor arrows acting by application). Then we do same for $Sub(A)$ (noting logic morphisms preserve pullbacks), and then we have naturality for fixed $A$ and between both diagrams (because of pullback preservation), thus inducing an iso between the colimit category hom set and subobject set which are colimits. Since I fixed $A$, I still need to check naturality of such isomorphism. Probably something similar for the exponential adjunction as well.
In summary, all reasoning shows the need objects can be obtained in some category of the diagram, and then I can take their equivalence class, all thanks to morphisms in the diagram being logic.
I've made several assertions regarding the form of the colimit, the form of set of hom sets and subobjects (as well as my reasoning about sequences being "legitimate" sequences) whose validity I'm not confident of, and this is more of a sketch for my attempt, so I'd like to ask if someone could tell me if my reasoning is correct (or if at least I'm in the right path), since I'm new to these concepts and so there might be a lot of mistakes in my reasoning.
Any help is appreciated, and sorry for the wall of text!
EDIT: I think my assumption about Sub is incorrect, that is, representants for monos in the colimit category don't seem to be necessarily monos in some category.
Never mind, I forgot I can use pullbacks to characterize monos, so the above statement holds.