19 lines
466 B
Idris
19 lines
466 B
Idris
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)))
|