I'm following Goldbaltt's Topoi: The categorial analysis of logic. I use this book's notation, but it is quite standard.
At some point, he defines disjunction as the morphism
$$\curlyvee:\Omega\times\Omega\longrightarrow\Omega$$
which is the character of the image of the morphism
$$w=[\langle\top_\Omega,\mathbf{1}_{\Omega}\rangle,\langle\mathbf{1}_\Omega,\top_\Omega\rangle]:\Omega+\Omega\longrightarrow\Omega\times\Omega$$
Using the epi-mono factorization
$$w=\text{im}(w)w^*:\Omega+\Omega\to w(\Omega+\Omega)\to\Omega\times\Omega$$
I have managed to prove that
$$\top\curlyvee\top = \curlyvee\langle\top,\top\rangle=\curlyvee\langle\top !_\Omega\top,\mathbf{1}_\Omega\top\rangle=\curlyvee\langle\top !_\Omega,\mathbf{1}_\Omega\rangle\top=\curlyvee wi_1\top=$$
$$=\curlyvee\text{im}(w)w^*i_1\top=\top!_{w(\Omega+\Omega)}w^*i_1\top=\top!_{\Omega+\Omega}i_1\top=\top !_\Omega\top=\top$$
And similary, using $\curlyvee\text{im}(w)w^*i_1\bot$ and $\curlyvee\text{im}(w)w^*i_2\bot$ it can be proven that
$$\top\curlyvee\bot=\bot\curlyvee\top = \top$$
I'm having lots of trouble proving that $\bot\curlyvee\bot = \bot$.
Goldblatt himself leaves this unproven until much later in the book, after he has developed other tools to work with truth values. However I would like a diagram-chasing proof that doesn't require introducing new definitions and lemmas.
I've already tried many things (and failed): trying to replicate a proof from the topos of sets, trying to use the universal property of the image of $w$ together with the $\Omega$-axiom…
Whatever I try, I can't complete the diagram with the key morphism.
Is it possible to find the proof I'm looking for?
Thanks in advance!
Best Answer
Unfortunately, I was not able to find a direct series of computations as you were asking for. However, I did find an argument that hopefully is reasonably elementary.
First, considering the monomorphism $(\bot, \bot) : 1 \to \Omega \times \Omega$, observe that since $(\bot_\Omega, 1_\Omega) : \Omega \to \Omega \times \Omega$ is the pullback of $\bot : 1 \to \Omega$ along $\pi_1 : \Omega\times\Omega \to \Omega$, we have $$\chi_{(\bot,\bot)} \circ (\top_\Omega, 1_\Omega) \le \chi_{(\bot_\Omega, 1_\Omega)} \circ (\top_\Omega, 1_\Omega) = \chi_\bot \circ \pi_1 \circ (\top_\Omega, 1_\Omega) = \chi_\bot \circ \top \circ {!}_\Omega = \bot !_\Omega.$$ Now, since $\bot !_\Omega$ is the minimum element of $\operatorname{Hom}(\Omega, \Omega)$, we conclude that $\chi_{(\bot,\bot)} \circ (\top_\Omega, 1_\Omega) = \bot !_\Omega$. A similar argument, using $\pi_2$ in place of $\pi_1$, shows that $\chi_{(\bot,\bot)} \circ (1_\Omega, \top_\Omega) = \bot !_\Omega$ also. Therefore, $\chi_{(\bot,\bot)} \circ w = \bot !_{\Omega+\Omega}$.
Now, since $\bar w$ is an epimorphism, we get that $\chi_{(\bot,\bot)} \circ \operatorname{im} (w) = \bot !_{w(\Omega\times\Omega)}$. As a result, we have a pullback diagram $$\require{AMScd}\begin{CD} 0 @>>> w(\Omega\times\Omega) \\ @VVV @VV \operatorname{im}(w) V \\ 1 @> (\bot,\bot) >> \Omega\times\Omega. \end{CD}$$ Now flipping this diagram and reading it the other way, we can conclude that $\curlyvee \circ (\bot,\bot) = \chi_{\operatorname{im}(w)} \circ (\bot,\bot) = \bot$.