I've been looking into Kripke-Joyal semantics and, for each formula $\phi(x)$ defining an object $\{ x \, | \, \phi(x) \}$. Is it possible to, somehow, "fix a variable"? Let's say I've got a formula $\phi(x,y)$. Would I be able to "fix" $y$ and construct $\{ x \, | \, \phi(x,y) \}$. I'm trying to generalize what would in topos $\mathbf{Set}$ be a function $f:Y \to \mathcal{P}X$ such that $f(y) = \{ x \in X \, | \, \phi(x,y) \}$. The left hand side would, of course, be $f \circ y$. But which morphism would be on the right hand side. Since $x$ is the only free varible, i assume it would be a subobject of $X$ (where $x:U \to X$ is the generalized element).
I was thinking about somehow using the projection from $\{ (x,y) \, | \, \phi(x,y) \}$, but never got anywhere.
Another idea was just defining a term $\sigma(y) := \forall y(f(y) = \{ x \, | \, \phi(x,y) \})$ but didn't know how would I do it, since the very thing I'm trying to define is inside that term.
The next idea was using the exponential transpose, but then I would end up with a term of type $\Omega^Y$, instead of $\Omega$, so I couldn't get the pullback of $1 \to \Omega$ along $\lambda y \phi(x)$.