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](https://arxiv.org/abs/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?



The idempotence of Mike Shulman's "Stack semantics"
The stack semantics as described in that paper doesn't involve any type theory, only the first-order language of categories. Writing $\ulcorner V \Vdash \phi \urcorner$ means to write out the definition of $\Vdash$, which is by induction over the structure of $\phi$. In your example, to say that


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


means, by definition of $\Vdash$, to say that



> 
> For any $p:W\to V$, any $Z \in \mathcal{S}/W$, and any $f,g : p^\*Y \to Z$ over $W$, if $f\circ p^\*e = g \circ p^\*e$ then $f=g$.
> 
> 
> 


(Strictly speaking, we should pass to a new $W,p$ with each universal quantifier or implication, but we can combine them all.) Thus,


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


means


$$U \Vdash \forall W.\forall p:W\to V. \forall Z. \forall q:Z\to W. \forall f,g: p^\*Y\to Z. f\circ p^\*e = g\circ p^\*e \to f = g.
$$


only even more verbose, because we have to write out the meaning of "$p^\*$" and the fact that $f,g$ are morphisms over $W$.


