{{ message }}

forked from gfjaru/Kiko

# [curry-howard] Re: unicity of arrows #1

Closed
opened this issue Feb 7, 2019 · 3 comments
Closed

# [curry-howard] Re: unicity of arrows#1

opened this issue Feb 7, 2019 · 3 comments

### glmxndr commented Feb 7, 2019

 Hi, nice blog post. Two nitpicks though. Similarly to the step before, by definition of product, since we know (A × B) × C is a product of A × B and C, and since we have the arrows l : T → A × B and q' ∘ q ∘ t : T → C, then there must exist an unique arrow t' : (A × B) × C. Nitpick 1: t' should probably be a T -> (AxB)xC since it is called an arrow. Nitpick 2: t' is not necessarily unique: there are as many arrows from T to (AxB)xC as there are members of this object. There is only one that makes some diagram (involving t) commute, though. I get what you meant but the wording is maybe a bit misleading to category theory newcomers. The text was updated successfully, but these errors were encountered:

### BartoszMilewski commented Feb 7, 2019

 Nitpick 1: You are correct. Nitpick 2: There is a unique arrow that factorizes the two arrows l and the other, q' ∘ q ∘ t, which should probably be given a name too. You're right that there are as many arrows from T to (AxB)xC as there are elements in it, but that might be zero. It would be the case if, for instance, C were empty. But then Ax(BxC) would be empty too, and we wouldn't have the starting arrow for the proof.

### vladciobanu commented Feb 7, 2019 • edited

 Thank you for your comments! Indeed, 1 is absolutely correct. Would you agree with the statement that `t'` is the unique arrow `T -> (A x B) x C` that can be derived from the initial arrow `t : T -> A x (B x C)`?

### BartoszMilewski commented Feb 7, 2019

 I think you should modify the definition of the product. There exist a unique arrow m such that p . m = p' and q . m = q'.
closed this in ``` 0d89dc8 ``` Feb 7, 2019
added a commit that referenced this issue Feb 7, 2019
``` Fix #1 ```
``` e1a0b4a ```