程序代写代做代考 Agda 1. Show that the following types are isomorphic:

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.