I'm confused about these lecture notes. Theorem 4 states, roughly, that for each coherent category $C$ there is a pretopos $C^\mathrm{eq}$ such that for any pretopos $D$, morphisms of coherent categories $C\to D$ correspond to morphisms of coherent categories $C^\mathrm{eq}\to D$.
In the same theorem it says:
In particular, [...] induces an equivalence of categories $\mathrm{Mod}(C^\mathrm{eq})\to \mathrm{Mod}(C)$.
Confusing point: Definition 2 defines models of a pretopos $P$ as morphisms of pretoposes $P\to\mathbf{Set}$. But since Theorem 4 only talks about morphisms of coherent categories I think both $\mathrm{Mod}$s in the above quote are meant to be models in the sense of Definition 8 from Lecture 5 and not in the sense of Definition 2. Is that right?
Second question: for each coherent category $C$ is there a pretopos $C'$ such that for any pretopos $D$, morphisms of coherent categories $C\to D$ correspond to morphisms of pretoposes $C'\to D$? If yes, as a special case one would get that the category of models of $C'$ as a pretopos (Definition 2 in Lecture 8) are the same as models of $C$ as a coherent category. Isn't that more natural anyway? Or can you convince me with arguments that Theorem 4 is really what one wants to say?
(Another confusing point is that the notes speak about weak syntactic categories, which are coherent categories in these notes, of first-order theories. But coherent categories correspond to coherent logic and not first-order logic.)