* Show that `A + (B + C) ~ (A + B) + C`.
* Show that if `A ~ A’` and `B ~ B’` then `Sum A B ~ Sum A’ B’`.
* Find another example of types `A, B` so that logically `A ↔ ︎B` but `A`, `B` are **not** isomorphic.
* Using the Church encoding check that indeed plus one one is equal to two.
* Revisit the proofs from Assignment 1 and write them as lambda terms.
* (**Hard**) Which one of the De Morgan equations cannot be proved constructively? Show constructive proofs for constructive De Morgan laws and a proof that non-constructive De Morgan laws imply DNE or LEM.
* If possible, infer types for:
* `\f x -> x`
* `\f x -> f(f x)`
* `\f x -> x(f x)`
* `\x -> x x x`
* `\h t f x -> f h (t f x)`