Comment by moomin

Probably not, but since no-one else is having a go, I will: f is “Functor”, which means roughly the same thing as in category theory (but restricted to the domain of Haskell types). I’m guessing it’s possible to construct a Provability functor.

-> in Haskell is just a function. I’ll mention that types and propositions have a structure preserving isomorphism. So “a” is an arbitrary type but you can think of it as an arbitrary proposition.

But equally, this holds true for all Functors, so we can specialise the function to something like

(List (List Int -> Int) -> List Int

I hope this helps, it might not.