@@ -23,11 +23,11 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
23 MkIso (\x => to' (to x))
23 MkIso (\x => to' (to x))
24 (\y => from (from' y))
24 (\y => from (from' y))
25 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
25 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
26− (to' (from' y)) ={ toFrom' y }=
26+ (to' (from' y)) ={ toFrom' y }=
28 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
28 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
29− (from (to x)) ={ fromTo x }=
29+ (from (to x)) ={ fromTo x }=
32isoSym : Iso a b -> Iso b a
32isoSym : Iso a b -> Iso b a
33isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
33isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
@@ -216,7 +216,7 @@ maybeEither = MkIso to from iso1 iso2
216 iso2 (Just x) = refl
216 iso2 (Just x) = refl
218maybeVoidUnit : Iso (Maybe _|_) ()
218maybeVoidUnit : Iso (Maybe _|_) ()
219−maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
219+maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
220 (Either _|_ ()) ={ eitherBotLeft }=
220 (Either _|_ ()) ={ eitherBotLeft }=