module HomeworkThirteen
%default total

infix 0 <=>
(<=>) : Type -> Type -> Type
a <=> b = (a -> b, b -> a)

exA : (p, q) <=> (q, p)
exA = (swap, swap)

exB : (p, (q, r)) <=> ((p, q), r)
exB = (\(a, (b, c)) => ((a, b), c), \((a, b), c) => (a, (b, c)))

pair : a -> b -> (a,b)
pair a b = (a, b)

exC : (p, Either q r) <=> Either (p, q) (p, r)
exC = (\(p, eqr) => either (Left . pair p) (Right . pair p) eqr, either (\(p, q) => (p, Left q)) (\(p, r) => (p, Right r)))