1. In the standard library I cannot fine equality, negation, logical
or, logical and...
Where are they?
2. How can I translate in Agda the following Coq type?
forall (A:Set), (forall (x y:A), {x=y}+{x<>y}) -> nat
3. How do you deal with proof irrelevance in Agda?