Recursive type encoding on System F (and other pure type systems)
There is a convention in category theory that the same symbol is used for a type constructor and the map function over that type constructor. Hence, if f : X -> Y then F f : F X -> F Y.