We consider fold-right for lists, and its static type.  The Church encoding for lists makes them into their own fold-right functions

The Church encoding represents data as their own fold-right functions.  For booleans, this means they become their own if-then-else expressions.  We consider the polymorphic type for these, which is forall X. X -> X -> X.

The Church encoding represents data as their own fold-right functions

Functional encodings take programming language features like pattern-matching and recursion and move them from outside of data to inside of data.

The idea that without lambda encodings, the current state of the art forces you to commit to a class of datatypes in the design of your type theory.

A lambda encoding is some way of representing data as functions (lambda abstractions).  Some motivations for this for computer-checked proofs and type theory.

Curry-style typing and realizability make it sensible to allow a top type to type every term, even non-normalizing ones.

Intersection types internalize the idea that a term has two types.  Curry-style typing is generally needed for this to be nontrivial.

In Curry-style typing annotations -- for example, the types of bound variables -- are erased, and not truly (semantically) part of the term.  In Church-style, they are intrinsic to the term and are truly there.  Discussion of some of the practicalities of Curry-style typing, in particular type annotations versus proving typings.

Types are specifications whose semantics is explained in terms of computation, which is thus conceptually prior.  Realizability is a way of explaining the semantics of types.