Posted on 2015-09-15
by Oleg Grenrus

### The Question

We know that `forall a. a -> a`

has only one element: `id = \x -> x`

. How to show it for more complicated type, like: `(b -> a) -> (a -> b -> c) -> b -> c`

### The answer

- You can apply sequent calculus
- Or you can use
`Yoneda lemma`

-approach with smart choices of functors.

Read rest the rest on StackOverflow

Site proudly generated by Hakyll