<p>Take a type theory of your choice (perhaps System Fω).
Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic function. </p>

<p>What is the counter-example? </p>

CC BY-SA 4.0
2019-01-29T07:44:03.097Z
What is the $\mathsf{Type}$ category? (Make sure you explain exactly how equality of morphisms is supposed to work, please.)
Andrej Bauer
CC BY-SA 4.0
2019-01-29T15:28:32.763Z
@AndrejBauer, Thank you for pointing out that choice of equality is relevant, I have not appreciated it. This remark alone is helpful as I see that this is essential in the definition of the natural transformation. I know the standard options are $\beta$ and $\beta\eta$ equalities. Are there others? Can/should we stipulate that isomorphic types are equal even if we can't prove it internally? I can't phantom what would be the effect. If I must choose one I'd like to focus on $\beta\eta$ equality.
Łukasz Lew
CC BY-SA 4.0
2019-01-29T15:31:29.307Z
This question has 3 votes to be closed, yet no comment explaining why or how it can be improved. The question is important to me and I'm keen to improve it if it is not clear.
Łukasz Lew
CC BY-SA 4.0
2019-01-29T22:54:01.167Z
There *is* a suggestion, namely that you explain what the $\mathrm{Type}$ category is. You have not done so. And please put the explanation in the main text, not the comments. I think you will discover that you do not know what the category is. I would also like to see a reference to the claim that "Parametric functions are known to be natural transformations in $\mathrm{Type}$ category" because it's not clear what that is supposed to mean.
Andrej Bauer
CC BY-SA 4.0
2019-01-30T14:52:16.883Z
Maybe "Normal Forms and Cut-Free Proofs as Natural Transformations", but it's dinatural, not natural.
xavierm02
<type-theory><ct.category-theory>
What's the example of natural transformation in 'Type" that is not a parametric function?
Łukasz Lew
# What's the example of natural transformation in 'Type" that is not a parametric function?

(Asked by: username_0 on 2019-01-29)

Take a type theory of your choice (perhaps System Fω).
Parametric functions are known to be natural transformations in 'Type' category. Yet not every natural transformation in 'Type' is a polymorphic function.

What is the counter-example?

**Tags:** type-theory, ct.category-theory
> **Comments:**
> **username_1**: What is the $\mathsf{Type}$ category? (Make sure you explain exactly how equality of morphisms is supposed to work, please.)  
> **username_0**: @AndrejBauer, Thank you for pointing out that choice of equality is relevant, I have not appreciated it. This remark alone is helpful as I see that this is essential in the definition of the natural transformation. I know the standard options are $\beta$ and $\beta\eta$ equalities. Are there others? Can/should we stipulate that isomorphic types are equal even if we can't prove it internally? I can't phantom what would be the effect. If I must choose one I'd like to focus on $\beta\eta$ equality.  
> **username_0**: This question has 3 votes to be closed, yet no comment explaining why or how it can be improved. The question is important to me and I'm keen to improve it if it is not clear.  
> **username_1**: There *is* a suggestion, namely that you explain what the $\mathrm{Type}$ category is. You have not done so. And please put the explanation in the main text, not the comments. I think you will discover that you do not know what the category is. I would also like to see a reference to the claim that "Parametric functions are known to be natural transformations in $\mathrm{Type}$ category" because it's not clear what that is supposed to mean.  
> **username_2**: Maybe "Normal Forms and Cut-Free Proofs as Natural Transformations", but it's dinatural, not natural.  

---

## 0 answers

