Has the "Lambek embedding" into the category of (co)product-preserving presheaves been studied very much?

Question

The Lambek embedding is a particular embedding which is similar to the Yoneda embedding.

Suppose we have any category $C$. Recall that a presheaf on $C$ is defined as a contravariant functor from $C$ to $\mathrm{Set}$, and the category of presheaves and natural transformations thereof is denoted $\widehat{C}$. The category $\widehat{C}$ is always a topos. The Yoneda embedding is an embedding $C \to \widehat{C}$ which preserves limits, but it does not always preserve colimits.

Fu et al., in the paper "On the Lambek embedding and the category of product-preserving presheaves," describe the Lambek embedding as follows. First, define a product-preserving presheaf as a contravariant functor from $C$ to $\mathrm{Set}$ which maps coproducts to products. Denote the category of product-preserving presheaves, and natural transformations thereof, as $C^\times$ (my notation). The Lambek embedding is the embedding $C \to C^\times$ which is identical to the Yoneda embedding except that its codomain is merely $C^\times$ instead of all of $\widehat{C}$.

In general, the category $C^\times$ is not quite as nice as $\widehat{C}$. According to the paper, $C^\times$ has all limits and colimits. Furthermore, if I understand correctly, if $C$ has all finite products, then $C^\times$ is cartesian closed.

The main interesting feature of the Lambek embedding is that it preserves not only limits, but colimits as well^[1]. As such, the Lambek embedding seems like it would be a very useful tool for studying categories which have products and coproducts but not much other structure. We can do whatever we want with limits, colimits, and exponentials in $C^\times$, and then as long as our result involves only limits and coproducts that exist in $C$, that result must hold in $C$ as well.

Given this, I would have guessed that this embedding was pretty well-known and well-studied prior to the 2022 paper by Fu et al. Granted, it appears that the name "Lambek embedding" was given to it in the 2022 paper, so any earlier references to the embedding would have had to call it something else. But I haven't found any references to it under any other name, either.

The Fu et al. paper cites Joachim Lambek (1966): Completions of categories, which presumably contains at least some discussion of the embedding, but I don't have a copy of that publication, so I don't know how extensively the embedding is discussed there.

So, has the Lambek embedding been studied and written about much? Is there a place where I can learn more about it beyond the information in Fu et al.'s paper?

(In case anyone is curious, the specific example of $C$ that I'm interested in is the category of primitive recursively decidable sets, and primitive recursive functions between them. If I'm not mistaken, that category has finite limits and coproducts, but is not cartesian closed, and the Lambek embedding seems like a great way to "bolt on" cartesian closure. I want to figure out if the resulting category would serve as an interesting foundation for mathematics.)

[1]: Actually, varkor points out in their answer that if we define $C^\times$ as the category of $\Phi$-limit-preserving presheaves, then the embedding only preserves $\Phi$-colimits. For example, if $C^\times$ contains all presheaves preserving finite products, then we only know that the embedding preserves finite coproducts.

Answer 1

This construction is well known in enriched category theory, and has been studied in the increased generality of a class of weights (which recovers the finite discrete weights, describing finite (co)products as a special case) in §6 of Kelly's Basic Concepts of Enriched Category Theory. See for instance Proposition 6.13 ibid. Note that the Yoneda embedding into the category of $\Phi$-limit-preserving presheaves only preserves $\Phi$-colimits, not arbitrary colimits. The embedding into the category of finite product-preserving presheaves therefore preserves finite coproducts, not arbitrary colimits.

For the case of finite products specifically, another good reference is Adámek–Rosický's On sifted colimits and generalized varieties (for the case when the category in question has finite coproducts).

Answer 2

It's not quite the same thing, but the full subcategory of presheaves preserving finite products (say call it $C^{f\times}$) is studied by Lurie in Higher Topos Theory section 5.5.8.

While $C\to\widehat C$ freely adjoins all colimits, the construction $C\to C^{f\times}$ freely adjoins sifted colimits and preserves finite coproducts.

(Actually, the paper you cite says "preserves products" but appears to mean "preserves finite products" --- maybe you do as well?)