search

hmemcpy / milewski-ctfp-pdf

Bartosz Milewski's 'Category Theory for Programmers' unofficial PDF and LaTeX source
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Other
10.84k stars 575 forks source link

Typo in section products-and-coproducts? #271

Closed technic closed 3 years ago

technic commented 3 years ago

https://github.com/hmemcpy/milewski-ctfp-pdf/blob/7de90c718518c3832484dcf24bbbe2c967a2c44c/src/content/1.5/products-and-coproducts.tex#L633-L636

Shall it be "from Either to it"?

technic commented 3 years ago

Hi, Sorry for bothering you. After more thinking a realized that there is no typo. It is funny that there was similar confusion in comments in the Bartosz blog.

Actually I think that challenge (5) makes people somewhat confused about challenge (8). Maybe it can be helpful to add some more hints/comments below.

So in (5) we use the intuitive proof by considering mapping Either -> int. We find that it is surjective (so in a sense "better") hence there is no way to invert it to obtain morphism int -> c' (for c' e.g. Either) which is required by definition of coproduct. In other words we can not construct it in a way that the factorization rule is satisfied, because information is lost.

Then in (8) we can consider

data Test a b c = Left a | Right b | Extra c

Then we shall consider morphism Test -> c' and require it to be unique for all objects c'. But for c' = Either there is not unique way to coerce Test. So here Test does not follow co-product definition.