Conceptual proof of product preservation for the coproduct in product-preserving presheaves

Develop a conceptual proof that the coproduct defined by the coend (P + Q)(c) := ∫_{c1,c2 ∈ C} Hom_C(c1 × c2, c) × P(c1) × Q(c2) in the category Func(C^op, Set)[×] of product-preserving presheaves yields a product-preserving presheaf, i.e., show conceptually that P + Q preserves finite products whenever P and Q preserve finite products.

Background

In the two-dimensional stable semantics, the category Func(Cop, Set)[×] of product-preserving presheaves arises as the sifted colimit completion of a category C with finite products and coproducts. Adámek–Rosický–Vitale show the existence of coproducts in this category abstractly, but the paper gives a direct coend formula for the coproduct to align with the stable-disjunction semantics.

While the object defined via the coend has the correct universal property of a coproduct, establishing that this construction is itself product-preserving (so it lies in Func(Cop, Set)[×]) is not presented by a conceptual argument in the paper; instead, product preservation is inferred by decomposing presheaves as sifted colimits and using closure properties. The open issue is to supply a direct, conceptual proof of product preservation for the coend-defined coproduct.

References

It is easy to prove that this object has the right universal property. However, a conceptual proof that it is product-preserving eludes me.

— Two-dimensional Kripke Semantics II: Stability and Completeness  (2406.03578 - Kavvos, 2024) in Section 5 (Two-dimensional stable semantics of intuitionistic logic), after the theorem giving the coend formula for the coproduct