Comment by _a_a_a_

Accessible for who, do you mean? That is in no way 'accessible' without solid exposure to quite a lot of discrete maths (which I have and it's still hard going).

λf :(τ 1 × τ 2 ) → τ 3 .λx:τ 1 .λy:τ 2 .f (x,y) has type ((τ 1 × τ 2 ) → τ 3 ) → (τ 1 → τ 2 → τ 3 ).

Yeah, that's accessible.