<p>Here is a proof that this is not a research question. It can be solved by a <em>machine</em>:</p>

<pre><code>Welcome to Djinn version 2011-07-23.
Type :h to get help.
Djinn&gt; f ? (a, Either b c) -&gt; Either (a,b) (a,c)
f :: (a, Either b c) -&gt; Either (a, b) (a, c)
f (a, b) =
    case b of
    Left c -&gt; Left (a, c)
    Right d -&gt; Right (a, d)
</code></pre>

CC BY-SA 3.0
2011-11-19T17:37:30.803Z
To be fair, the version number indicates solving it by machine would count as a valid research question :-).
Rob Simmons
CC BY-SA 3.0
2011-11-19T19:19:45.810Z
I am pretty sure even very early versions of Djinn could solve this one.
Andrej Bauer
CC BY-SA 3.0
2011-11-19T09:32:26.107Z
2011-11-19T09:32:26.107Z
Andrej Bauer
<p>$ A \times \left ( B + C \right ) $ is isomorphic to $ \left ( A \times B \right ) + \left ( A \times C \right ) $, right? That means there's a function from one to the other and another function back. But what are those functions? Furthest I got was $ \left &lt; \mathrm { p } _ 0 , ( \mathrm { id } + \mathrm { id } ) \circ \mathrm { p } _ 1 \right &gt; $ but that's just equal to $ \mathrm { id } _ { A \times \left ( B + C \right ) } $.</p>

CC BY-SA 3.0
2011-11-18T23:35:12.957Z
Is this homework?
Radu GRIGore
CC BY-SA 3.0
2011-11-20T12:53:20.103Z
You can ask elementary questions in computer science on http://math.stackexchange.com/ .
beroal
<functional-programming><ct.category-theory>
What function has the signature $ A \times \left ( B + C \right ) \rightarrow \left ( A \times B \right ) + \left ( A \times C \right ) $?
Fox
# What function has the signature $ A \times \left ( B + C \right ) \rightarrow \left ( A \times B \right ) + \left ( A \times C \right ) $?

(Asked by: username_0 on 2011-11-18)

$ A \times \left ( B + C \right ) $ is isomorphic to $ \left ( A \times B \right ) + \left ( A \times C \right ) $, right? That means there's a function from one to the other and another function back. But what are those functions? Furthest I got was $ \left < \mathrm { p } \_ 0 , ( \mathrm { id } + \mathrm { id } ) \circ \mathrm { p } \_ 1 \right > $ but that's just equal to $ \mathrm { id } \_ { A \times \left ( B + C \right ) } $.

**Tags:** functional-programming, ct.category-theory

> **Comments:**
> **username_1**: Is this homework?  
> **username_2**: You can ask elementary questions in computer science on http://math.stackexchange.com/ .  

---

## 1 answers

### Answer by username_3 on 2011-11-19. Score: 11

Here is a proof that this is not a research question. It can be solved by a machine:
Welcome to Djinn version 2011-07-23.
Type :h to get help.
Djinn> f ? (a, Either b c) -> Either (a,b) (a,c)
f :: (a, Either b c) -> Either (a, b) (a, c)
f (a, b) =
    case b of
    Left c -> Left (a, c)
    Right d -> Right (a, d)

> **Comments:**
> **username_4**: To be fair, the version number indicates solving it by machine would count as a valid research question :-).  
> **username_3**: I am pretty sure even very early versions of Djinn could solve this one.  

---

