Proving intuitionistic tautologies in Agda
For examples like this, they can often by easily written interactively just looking for the only thing possible to do at each stage. So for instance, you start with:
wp e = ?

and the only option is to apply e, at which point Agda will tell you you need to provide $((A → B) → A) → A$, so you introduce a lambda:
wp e = e (λ k -&gt; ?)

Now you need to give an A, which is the result type of k, so you apply k and abstract again:
wp e = e (λ k -&gt; k (λ x -&gt; ?))

Now you need to give a B. The only thing that results in a B is e, so you apply it again. However, now your situation is different, because x is in scope. And presumably you don't want to follow the same pattern as you did before, so you can write:
wp e = e λ k → k (λ x → e (λ _ -&gt; x))

In this case, the process is constrained enough that the auto-solver comes up with this solution.
As for what the type means, Peirce's law is similar to double-negation elimination with the $⊥$ replaced with $B$: $$((A → B) → B) → A$$ Peirce's law follows from the above type, because you can massage an $(A → B) → A$ into an $(A → B) → B$ by duplicating the function argument.
So, your overall type can be read as similar to:
$$¬¬(¬¬A → A)$$
Which fits the theme of double-negated classical (propositional) theorems being intuitionistic theorems.