The idempotence of Mike Shulman's "Stack semantics"

Question

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?

Answer 1

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$.