This explanation is useless imo because it expects the reader to already understand the weirdest part:

"If I have a function A -> B, how could I possibly get something that goes in the direction F B -> F A out of it?"

The answer to this is: given e.g. a function that accepts a B, i.e. `B -> ...` you can compose it with `A -> B` on the _input side_, to get a function that accepts an A, i.e. `A -> B` (+) `B -> ...` = `A -> ...`.

Once you've managed to get that across, you can start talking about contravariant functors. But expecting people to just intuit that from the condensed type signature is pedagogical nonsense.

Saying without examples is a pedagogical nonsense, I can't argue, because I agree.

But if I provide the two typical examples Hom(A,) and Home(,A) and how they transport the arrows it starts to click.

There is also List which is a covariant functor. The stupid Home(unit,) which is the "identity" functor.

I could also add Hom(Bool,) which is the pair functor, ie Hom(Bool,A) is a tuple in AxA. A->AxA (or A->Him(Bool, A)) is a covariant functor.

Etc. Examples are the keys to understand the idea.

In my simple language, `F` is that context. And (A->B) is a single-argument function.

   // Int -> Float
   oneArgFn(x) = x + 1.1

   // List of Int -> List of Float
   ctxOneArgFn(xs) = ListFunctor(oneArgFn, xs) //ie., map()

Single-argument doesn't capture the difference between functor and applicative.

  ex1 :: Functor f => f (Int, Int) -> f Int
  ex1 = map (uncurry (+))

Applies a multi-argument function within a functor. What applicative allows you do is take a product of contexts to a context of products, and lift a value to a context.

  pure :: a -> f a
  zip :: (Applicative f) => (f a, f b) -> f (a, b)

This can then be used to make ex1 into a multi-argument function of contexts, which is not the same as (uncurry (+)) being a multi-argument function

  ex2 :: (Functor f) => (f Int, f Int) -> f Int
  ex2 = ex1 . zip

Sure, it's a particular interpretation of `(f a, f b) -> f (a, b)`

    (a, b) is an a -> b
    (f a, f b) is an f a -> f b

Applicative, over an above this, is really just useful when you have (f a, f b, f c, ..)

You're just reducing my idea to a specific case. You missed the generalized idea.

Send a PR to fix it!

There are so many things to fix. And they should have use coq as default language.