## Example

## Intuition

The categorical product of two types **A** and **B** should contain the minimal information necessary to contain inside an instance of type **A** or type **B**. We can see now that the intuitive coproduct of two types should be `Either a b`

. Other candidates, such as `Either a (b,Bool)`

, would contain a part of unnecessary information, and they wouldn't be minimal.

The formal definition is derived from the categorical definition of coproduct.

## Categorical coproducts

A categorical coproduct is the dual notion of a categorical product. It is obtained directly by reversing all the arrows in the definition of the product. The coproduct of two objects **X**,**Y** is another object **Z** with two inclusions: **i_1: X → Z** and **i_2: Y → Z**; such that any other two morphisms from **X** and **Y** to another object decompose uniquely through those inclusions. In other words, if there are two morphisms **f₁ : X → W** and **f₂ : Y → W**, exists a unique morphism **g : Z → W** such that **g ○ i₁ = f₁** and **g ○ i₂ = f₂**

## Coproducts in Hask

The translation into the **Hask** category is similar to the translation of the product:

```
-- if there are two functions
f1 :: A -> W
f2 :: B -> W
-- and we have a coproduct with two inclusions
i1 :: A -> Z
i2 :: B -> Z
-- we can construct a unique function
g :: Z -> W
-- such that the other two functions decompose using g
g . i1 == f1
g . i2 == f2
```

The coproduct type of two types `A`

and `B`

in **Hask** is `Either a b`

or any other type isomorphic to it:

```
-- Coproduct
-- The two inclusions are Left and Right
data Either a b = Left a | Right b
-- If we have those functions, we can decompose them through the coproduct
decompose :: (A -> W) -> (B -> W) -> (Either A B -> W)
decompose f1 f2 (Left x) = f1 x
decompose f1 f2 (Right y) = f2 y
```