I have hyperlinked that to *doubly closed monoidal category*.

Mention that Day convolution and slice over a monoid are always biclosed monoidal

]]>Ah of course.

It occurs to me that this monoidal structure is actually the same as the monoidal structure on a glued category in Section 4 of Hyland and Schalk by representing the monoid object in the topos as a lax monoidal functor $1 \to H$ where $1$ is trivially monoidal closed.

]]>The internal hom constructed in that answer is in fact an object of $\mathscr{F}/T$. Recall that the phrase “the pullback of a map $B \to C$ along a map $A \to C$” refers to the projection map $A\times_C B \to A$.

]]>I must be missing something, the construction in that answer is an object of $F / [G,T]$ not $F / T$

]]>Yes, that’s true, and one can give an easy construction of the internal hom; see this MO answer.

]]>Also am I correct that the slice over a monoid object in a topos is always monoidal *closed*? Seems to follow by the AFT because the tensor product should preserve colimits in each argument because colimits are computed in the original category and the cartesian product preserves colimits in each argument.

If so I’ll add that to the page too.

]]>Observe that the overlap between Day convolution and slice over a monoid object agree.

]]>added (here) mentioning of the example of tangent $\infty$-toposes.

It ought to be true that every $\infty$-topos arising from parameterized objects in an $\otimes$-monoidal Joyal locus carries the corresponding external $\otimes$-tensor product — but now that I say this I realize that this needs a formal argument which might be easy but I haven’t fully thought about.

]]>added to the Idea-section (here) a sentence pointing to *doubly closed monoidal category*.

Relation to bunched logic

]]>