>we have the identity function of type A → A (which reads a value as input and outputs the same value)

That only exists in theoretical computer science. In real computer programming, you always have some bounds to the value of A.

I think it is time to repost Against Curry-Howard Mysticism (https://liamoc.net/forest/loc-000S/index.xml)