xacid

I still don't see what's wrong with notation. Let's focus on paper:

There is an isomorphism between the types of fac, the factorial function in CPS style, and the direct factorial function of type Nat -> Nat. Applying the identity function is one direction of the isomorphism, from CPS to direct style.

The factorial isomorphism is an instance of the isomorphism of the types A -> B and

∀X : (B -> X) -> (A -> X).

The covariant homfunctor for a fixed object A is C(A, -) : C -> Set,
with the action on arrows given by C(A, f ) h = f . h

The functor C(A, -) maps an object B to the set of arrows from a fixed A to B,
and it takes an arrow f : C(X, Y ) to a function.

C(A, f ) : C(A, X) -> C(A, Y ).

Conversely, C(-. B) : C op -> Set is a covariant functor defined C(f, B) h = h . f

Let us continue by transliterating the CPS isomorphism into more categorical language,

C(A, B) = ∀X : C(B, X) -> C(A, X)

We can continue generalizing by extracting out the covariant homfunctor C(A, - ) and naming it H.

HB = ∀X : C(B, X) -> HX

The covariant hom-functor has type C -> Set, and in one final abstraction we can let H : C -> Set be any set-valued functor.

The isomorphism we have arrived at is a statement of the Yoneda lemma.