@@ -23,11 +23,11 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
2323 MkIso (\x => to' (to x))
2424 (\y => from (from' y))
2525 (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
26− (to' (from' y)) ={ toFrom' y }=
27− y QED)
26+ (to' (from' y)) ={ toFrom' y }=
27+ y QED)
2828 (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
29− (from (to x)) ={ fromTo x }=
30− x QED)
29+ (from (to x)) ={ fromTo x }=
30+ x QED)
3131
3232isoSym : Iso a b -> Iso b a
3333isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
@@ -216,7 +216,7 @@ maybeEither = MkIso to from iso1 iso2
216216 iso2 (Just x) = refl
217217
218218maybeVoidUnit : Iso (Maybe _|_) ()
219−maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
219+maybeVoidUnit = (Maybe _|_) ={ maybeEither }=
220220 (Either _|_ ()) ={ eitherBotLeft }=
221221 () QED
222222