@@ -17,21 +17,22 @@ record Iso a b where
18-- Isomorphism properties
18-- Isomorphism properties
20−||| Isomorphism is Reflexive
20+||| Isomorphism is reflexive
21isoRefl : Iso a a
21isoRefl : Iso a a
22−isoRefl = MkIso id id (\x => Refl) (\x => Refl)
22+isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)
24||| Isomorphism is transitive
24||| Isomorphism is transitive
25isoTrans : Iso a b -> Iso b c -> Iso a c
25isoTrans : Iso a b -> Iso b c -> Iso a c
26isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
26isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
27− MkIso (\x => to' (to x))
27+ MkIso xto xfrom xtoFrom xfromTo where
28− (\y => from (from' y))
28+ xto : a -> c
29− (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
29+ xto = to' . to
32+ xtoFrom : (z : c) -> xto (xfrom z) = z
30− (to' (from' y)) ={ toFrom' y }=
33+ xtoFrom z = rewrite toFrom $ from' z in toFrom' z
31− y QED)
34+ xfromTo : (x : a) -> xfrom (xto x) = x
32− (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
35+ xfromTo x = rewrite fromTo' (to x) in fromTo x
33− (from (to x)) ={ fromTo x }=
36Category Iso where
37Category Iso where
37 id = isoRefl
38 id = isoRefl
@@ -99,8 +100,7 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft
100||| Isomorphism is a congruence with regards to disjunction
101||| Isomorphism is a congruence with regards to disjunction
101eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
102eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
102−eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
103− (MkIso to from toFrom fromTo)
103+eitherCong (MkIso to from toFrom fromTo)
104 (MkIso to' from' toFrom' fromTo') =
104 (MkIso to' from' toFrom' fromTo') =
105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
@@ -143,9 +143,7 @@ pairAssoc = MkIso to from ok1 ok2
144||| Conjunction with truth is a no-op
144||| Conjunction with truth is a no-op
145pairUnitRight : Iso (a, ()) a
145pairUnitRight : Iso (a, ()) a
146−pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
146+pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)
147− where ok : (x : (a, ())) -> (fst x, ()) = x
150||| Conjunction with truth is a no-op
148||| Conjunction with truth is a no-op
151pairUnitLeft : Iso ((), a) a
149pairUnitLeft : Iso ((), a) a
@@ -161,8 +159,7 @@ pairBotRight = isoTrans pairComm pairBotLeft
162||| Isomorphism is a congruence with regards to conjunction
160||| Isomorphism is a congruence with regards to conjunction
163pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
161pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
164−pairCong {a = a} {a' = a'} {b = b} {b' = b'}
165− (MkIso to from toFrom fromTo)
162+pairCong (MkIso to from toFrom fromTo)
166 (MkIso to' from' toFrom' fromTo') =
163 (MkIso to' from' toFrom' fromTo') =
167 MkIso to'' from'' iso1 iso2
164 MkIso to'' from'' iso1 iso2
168 where to'' : (a, b) -> (a', b')
165 where to'' : (a, b) -> (a', b')
@@ -205,7 +202,7 @@ distribLeft = MkIso to from toFrom fromTo
206||| Products distribute over sums
203||| Products distribute over sums
207distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
204distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
208−distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
205+distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
211-- Enable preorder reasoning syntax over isomorphisms
208-- Enable preorder reasoning syntax over isomorphisms
@@ -222,7 +219,7 @@ step a iso1 iso2 = isoTrans iso1 iso2
222-- Isomorphisms over Maybe
219-- Isomorphisms over Maybe
223||| Isomorphism is a congruence with respect to Maybe
220||| Isomorphism is a congruence with respect to Maybe
224maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
221maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
225−maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
222+maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
226 where ok1 : (y : Maybe b) -> map to (map from y) = y
223 where ok1 : (y : Maybe b) -> map to (map from y) = y
227 ok1 Nothing = Refl
224 ok1 Nothing = Refl
228 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
225 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
@@ -253,7 +250,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=
255eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
252eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
256−eitherMaybeLeftMaybe {a} {b} =
253+eitherMaybeLeftMaybe =
257 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
254 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
258 (Either (Either a ()) b) ={ eitherAssoc }=
255 (Either (Either a ()) b) ={ eitherAssoc }=
259 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
256 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
@@ -263,7 +260,7 @@ eitherMaybeLeftMaybe {a} {b} =
265eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
262eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
266−eitherMaybeRightMaybe {a} {b} =
263+eitherMaybeRightMaybe =
267 (Either a (Maybe b)) ={ eitherComm }=
264 (Either a (Maybe b)) ={ eitherComm }=
268 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
265 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
269 (Maybe (Either b a)) ={ maybeCong eitherComm }=
266 (Maybe (Either b a)) ={ maybeCong eitherComm }=
@@ -288,8 +285,8 @@ maybeIsoS = MkIso forth back fb bf
288 fb (FS x) = Refl
285 fb (FS x) = Refl
290finZeroBot : Iso (Fin 0) Void
287finZeroBot : Iso (Fin 0) Void
291−finZeroBot = MkIso (\x => void (uninhabited x))
288+finZeroBot = MkIso (void . uninhabited)
292− (\x => void x)
289+ void
293 (\x => void x)
290 (\x => void x)
294 (\x => void (uninhabited x))
291 (\x => void (uninhabited x))