I expect this was just a mistake. Whoever wrote that (probably me) may have been thinking of the fact that, as mentioned above, the coproduct in Set is both a product and a coproduct in Rel, and mistakenly dualized it.

]]>Thank you, then I will just skip it. And thanks for the explanation above!

But I am still interested in what is the intended theorem there. If someone knows, thanks for telling me or just editing the page…

]]>Re #1: For a non-naïve set theory proof that theorem 2.8 is wrong: Rel is the Kleisli category of the power set monad, so the inclusion $\mathrm{Set}\to\mathrm{Rel}$ preserves colimits, but the product set $A\times B$ and disjoint union set $A\sqcup B$ are generally not isomorphic in Rel since they needn’t have the same cardinality (and invertible relations are functions). (That $A\sqcup B$ is also the product in Rel follows from $\operatorname{Rel}(X,A\sqcup B) \cong\operatorname{Set}(X\times (A\sqcup B),\Omega) \cong\operatorname{Set}((X\times A)\sqcup (X\times B),\Omega) \cong\operatorname{Set}(X\times A,\Omega)\times\operatorname{Set}(X\times B,\Omega) \cong\operatorname{Rel}(X,A)\times\operatorname{Rel}(X,B)$.)

The disjoint union of sets isn’t introduced until later on in the article, so I’ll just remove the mention of Rel from the theorem.

]]>If you spot typos and think you know what you are doing, then you are doing the community a favor by going ahead and fixing them. Thanks!

]]>Thanks for the quick reply and comment anyway, and thank you for teaching me to write the link.

By the way, I think I can report a typo now in a relative page allegory, in the subsection allegory#division-allegory, I saw:

That is: given $r:A\to B$ and $s:A\to C$, there exists $r/s:B\to C$ such that $t\le s/r\in hom(B,C)$…

It seems that the first $r/s$ should be $s/r$.

]]>Not to answer your question (i have never worked on or even read that page) but just to note that in order to hyperlink to an entry here, just enclose its name in double square brackets: `[[SEAR]]`

produces *SEAR*. Specifically, you are asking about this Prop..

Hm, but looking at what it says there, I agree that it *sounds* like directly contradicting both what one expects as well as what it says at *Rel* (here). Maybe a typo.

Hi, all.

I am reading the SEAR nlab page here: https://ncatlab.org/nlab/show/SEAR

Regarding Theorem 2.8, it says:

Theorem 2.8. For any sets A and B, $A\times B$ is a product of A and B in the category Set, and a coproduct in the category Rel.

and the proofs says just in naive set theory.

But the coproduct of Rel in naive set theory is the disjoint union! I am confused how can $A\times B$ can serve as the coproduct of Rel, I know that the coproduct/product in Rel is the disjoint union, but how can the cartesian product coincide with the disjoint union? Given relation $f:A\to X,g:B\to X$, how can we define the relation $A \times B \to X$ so it is a coproduct?

I assume the inclusion relations $A\to A \times B$ and $B\to A\times B$ is $(a,(a1,b1))$ holds iff $a = a1$, and $(b,(a1,b1))$ holds iff $b = b1$. I may also make mistake here but I still wonder what else could it be.

Thank you for any explaination! (and sorry if it turns out to be a stupid question…)

]]>