I started doing the exercises from a Homotopy Type Theory intoduction class by Thorsten Altenkirch. The first one is very simple, you just have to prove some logical propositions by mapping them to types and finding an element of the associated type for each proposition. I had some problems with the ones involving negation, which is mapped to the type $A \to 0$. I don't really get what does it mean to construct a function that computes the empty type.
So, i think i managed to do this: $$\lnot (P \lor Q) \Leftrightarrow \lnot P \land \lnot Q $$ which is mapped to $$((P+Q \to 0) \to ((P \to 0) \times (Q \to 0)))\times (((P \to 0) \times (Q \to 0)) \to (P+Q \to 0))$$ An element of this is a pair of functions. The first one can be defined as $f: \equiv \lambda h.(h\; inl, h\; inr)$, for $h:P+Q \to 0$ and $inl:P\to P+Q, inr:Q\to P+Q$ the known injection functions.
The second, let's call it g, as $(g\, m)\,(inl\, p) : \equiv pr_1\, m\, p$ and $(g\, m)\,(inr\, q) : \equiv pr_2\, m\, q$, for $m: (P \to 0)\times (Q\to 0)$ and the known projection functions. (How would i use lambdas to define g, or any branching function?)
So, the next two examples had me stuck, and i'm not even sure that they can be solved:
1) $\lnot (P \land Q) \Leftrightarrow \lnot P \lor \lnot Q $
2)$\lnot(P \Leftrightarrow \lnot P)$
If they can be solved can you give me a proof, or some hints based on my proof above? (if it is correct that is). If not can you prove how they can't? And also some motivation for negation in constructive mathematics would help me.
In comments to another of your questions, I suggested that you learn the basics of Agda, to the point that you can do these types of exercises in it. I specifically recommend Agda as opposed to Coq because it's easier to see what's going on in Agda. In Coq you write a program (called a proof script) to produce a proof term. In Agda, you just directly write the proof term, and it directly corresponds to what's being written in the HoTT book. Indeed, you should just start doing the exercises of the HoTT book in Agda. For the content of the first chapter, there should be no difficulties. You do not need to use or learn anything about the Agda standard library. If you've never programmed before, this will take a lot of effort, but, again, there's close to a one-to-one correspondence between the language of the HoTT book and the language of Agda. The point being that 1) that effort is for the most part directly relevant to understanding the concepts in HoTT, and 2) if you can't formulate and solve the problem in Agda, then you probably don't understand what's going on in HoTT, at least and especially for the basics. Finally, if you've never programmed before, one thing you have to get used to is being constantly told you're wrong by the compiler/type checker. Indeed, that's why I'm suggesting that you learn and use Agda; it will not let you trick yourself into thinking you understand something when you don't, but also it lets you play around and experiment and it lets you know when you're right.
At any rate, here are Agda programs, intentionally without explanation, that correspond to proofs of the above statements.
thm1corresponding to statement (1) is incomplete as indicated by the question mark. (You can load the code into Agda, and it will tell you what type of term is expected for the question mark; the question mark is part of Agda syntax.) You should get to where you can understand what these programs are doing, or, alternatively, produce your own programs for these types. I don't expect it to be at all obvious what's going on if you have no experience with Agda or a similar language.