I am struggeling to understand lemma 7.20 of the paper Stack Semantic and the Comparison of Material and Structural Set Theories by Mike Shulman. It contains formal sequents of the form $$U \Vdash \ulcorner V\Vdash \phi\urcorner$$ and I do not understand how I can remove the Quine-Corners in a systematic way. I would love to see an explicit example.

So let let $p: V\to U$ be a morphism in the base category $\mathscr S$, let $e:X\to Y$ be a morphism in the slice category $\mathscr S/V$ and let $\phi$ be the statement that $e$ is epi. How do I remove the Quine corner in the expression below systematically?

$$U\Vdash \ulcorner V \Vdash \forall Z:Ob. \forall f,g:Y\to Z. fe =ge \to f = g\urcorner$$

Edit. I have moved the question from the proofassistant stackexchange site to this site because I was told to do so. I hope it is welcome here.

I believe that I can do the specific example above by using dependent types. I should get the following statement: $$U\Vdash \forall v:V. \forall y:Y(v).\exists x:X(v). e(v,x) = y$$ This is just a guess by me. I believe that $\ulcorner V\Vdash \phi\urcorner$ should mean that $\phi$ holds fiberwise, so I tried to express that in the internal language of the base category $\mathscr S$.

When I apply the Kripke-Joyal semantic to the above sequent then I see that it holds if and only if the pullback of $e$ along each morphism into the interpretation of $U,v:V$ is epi. That should be the same thing as $$U,v:V\Vdash \forall Z:Set.\forall f,g: Y(v)\to Z. f\circ e(v) =g\circ e(v) \to f = g$$ and hence the idempotence works out in that example. Have I done that correctly? If yes, how do I do it systematically?

I am struggling to understand lemma 7.20 of the paper Stack Semantics and the Comparison of Material and Structural Set Theories by Mike Shulman (arXiv:1004.3802). It contains formal sequents of the form $$U \Vdash \ulcorner V\Vdash \phi\urcorner$$ and I do not understand how I can remove the Quine-Corners in a systematic way. I would love to see an explicit example.

So let let $p: V\to U$ be a morphism in the base category $\mathscr S$, let $e:X\to Y$ be a morphism in the slice category $\mathscr S/V$ and let $\phi$ be the statement that $e$ is epi. How do I remove the Quine corner in the expression below systematically?

$$U\Vdash \ulcorner V \Vdash \forall Z:Ob. \forall f,g:Y\to Z. fe =ge \to f = g\urcorner$$

Edit. I have moved the question from the proofassistant stackexchange site to this site because I was told to do so. I hope it is welcome here.

I believe that I can do the specific example above by using dependent types. I should get the following statement: $$U\Vdash \forall v:V. \forall y:Y(v).\exists x:X(v). e(v,x) = y$$ This is just a guess by me. I believe that $\ulcorner V\Vdash \phi\urcorner$ should mean that $\phi$ holds fiberwise, so I tried to express that in the internal language of the base category $\mathscr S$.

When I apply the Kripke-Joyal semantic to the above sequent then I see that it holds if and only if the pullback of $e$ along each morphism into the interpretation of $U,v:V$ is epi. That should be the same thing as $$U,v:V\Vdash \forall Z:Set.\forall f,g: Y(v)\to Z. f\circ e(v) =g\circ e(v) \to f = g$$ and hence the idempotence works out in that example. Have I done that correctly? If yes, how do I do it systematically?