Proving intuitionistic tautologies in Agda I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law
$$
((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B
$$
I understand that there is an &quot;equivalence&quot; between intuitionistic tautologies and programs and their types, that is if I manage to write a function of this type, it works like a proof of this tautology.
The type of the function is wp : {A B : Set} ((((A -&gt; B) -&gt; A) -&gt; A) -&gt; B) -&gt; B.
My question is - how do I even approach this thing? I managed to prove some other laws of intuitionistic logic, but with this one I'm kind of stuck. I imagine that somehow I'd like to get the first A -&gt; B function and apply A to it, but how can I do that if all I get is the whole function f of type ((((A -&gt; B) -&gt; A) -&gt; A) -&gt; B)? Should I use $\lambda$'s for this?
Additional question: What does this Law even mean? There are so many implications that I can't even parse it...
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.