It's about Excercise 2 from here:
While the principle of excluded middle $P\vee\neg P$ ( tertium non datur) is not provable, prove its double negation using the propositions as types translation:
$\neg\neg (P\vee \neg P)$.
If for a particular proposition $P$ we can establish $P\vee\neg P$ then we can also derive the principle of indirect proof (reduction ad absurdo) for the same proposition $\neg\neg P\implies P$. Hence show:
$(P\vee\neg P)\implies (\neg\neg P \implies P)$
However, the converse does not hold (what would be a counterexample?). However, use the two tautologies to show that the two principles are equivalent.
For the first part, $\neg\neg (P\vee \neg P)$ unfolds for me as
$ f:((P+(P\to 0))\to 0)\to 0 $
and I'm not sure how to proceed, i.e. how to construct witness $f$ (or should it ever be constructed since we are aiming at empty type).
For the second part- $(P\vee\neg P)\implies (\neg\neg P \implies P)$- I derive
$ f:(P+(P\to 0))\to (((P\to 0)\to 0)\to P) $
and assuming $h:(P\to 0)\to 0$ and $a:P\to 0$ I'm trying something like that:
$ (f\;left\;p)h=\;...\;? $
$ (f\;right\;a)h=h(a)\;...\;? $
I also don't understand last paragraph of the exercise, namely that converse does not hold, but nevertheless the principles are equivalent. My understanding is that equivalence($\iff$) would mean that the converse ($\impliedby $) follows.
By the way, do you have some materials on the subject to recommend, exercises as the above, from simple to harder ones, with a lot of examples or explanation so I don't get stuck again and can develop more intuition? The materials I have found so far are vestigial in amount of such basic examples/exercises or feel like pro level for me with little or no explanation... Maybe my problem is that I skipped some prerequisites on which homotopy type theory is based and those topics would be richer in what I expect. Nonetheless I'm not sure what to google to find those topics...
For the first part, you don't have a lot of choices in your strategy. You want: $$f : ¬(P ∨ ¬P) → 0$$ so your only option is to define a function: $$f\ (e : (P ∨ ¬P) → 0) = ...$$
Now you have no way of producing a value of $0$ but calling $e$: $$f\ e = e (...)$$ and you must supply a value of $P ∨ ¬P$, but you have no value of $P$, so you must try the right option: $$f\ e = e(\mathsf{right} (λ p →\ ...))$$
Now you are again in a situation where you must provide a value of $0$, but this time you have a value of $P$.
The second problem doesn't have many degrees of freedom either. One thing to keep in mind is that there is a function with type $0 → P$
The bit about the converse is perhaps a bit cryptic. When it says that the principles are equivalent, it means that e.g. assuming the axiom $$\mathsf{lem} : \prod_{P : \mathsf{Prop}_\mathcal{U}} P ∨ ¬ P$$ is equivalent to assuming the axiom $$\mathsf{dne} : \prod_{P : \mathsf{Prop}_\mathcal{U}} ¬¬P → P$$
The reason for this is that above we exhibited $$¬¬(P ∨ ¬P)$$ for arbitrary $P$, and $\mathsf{dne}$ allows the double negation to be eliminated. However, that uses double negation elimination for $$P ∨ ¬P : \mathsf{Prop}_\mathcal{U}$$ not for $P$. I think you'll find that double negation elimination at $P$ is insufficient to prove excluded middle at $P$, which is the converse formula they were referring to. I believe they are asking you (parenthetically) to think of an example of a type $P$ for which $\mathsf{dne}\ P$ holds, but $\mathsf{lem}\ P$ does not.
As for resources, I don't have any books or anything to recommend. One thing you might want to look into, though, is trying out a computerized proof assistant like Agda (or Lean, or ...) if you haven't. Using something like that, it is very natural to have the system guide you through the sort of steps I went through in the first part. You can incrementally refine your definition, and it will show you your options at each step, and there is even an analogue of the '$...$' written in each step.
Working in such an environment can make it easier to be confident that an approach is correct or not for these sorts of problems, and aid building intuition that is necessary for similar confidence in a 'pen and paper' scenario (where you must check things that the computer would check).