[TYPES] [newbie] is {initial, terminal} object the identity for {coproduct, product}?

[wagnerdm@seas.upenn.edu]

Quoting Larry Evans <cppljevans at suddenlink.net>:

> Define + as the coproduct operator,
>   IOW, X+Y is the coproduct of X and Y for some category C.
> Define * as the product operator,
>   IOW  X*Y is the product of X and Y for some category C.
> Define 0 as the initial object of C.
> Define 1 as the terminal object of C.

Being completely careful here, we must observe that if we view + as an  
operator, then X+Y is merely picking out one of many possible  
coproducts of X and Y. (Of course, any other coproducts that exist are  
isomorphic.) We must make a similar caveat for *, 0, and 1 (which are  
particular initial and terminal objects, though again unique up to  
isomorphism).

> Is it true that, for all objects, X in C:
>
>   X+0 = X
>   0+X = X
>   X*1 = X
>   1*X = X

Then, here, we must take equality as isomorphism, of course. It's  
pretty straightforward to show that X is *a* coproduct of X and 0 --  
just take id : X -> X and the unique arrow i : 0 -> X as the  
injections. Therefore X is isomorphic to whatever object X+0 happens  
to be. The remaining equations follow by symmetry and duality.

> Also, what's X*0 and X+1?

I wasn't able to come up with a more edifying description of these  
objects than simply expanding the definitions. Perhaps somebody else  
can come up with some further property of X*0/X+1 or show that there  
isn't anything additional we can assume...?

~d