@@ -18,20 +18,23 @@ import Data.ZZ
1818-- and Monoid).
1919
2020interface Functor f => VerifiedFunctor (f : Type -> Type) where
21− functorIdentity : {a : Type} -> (x : f a) -> map Basics.id x = Basics.id x
21+ functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x
2222 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
2323 (g1 : a -> b) -> (g2 : b -> c) ->
2424 map (g2 . g1) x = (map g2 . map g1) x
2525
26+functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
27+functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
28+
2629VerifiedFunctor Maybe where
27− functorIdentity Nothing = Refl
28− functorIdentity (Just x) = Refl
30+ functorIdentity _ _ Nothing = Refl
31+ functorIdentity g p (Just x) = rewrite p x in Refl
2932 functorComposition Nothing g1 g2 = Refl
3033 functorComposition (Just x) g1 g2 = Refl
3134
3235VerifiedFunctor (Vect n) where
33− functorIdentity [] = Refl
34− functorIdentity (x :: xs) = rewrite functorIdentity xs in Refl
36+ functorIdentity _ _ [] = Refl
37+ functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
3538 functorComposition [] _ _ = Refl
3639 functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
3740
@@ -49,7 +52,7 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
4952VerifiedApplicative (Vect n) where
5053 applicativeMap [] f = Refl
5154 applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
52− applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity xs
55+ applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
5356 applicativeComposition [] [] [] = Refl
5457 applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
5558 applicativeHomomorphism = prf