Uniqueness of arrows between Heyting-valued sets I’m going through Goldblatt’s “Topoi”, in particular through the subchapter 11.9 on Heyting-valued sets, and it feels overly… concise. In short, I’m not sure how to prove uniqueness of arrows.
For instance, Goldblatt doesn’t explicitly define product arrows in $\Omega\textrm{-set}$ (ok, that was easy to figure out) and doesn’t show they are unique (so I have no good examples of techniques for doing so in $\Omega\textrm{-set}$), or coproducts in general (although are used in one of the exercises).
Let’s look at that last one. For coproducts I figured $\mathbf{A} + \mathbf{B}$ should probably be the set $$A + B = \{ (0, a) \mid a \in A \} \cup \{ (1, b) \mid b \in B \}$$ and the “value function”
$$
⟦ (n_1, e_1) \approx (n_2, e_2) ⟧ =
\begin{cases}
⟦ e_1 \approx e_2 ⟧, & n_1 = n_2, \\
\bot,                & \text{otherwise},
\end{cases}
$$
the intuition being the elements of the same set inheriting the same “equalness”, and the elements of different sets being as un-equal as possible.
The injections follow the similar intuition, for instance:
$$
\iota_A(a, (n, e)) =
\begin{cases}
⟦ a \approx e ⟧, & n = 0, \\
\bot,            & n = 1.
\end{cases}
$$
Then, defining $[f, g]$ for arbitrary $f \colon \mathbf{A} \rightarrow \mathbf{C}$, $g \colon \mathbf{B} \rightarrow \mathbf{C}$ by, similarly,
$$
[f, g]((0, a), c) = f(a, c) \,,
$$
$$
[f, g]((1, b), c) = g(b, c) \,.
$$
I can prove that the corresponding diagram commutes, but how do I prove that it’s the only function making it commute? That is, how do I prove this is the only $\varphi$ such that
$$
f(a, c) = \bigsqcup_{e \in A + B} \varphi(e, c) \sqcap \iota_A (a, e)
$$
(and similarly for $g$)?
I have no idea how to reason about uniqueness when the only defining condition, really, is a union over some set. So, my two general questions:

*

*How do I prove uniqueness in contexts like this? Elsewhere he asks to prove a certain construct satisfies the $\Omega$-axiom, and while I can surely prove the corresponding diagram commutes with some lattice-juggling efforts, I’m not sure how to prove uniqueness there either.

*Is there an accessible and more-detailed-than-Goldblatt’s exposition to Heyting-valued sets, so I could learn a little more? Quick Google only gives some papers about more advanced topos theory that is quite above my level.

 A: Let us unwrap the definitions: suppose we have a morphism $h \in \operatorname{Hom}(A + B, C)$ such that $h \circ \iota_A = f$ and $h \circ \iota_B = g$.  Then applying the definition of composition to the first equation, we get for each $a\in A$ and $c\in C$ that:
$$f(a, c) = \sum_{s\in A+B} h(s, c) \cdot \iota_A(a, s).$$
Now by distributivity, we can rewrite this as:
$$f(a, c) = \sum_{x \in A} h((0, x), c) \cdot \iota_A(a, (0, x)) + \sum_{y\in B} h((1, y), c) \cdot \iota_A(a, (1, y)).$$
However, in the second part of this sum, each $\iota_A(a, (1, y)) = \bot$; so only the first part of the sum matters, and we get:
$$f(a, c) = \sum_{x\in A} h((0, x), c) \cdot [a \approx x].$$
However, by the well-definedness condition of $h$, we see that for each $x\in A$, $h((0, x), c) \cdot [a \approx x] = h((0, x), c) \cdot [(0, a) \approx (0, x)] \le h((0, a), c)$.  Therefore, $f(a, c) \le h((0, a), c)$.  On the other hand, since the supremum includes the case $x = a$, we see $f(a, c) \ge h((0, a), c) \cdot [a \approx a]$.  However, by the domain condition of $h$, we get in particular that $h((0, a), c) \le [(0, a) \approx (0, a)] = [a \approx a]$, so $h((0, a), c) \cdot [a \approx a] = h((0, a), c)$.  By antisymmetry, we can now conclude that $h((0, a), c) = f(a, c)$.
A similar argument shows $h((1, b), c) = g(b, c)$ for each $b\in B, c\in C$.  Thus, we get that $h$ is uniquely determined by $f$ and $g$.
