I'm looking for examples of proofs that some Quillen model categories are monoidal, or enriched over an other model category, which are based on explicit computation of the "pushout product" of the generating cofirbations and generating trivial cofibrations, i.e. an explicit combinatorial proofs of a statement like: if $i:A \rightarrow C$ and $j:B \rightarrow D$ are respectively a generating cofibrations and a generating trivial cofibration then the "pushout-product" map:

$$i \otimes' j : C \otimes B \coprod_{A \otimes B} A \otimes D \rightarrow C \otimes D$$

is a composite of pushout of the generating trivial cofibrations (or maybe a retract of one of these). And same things for pushout-product of generating cofibrations.

I'm specifically interested in $\omega$-combinatorial model category, i.e. locally finitely presentable categories, with the generating cofibration and generating trivial cofibrations being maps between finitely presentable objects.

$\otimes$ above can either bi a monoidal structures or the tensoring for some enrichment. I also accept things that are not quite monoidal structure, as long as they are "bi-closed", so that this sort of condition does implies somethings (for example, the dendroidal "tensor product"), or things that are not quite model structures (like opetopic sets) if you have such combinatorial proof.

I already have some example where the condition are very easy to check:

- The model structure on ordinary category with cartesian product.
- Chain complexes.

In the literature I found such a proof for simplicial sets (both for the model structure for Kan complexes and for quasicategory) For Kan complex theorem 3.2.3 of Joyal & Tierney notes on simplicial homotopy theory does a special case, but it appears to be enough for deducing the general case by just playing around with the formal properties of the pushout-product. Similarly, Prop 2.3.2.1 of Lurie's Higher topos theory does a special case for the model structure for quasi-category, which also appears to be sufficient by formal property of the pushout-product.

In both case, the proof of the special case are pure combinatorics.

Cubical sets are also relatively easy to treat, but I still would prefer a reference if it exists.

I would be interested to see other examples of such direct combinatorics proof (like dendroidal sets, cellular sets, complicial sets, other algebraic structure , I assume no such things is known for opetopic sets but I would love to be wrong on that ).

Motivation : I'm finishing a paper about constructing some "weak" (like left & right semi structure) Quillen model structures in constructive mathematics. I have results which says that essentially when these kind of properties are verified then you can get some sort of weak model structure completely constructively. As these properties are purely combinatorial, there proof are generally constructive. I'd like to give as much example as I can, but proving myself that these conditions are indeed constructively valid is out of the scope of the paper if it takes more than five line. I can always invoke principle like Barr's covering theorem to say that constructive proof exists, but having a "clearly constructive proof" in the Litterature that I can quote is considerably better.