1. Show that the following types are isomorphic:
* `Prod Boolean Boolean ~ Sum Boolean Boolean`
* `Prod A B ~ Prod B A`
* `Prod A (Sum B C) ~ Sum (Prod A B) (Prod A C)`
2. Some programming languages provide a “recursion combinator” `rec : {A : Set} -> (A -> A) -> A`. Show that `rec` allows the implementation of the `unsafe : {A : Set} -> A -> Void` function. Argue that, therefore, `rec` cannot be implemented in Agda.
3. Check that `\f x -> x (f x) : ((A -> B) -> A) -> (A -> B) -> B`.
**Obs:** This assignment is to be submitted as a plain text file using Agda-like syntax. It is not meant to be solved in Agda.