TITLE: What is the monoidal equivalent of a locally cartesian closed category?
QUESTION [16 upvotes]: If a closed monoidal category is the monoidal equivalent of a Cartesian closed category, is there an analogous equivalent for locally cartesian closed categories? Is there a standard terminology or reference for such a construction?

REPLY [1 votes]: The proposed use of comonoid homomorphisms in the other answers is intriguing, but there are more basic things about locally cartesian closed categories that need to be loosened first, although conceivably the homomorphisms generalise what I am about to say.
We have known for decades that substitution is pullback, though I haven't seen a formalisation and proof of this other than the one in Chapter VIII of my book.
Lawvere said that the quantifiers adjoint to substitution, but that is not accurate: they are actually adjoint to weakening.
Also, the two legs of a pullback do not play the same role: one is substitution or weakening and other is the display of a type.
There is a more subtle version of the traditional notion in which the adjoints are only required over a certain pullback-stable class of "display maps".
Plain and local cartesian closure are the extremes in which this class consists of just product projections or all maps, respectively.
In particular, the quantifiers over diagonals ($X\to X\times X$) are oddities that I will leave as an exercise.
It would be interesting to see how the other proposals on this page fit together with this.
{"set_name": "stack_exchange", "score": 16, "question_id": 205902}