@@ -17,22 +17,21 @@ record Iso a b where
1717
1818-- Isomorphism properties
1919
20−||| Isomorphism is reflexive
20+||| Isomorphism is Reflexive
2121isoRefl : Iso a a
22−isoRefl = MkIso id id (\_ => Refl) (\_ => Refl)
22+isoRefl = MkIso id id (\x => Refl) (\x => Refl)
2323
2424||| Isomorphism is transitive
2525isoTrans : Iso a b -> Iso b c -> Iso a c
2626isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
27− MkIso xto xfrom xtoFrom xfromTo where
28− xto : a -> c
29− xto = to' . to
30− xfrom : c -> a
31− xfrom = from . from'
32− xtoFrom : (z : c) -> xto (xfrom z) = z
33− xtoFrom z = rewrite toFrom $ from' z in toFrom' z
34− xfromTo : (x : a) -> xfrom (xto x) = x
35− xfromTo x = rewrite fromTo' (to x) in fromTo x
27+ MkIso (\x => to' (to x))
28+ (\y => from (from' y))
29+ (\y => (to' (to (from (from' y)))) ={ cong (toFrom (from' y)) }=
30+ (to' (from' y)) ={ toFrom' y }=
31+ y QED)
32+ (\x => (from (from' (to' (to x)))) ={ cong (fromTo' (to x)) }=
33+ (from (to x)) ={ fromTo x }=
34+ x QED)
3635
3736Category Iso where
3837 id = isoRefl
@@ -100,7 +99,8 @@ eitherBotRight = isoTrans eitherComm eitherBotLeft
10099
101100||| Isomorphism is a congruence with regards to disjunction
102101eitherCong : Iso a a' -> Iso b b' -> Iso (Either a b) (Either a' b')
103−eitherCong (MkIso to from toFrom fromTo)
102+eitherCong {a = a} {a' = a'} {b = b} {b' = b'}
103+ (MkIso to from toFrom fromTo)
104104 (MkIso to' from' toFrom' fromTo') =
105105 MkIso (eitherMap to to') (eitherMap from from') ok1 ok2
106106 where eitherMap : (c -> c') -> (d -> d') -> Either c d -> Either c' d'
@@ -143,7 +143,9 @@ pairAssoc = MkIso to from ok1 ok2
143143
144144||| Conjunction with truth is a no-op
145145pairUnitRight : Iso (a, ()) a
146−pairUnitRight = MkIso fst (\x => (x, ())) (\_ => Refl) (\(_, ()) => Refl)
146+pairUnitRight = MkIso fst (\x => (x, ())) (\x => Refl) ok
147+ where ok : (x : (a, ())) -> (fst x, ()) = x
148+ ok (x, ()) = Refl
147149
148150||| Conjunction with truth is a no-op
149151pairUnitLeft : Iso ((), a) a
@@ -159,7 +161,8 @@ pairBotRight = isoTrans pairComm pairBotLeft
159161
160162||| Isomorphism is a congruence with regards to conjunction
161163pairCong : Iso a a' -> Iso b b' -> Iso (a, b) (a', b')
162−pairCong (MkIso to from toFrom fromTo)
164+pairCong {a = a} {a' = a'} {b = b} {b' = b'}
165+ (MkIso to from toFrom fromTo)
163166 (MkIso to' from' toFrom' fromTo') =
164167 MkIso to'' from'' iso1 iso2
165168 where to'' : (a, b) -> (a', b')
@@ -202,7 +205,7 @@ distribLeft = MkIso to from toFrom fromTo
202205
203206||| Products distribute over sums
204207distribRight : Iso (a, Either b c) (Either (a, b) (a, c))
205−distribRight = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
208+distribRight {a} {b} {c} = (pairComm `isoTrans` distribLeft) `isoTrans` eitherCong pairComm pairComm
206209
207210
208211-- Enable preorder reasoning syntax over isomorphisms
@@ -219,7 +222,7 @@ step a iso1 iso2 = isoTrans iso1 iso2
219222-- Isomorphisms over Maybe
220223||| Isomorphism is a congruence with respect to Maybe
221224maybeCong : Iso a b -> Iso (Maybe a) (Maybe b)
222−maybeCong (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
225+maybeCong {a} {b} (MkIso to from toFrom fromTo) = MkIso (map to) (map from) ok1 ok2
223226 where ok1 : (y : Maybe b) -> map to (map from y) = y
224227 ok1 Nothing = Refl
225228 ok1 (Just x) = (Just (to (from x))) ={ cong (toFrom x) }= (Just x) QED
@@ -250,7 +253,7 @@ maybeVoidUnit = (Maybe Void) ={ maybeEither }=
250253 () QED
251254
252255eitherMaybeLeftMaybe : Iso (Either (Maybe a) b) (Maybe (Either a b))
253−eitherMaybeLeftMaybe =
256+eitherMaybeLeftMaybe {a} {b} =
254257 (Either (Maybe a) b) ={ eitherCongLeft maybeEither }=
255258 (Either (Either a ()) b) ={ eitherAssoc }=
256259 (Either a (Either () b)) ={ eitherCongRight eitherComm }=
@@ -260,7 +263,7 @@ eitherMaybeLeftMaybe =
260263
261264
262265eitherMaybeRightMaybe : Iso (Either a (Maybe b)) (Maybe (Either a b))
263−eitherMaybeRightMaybe =
266+eitherMaybeRightMaybe {a} {b} =
264267 (Either a (Maybe b)) ={ eitherComm }=
265268 (Either (Maybe b) a) ={ eitherMaybeLeftMaybe }=
266269 (Maybe (Either b a)) ={ maybeCong eitherComm }=
@@ -285,8 +288,8 @@ maybeIsoS = MkIso forth back fb bf
285288 fb (FS x) = Refl
286289
287290finZeroBot : Iso (Fin 0) Void
288−finZeroBot = MkIso (void . uninhabited)
289− void
291+finZeroBot = MkIso (\x => void (uninhabited x))
292+ (\x => void x)
290293 (\x => void x)
291294 (\x => void (uninhabited x))
292295