Assignment 2

1. Write Agda functions that convert between Prod Boolean Boolean and Sum Boolean Boolean. [2.5 pts]
2. Supposed that we have conversion functions f : A1 -> A2 and f' : A2 -> A1 and, respectively, g : B1 -> B2 and g' : B2 -> B1. Construct conversion functions
   • between Sum A1 B1 and Sum A2 B2 [2.5 pts]
   • between Prod A1 B1 and Prod A2 B2. [2.5 pts]
   • define functions of type (A1 -> A2) -> (B1 -> B2) -> (Sum A1 B1) -> (Sum A2 B2) and (A2 -> A1) -> (B2 -> B1) -> (Sum A2 B2) -> (Sum A1 B1) and , respectively, (A1 -> A2) -> (B1 -> B2) -> (Prod A1 B1) -> (Prod A2 B2) and (A2 -> A1) -> (B2 -> B1) -> (Prod A2 B2) -> (Prod A1 B1) which produce the functions above. [2.5 pts]
3. Write Agda proof (terms) for [2.5 pts]
   • (A1 -> A2) -> (B1 -> B2) -> (A1 or B1) -> (A2 or B2)
   • (A1 -> A2) -> (B1 -> B2) -> (A1 and B1) -> (A2 and B2)

Write the proofs for the following propositions in Agda:

R -> (not Q -> S) -> (Q and R -> not R) -> S
(not P or Q) -> not (P and not Q)