@@ -28,7 +28,8 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
2828 (from (to x)) ={ fromTo x }=
2929 x QED)
3030
31−
31+isoSym : Iso a b -> Iso b a
32+isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
3233
3334-- Isomorphisms over sums
3435
@@ -79,6 +80,22 @@ eitherBotLeft = MkIso to from ok1 ok2
7980eitherBotRight : Iso (Either a _|_) a
8081eitherBotRight = isoTrans eitherComm eitherBotLeft
8182
83+
84+eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
85+eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
86+ (MkIso to from toFrom fromTo)
87+ (MkIso to' from' toFrom' fromTo') =
88+ MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
89+ where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
90+ eitherMap f g (Left x) = Left (f x)
91+ eitherMap f g (Right x) = Right (g x)
92+ ok1 : (x : Either a' b') -> eitherMap to to' (eitherMap from from' x) = x
93+ ok1 (Left x) = cong (toFrom x)
94+ ok1 (Right x) = cong (toFrom' x)
95+ ok2 : (x : Either a b) -> eitherMap from from' (eitherMap to to' x) = x
96+ ok2 (Left x) = cong (fromTo x)
97+ ok2 (Right x) = cong (fromTo' x)
98+
8299-- Isomorphisms over products
83100pairComm : Iso (a, b) (b, a)
84101pairComm = MkIso swap swap swapSwap swapSwap
@@ -113,6 +130,23 @@ pairBotLeft = MkIso fst FalseElim (\x => FalseElim x) (\y => FalseElim (fst y))
113130pairBotRight : Iso (a, _|_) _|_
114131pairBotRight = isoTrans pairComm pairBotLeft
115132
133+pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
134+pairCong {a = a} {a' = a'} {b = b} {b' = b'}
135+ (MkIso to from toFrom fromTo)
136+ (MkIso to' from' toFrom' fromTo') =
137+ MkIso to'' from'' iso1 iso2
138+ where to'' : (a, b) -> (a', b')
139+ to'' (x, y) = (to x, to' y)
140+ from'' : (a', b') -> (a, b)
141+ from'' (x, y) = (from x, from' y)
142+ iso1 : (x : (a', b')) -> to'' (from'' x) = x
143+ iso1 (x, y) = rewrite toFrom x in
144+ rewrite toFrom' y in
145+ refl
146+ iso2 : (x : (a, b)) -> from'' (to'' x) = x
147+ iso2 (x, y) = rewrite fromTo x in
148+ rewrite fromTo' y in
149+ refl
116150
117151-- Enable preorder reasoning syntax over isomorphisms
118152qed : (a : Type) -> Iso a a
@@ -120,3 +154,54 @@ qed a = isoRefl
120154
121155step : (a : Type) -> Iso a b -> Iso b c -> Iso a c
122156step a iso1 iso2 = isoTrans iso1 iso2
157+
158+
159+
160+-- Isomorphisms over Maybe
161+maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
162+maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
163+ where ok1 : (y : Maybe b) -> map to (map from y) = y
164+ ok1 Nothing = refl
165+ ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
166+ ok2 : (x : Maybe a) -> map from (map to x) = x
167+ ok2 Nothing = refl
168+ ok2 (Just x) = (Just (from (to x))) ={ cong (fromTo x) }= (Just x) QED
169+
170+maybeEither : Iso (Maybe a) (Either a ())
171+maybeEither = MkIso to from iso1 iso2
172+ where to : Maybe a -> Either a ()
173+ to Nothing = Right ()
174+ to (Just x) = Left x
175+ from : Either a () -> Maybe a
176+ from (Left x) = Just x
177+ from (Right ()) = Nothing
178+ iso1 : (x : Either a ()) -> to (from x) = x
179+ iso1 (Left x) = refl
180+ iso1 (Right ()) = refl
181+ iso2 : (y : Maybe a) -> from (to y) = y
182+ iso2 Nothing = refl
183+ iso2 (Just x) = refl
184+
185+maybeVoidUnit : Iso (Maybe _|_) ()
186+maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
187+ (Either _|_ ()) ={ eitherBotLeft }=
188+ () QED
189+
190+eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
191+eitherMaybeLeftMaybe {a} {b} =
192+ (Either (Maybe a) b) ={ eitherCong maybeEither isoRefl }=
193+ (Either (Either a ()) b) ={ eitherAssoc }=
194+ (Either a (Either () b)) ={ eitherCong isoRefl eitherComm }=
195+ (Either a (Either b ())) ={ isoSym eitherAssoc }=
196+ (Either (Either a b) ()) ={ isoSym maybeEither }=
197+ (Maybe (Either a b)) QED
198+
199+
200+eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
201+eitherMaybeRightMaybe {a} {b} =
202+ (Either a (Maybe b)) ={ eitherComm }=
203+ (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
204+ (Maybe (Either b a)) ={ maybeCong eitherComm }=
205+ (Maybe (Either a b)) QED
206+
207+