Dependent product functor

Stream: mathlib4

[Robert Maxton]

So, having run into one too many cases where I wished I could talk about "dependently typed functors," I'm implementing the generalized dependent product functor in an arbitrary cartesian closed category.

I've gotten most of the way through the setup, only to realize belatedly that my source (nLab) has been implicitly defining the internal dependent product in a way that doesn't actually need to be talking about the canonical categorical product, but in fact can be defined relative to any arbitrary tensor product/cartesian structure.

I would kind of like to incorporate that generality into my definition, but I'm not entirely sure what the best way to do that is. In particular, I'd need there to be versions of docs#CategoryTheory.Over.pullback and docs#CategoryTheory.Over.star defined relative to said arbitrary cartesian structure.

... So, first of all, does this exist in Mathlib? And second of all, is there a better way of doing what I'm trying to do here?

[Robert Maxton]

... And now that I think about this further, I'm no longer confident that this is even mathematically sound to begin with; the tensor product will define its own subcategory of internal homs that won't really line up with Over, so I really need to be talking about that instead.