# 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)`
## Submission instructions : http://bit.ly/2SM4bPh
## Solutions
https://bit.ly/2XT7OXI
“`
eq1to : Prod Boolean Boolean -> Sum Boolean Boolean
eq1to (pair true true) = left true
eq1to (pair true false) = left false
eq1to (pair false true) = right true
eq1to (pair false false) = right false
eq1from : Sum Boolean Boolean -> Prod Boolean Boolean
eq1from (left true) = pair true true
eq1from (left false) = pair true false
eq1from (right true) = pair false true
eq1from (right false) = pair false false
eq2ato : {A1 A2 B1 B2 : Set} -> Sum A1 B1 -> Sum A2 B2
eq2ato (left a1) = left (f a1)
eq2ato (right b1) = right (g b1)
eq2afrom : {A1 A2 B1 B2 : Set} -> Sum A2 B2 -> Sum A1 B1
eq2afrom (left a2) = left (f’ a2)
eq2afrom (right b2) = right (g’ b2)
eq2bto : {A1 A2 B1 B2 : Set} -> Prod A1 B1 -> Prod A2 B2
eq2bto (pair a1 b1) = pair (f a1) (g b1)
eq2bfrom : {A1 A2 B1 B2 : Set} -> Prod A2 B2 -> Prod A1 B1
eq2bfrom (pair a2 b2) = pair (f’ a2) (g’ b2)
eq2c1 : {A1 A2 B1 B2 : Set} -> (A1 -> A2) -> (B1 -> B2) -> (Sum A1 B1) -> (Sum A2 B2)
eq2c1 f g (left a1) = left (f a1)
eq2c1 f g (right b1) = right (g b1)
eq2c2 : {A1 A2 B1 B2 : Set} -> (A2 -> A1) -> (B2 -> B1) -> (Sum A2 B2) -> (Sum A1 B1)
eq2c2 f’ g’ (left a2) = left (f’ a2)
eq2c2 f’ g’ (right b2) = right (g’ b2)
eq2c3 : {A1 A2 B1 B2 : Set} -> (A1 -> A2) -> (B1 -> B2) -> (Prod A1 B1) -> (Prod A2 B2)
eq2c3 f g (pair a1 b1) = pair (f a1) (g b1)
eq2c4 : {A1 A2 B1 B2 : Set} -> (A2 -> A1) -> (B2 -> B1) -> (Prod A2 B2) -> (Prod A1 B1)
eq2c4 f’ g’ (pair a2 b2) = pair (f’ a2) (g’ b2)
eq3a : {A1 A2 B1 B2 : Prop} -> (A1 -> A2) -> (B1 -> B2) -> (A1 or B1) -> (A2 or B2)
eq3a {A1} {A2} {B1} {B2} f g a1b1 = a2b2
where
or1 : A1 -> A2 or B2
or1 a1 = orIl (f a1)
or2 : B1 -> A2 or B2
or2 b1 = orIr (g b1)
a2b2 : A2 or B2
a2b2 = orE a1b1 or1 or2
eq3b : {A1 A2 B1 B2 : Prop} -> (A1 -> A2) -> (B1 -> B2) -> (A1 and B1) -> (A2 and B2)
eq3b {A1} {A2} {B1} {B2} f g a1b1 = a2b2
where
a1 : A1
a1 = andEl a1b1
b1 : B1
b1 = andEr a1b1
a2b2 : A2 and B2
a2b2 = andI (f a1) (g b1)
“`