Perhaps to get a one-to-one correspondence, one would need to relax the requirement that the logic be a fragment of first-order logic, then?

@SimonHenry: thanks. I had overlooked the distributivity condition for disjunction.

Any topos with a natural numbers object, e.g. a Grothendieck topos, is a W-pretopos. So the category of presheaves $[\mathbf C^{\mathrm{op}}, \mathrm{Set}]$ for any small category $\mathbf C$ models inductive types; or the category of sheaves over any small site.

Inductive data types are the same as W-types, which are represented categorically by initial algebras for polynomial functors. Therefore any category with initial algebras for polynomial functors (e.g. a W-pretopos) will be able to interpret inductive types.

In Lawvere theories enriched over a general base, Nishizawa and Power describe the 1-monad for cartesian-closed categories on $\mathrm{Cat}$. By allowing the arities of the monad to differ from the base of enrichment, they can describe contravariant structure. Presumably the same method also works for the 2-monad on $\mathrm{Cat}_g$.

@IvanDiLiberti: I accept this is certainly a possibility.

@TimCampion: I feel the condition that "every object is the equaliser of a finite product of objects in the image of $F$" is rather inelegant, compared to the structured subobject conditions of the examples.

Let me note that there is an intuitive characterisation of the categories representing these theories: they are those finitely complete categories $\mathscr C$ with an injective-on-objects functor $F : S \to \mathscr C$, such that every object is the equaliser of a finite product of objects in the image of $F$. This is really the definition I want to capture, but it is not obvious to me how to make this precise in a manner as elegant as the examples in the question.

@TimCampion: a categorical formulation is not obvious (which is the main motivation for the question), so for the purposes of this question, an $S$-sorted essentially algebraic theory is defined syntactically (i.e. as quadruple $\Gamma = (\Sigma, E, \Sigma_t, \mathrm{Def})$): here, there is an explicit set of sorts.

@TimCampion: $S$-sorted algebraic theory here means a "cartesian category $\mathscr A$ together with a strict identity-on-objects finite product-preserving functor $\mathbb A(S) \to \mathscr A$", where $\mathbb A(S)$ is the free strict cartesian category on the set $A$, as in Bénabou's Structures algébriques dans les catégories.

@TimCampion: thanks, I had completely overlooked that observation in ABLR. I've edited the question to make my intent clearer.