Church Encoding, Parametricity, and the Yoneda Lemma

I'm doing my masters pre-dissertation project on functorial semantics of STLC so this is super interesting! I confess, I'm coming at it from the direction of already knowing category theory, and not being super familiar with the lambda calculus, Y-combinator, System F etc. So the author's choice of what is "daunting formalism" and what is simple is opposite to what I'm familiar with. Therefore I don't really follow what's going on - but I am bookmarking it to come back to and go through at some point.