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