# Internal Union Arrows In A Topos

Below I describe an internal intersection arrow in a topos. My main question is, is there a corresponding idea of an internal union arrow, and if so what is the definition of it ?

Pointers to literature would also be helpful. I did see that

https://ncatlab.org/toddtrimble/published/An+elementary+approach+to+elementary+topos+theory

refers to an internal join arrow (which is probably what I want), but Todd Trimble does not seem to elaborate about it.

I learnt about internal intersection arrows from Exercise 13.9 of Elementary Categories, Elementary Toposes (by Colin Mclarty), but I am also unsure of their exact nature. I paraphrase this exercise below, in the hope that somebody can tell me exactly how internal intersection arrows are defined too (feel free to use the Mitchell–Bénabou language if it helps):

For an object $$A,$$ in a topos with subobject classifier $$\Omega,$$ we write $$x \in^A p$$ to denote that that pair $$\langle p,x \rangle$$ is a member of the subobject classified by the exponential evaluation arrow $$\Omega ^A \times A\overset{e}{\rightarrow} \Omega.$$ Mclarty asks us to define an internal intersection arrow

$$\Omega ^{\Omega ^A} \overset{\cap}{\rightarrow} \Omega ^A$$

and he tells us that $$\cap$$ is the exponential transpose of the arrow

$$\Omega ^{\Omega ^A} \times A \overset{}{\rightarrow} \Omega$$

which takes a pair $$\langle s, x \rangle$$ to true if and only if for every

$$p \in^{\Omega ^A} s$$

we have $$x \in^A p.$$

• If you're comfortable with the Mitchell-Benabou language, then I'm not sure what more there is to do; it's just defined in the internal language like it would be set-theoretically. So I'm guessing you'd actually prefer a pure arrows version? – Malice Vidrine Feb 6 at 23:01
• I think I've used the Mitchell-Benabou language to get at the internal intersection arrow, but I'm not sure, so I would appreciate seeing a pure arrow version. But the main thing I'm hoping for is some sort of description of the internal union arrow. – Richard Southwell Feb 6 at 23:34
• It is probably described in Goldblatt's Topoi. – Berci Feb 6 at 23:45
• Maybe, but I have looked at bit, and not seen it yet. – Richard Southwell Feb 6 at 23:52

For an object $$A$$, we can form the subobject $$\pi_{1,2}^*(\in^{\Omega^A})\wedge\pi_{2,3}^*(\in^{A})\hookrightarrow\Omega^{\Omega^A}\times\Omega^A\times A\qquad (1)$$ by taking the meet of the subobjects obtained by pulling back $$\in^{\Omega^A}$$ and $$\in^A$$ along the relevant product projections. Then $$\exists_{\pi_{1,3}}(\pi_{1,2}^*(\in^{\Omega^A})\wedge\pi_{2,3}^*(\in^{A}))\hookrightarrow\Omega^{\Omega^A}\times A\qquad (2)$$ is the image of the composition of the inclusion in (1) with the projection $$\pi_{1,3}:\Omega^{\Omega^A}\times\Omega^A\times A\to\Omega^{\Omega^A}\times A$$. Intuitively, (2) is the extension of the predicate $$\exists P(a\in P\wedge P\in X)$$; i.e. all the $$\langle a,X\rangle$$ in the image of the map that deletes the middle term from $$\langle a,P,X\rangle$$ with $$a\in P\in X$$.
The subobject in (2) has a classifying map; call it $$U:\Omega^{\Omega^A}\times A\to \Omega$$. Then, as with the intersection map, the union map $$\bigvee:\Omega^{\Omega^A}\to\Omega^A$$ is obtained by taking the exponential transpose of $$U$$.
The only difference between this map and the intersection map is whether you're using the left or right adjoint to $$\pi_{1,3}^*:\mathrm{Sub}(\Omega^{\Omega^A}\times A)\to\mathrm{Sub}(\Omega^{\Omega^A}\times\Omega^A\times A)$$ in going from (1) to (2); they each give a different subobject of $$\Omega^{\Omega^A}\times A$$, and so a different classifying arrow to take the transpose of in the last step.