@@ -0,0 +1,122 @@
1+module Control.Isomorphism
2+
3+import Syntax.PreorderReasoning
4+
5+%default total
6+
7+-- An isomorphism between two types
8+data Iso : Type -> Type -> Type where
9+ MkIso : (to : a -> b) ->
10+ (from : b -> a) ->
11+ (toFrom : (y : b) -> to (from y) = y) ->
12+ (fromTo : (x : a) -> from (to x) = x) ->
13+ Iso a b
14+
15+-- Isomorphism properties
16+
17+isoRefl : Iso a a
18+isoRefl = MkIso id id (\x => refl) (\x => refl)
19+
20+isoTrans : Iso a b -> Iso b c -> Iso a c
21+isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
22+ MkIso (\x => to' (to x))
23+ (\y => from (from' y))
24+ (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
25+ (to' (from' y)) ={ toFrom' y }=
26+ y QED)
27+ (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
28+ (from (to x)) ={ fromTo x }=
29+ x QED)
30+
31+
32+
33+-- Isomorphisms over sums
34+
35+eitherComm : Iso (Either a b) (Either b a)
36+eitherComm = MkIso swap swap swapSwap swapSwap
37+ where swap : Either a b -> Either b a
38+ swap (Left x) = Right x
39+ swap (Right x) = Left x
40+ swapSwap : (e : Either a b) -> swap (swap e) = e
41+ swapSwap (Left x) = refl
42+ swapSwap (Right x) = refl
43+
44+eitherAssoc : Iso (Either (Either a b) c) (Either a (Either b c))
45+eitherAssoc = MkIso eitherAssoc1 eitherAssoc2 ok1 ok2
46+ where eitherAssoc1 : Either (Either a b) c -> Either a (Either b c)
47+ eitherAssoc1 (Left (Left x)) = Left x
48+ eitherAssoc1 (Left (Right x)) = Right (Left x)
49+ eitherAssoc1 (Right x) = Right (Right x)
50+
51+ eitherAssoc2 : Either a (Either b c) -> Either (Either a b) c
52+ eitherAssoc2 (Left x) = Left (Left x)
53+ eitherAssoc2 (Right (Left x)) = Left (Right x)
54+ eitherAssoc2 (Right (Right x)) = Right x
55+
56+ ok1 : (x : Either a (Either b c)) -> eitherAssoc1 (eitherAssoc2 x) = x
57+ ok1 (Left x) = refl
58+ ok1 (Right (Left x)) = refl
59+ ok1 (Right (Right x)) = refl
60+
61+ ok2 : (x : Either (Either a b) c) -> eitherAssoc2 (eitherAssoc1 x) = x
62+ ok2 (Left (Left x)) = refl
63+ ok2 (Left (Right x)) = refl
64+ ok2 (Right x) = refl
65+
66+eitherBotLeft : Iso (Either _|_ a) a
67+eitherBotLeft = MkIso to from ok1 ok2
68+ where to : Either _|_ a -> a
69+ to (Left x) = FalseElim x
70+ to (Right x) = x
71+ from : a -> Either _|_ a
72+ from = Right
73+ ok1 : (x : a) -> to (from x) = x
74+ ok1 x = refl
75+ ok2 : (x : Either _|_ a) -> from (to x) = x
76+ ok2 (Left x) = FalseElim x
77+ ok2 (Right x) = refl
78+
79+eitherBotRight : Iso (Either a _|_) a
80+eitherBotRight = isoTrans eitherComm eitherBotLeft
81+
82+-- Isomorphisms over products
83+pairComm : Iso (a, b) (b, a)
84+pairComm = MkIso swap swap swapSwap swapSwap
85+ where swap : (a, b) -> (b, a)
86+ swap (x, y) = (y, x)
87+ swapSwap : (x : (a, b)) -> swap (swap x) = x
88+ swapSwap (x, y) = refl
89+
90+pairAssoc : Iso (a, (b, c)) ((a, b), c)
91+pairAssoc = MkIso to from ok1 ok2
92+ where
93+ to : (a, (b, c)) -> ((a, b), c)
94+ to (x, (y, z)) = ((x, y), z)
95+ from : ((a, b), c) -> (a, (b, c))
96+ from ((x, y), z) = (x, (y, z))
97+ ok1 : (x : ((a, b), c)) -> to (from x) = x
98+ ok1 ((x, y), z) = refl
99+ ok2 : (x : (a, (b, c))) -> from (to x) = x
100+ ok2 (x, (y, z)) = refl
101+
102+pairUnitRight : Iso (a, ()) a
103+pairUnitRight = MkIso fst (\x => (x, ())) (\x => refl) ok
104+ where ok : (x : (a, ())) -> (fst x, ()) = x
105+ ok (x, ()) = refl
106+
107+pairUnitLeft : Iso ((), a) a
108+pairUnitLeft = isoTrans pairComm pairUnitRight
109+
110+pairBotLeft : Iso (_|_, a) _|_
111+pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
112+
113+pairBotRight : Iso (a, _|_) _|_
114+pairBotRight = isoTrans pairComm pairBotLeft
115+
116+
117+-- Enable preorder reasoning syntax over isomorphisms
118+qed : (a : Type) -> Iso a a
119+qed a = isoRefl
120+
121+step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
122+step a iso1 iso2 = isoTrans iso1 iso2