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 "equivalence" 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 -> B) -> A) -> A) -> B) -> 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 -> 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 -> B) -> A) -> A) -> 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 -> ?)


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 -> k (λ x -> ?))


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 (λ _ -> 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.

• OK - I just didn't think of passing lambdas to the "top" function. Now that you showed the solution it does seem quite obvious :D Thanks a lot! May 19, 2021 at 21:02
• I also have a followup - how could I approach proving something called "irrefutability" that is irrefutability : {A : Set} → ¬ ¬ (A ∨ ¬ A)? Following your answer I could do something like irrefutability f = f (λ (left a) -> ? ; (right ¬a) -> ?) but having only f and a or ¬a I don't know how I can get bottom from that... May 19, 2021 at 21:44
• Are you using the interactive programming mode? f needs to be applied to an A ∨ ¬ A, not a function. So Agda will complain about type mismatches as soon as you try to do the λ expression. If you aren't, I'd recommend trying to get it set up, because immediate computer feedback is extremely helpful for this sort of thing. May 19, 2021 at 22:28
• I'm using nextjournal, so it's not really interactive - I will try to set up some interactive environment, then :3 May 20, 2021 at 6:31