@@ -18,20 +18,23 @@ import Data.ZZ
18-- and Monoid).
18-- and Monoid).
20interface Functor f => VerifiedFunctor (f : Type -> Type) where
20interface 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
22 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
22 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
23 (g1 : a -> b) -> (g2 : b -> c) ->
23 (g1 : a -> b) -> (g2 : b -> c) ->
24 map (g2 . g1) x = (map g2 . map g1) x
24 map (g2 . g1) x = (map g2 . map g1) x
26+functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
27+functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
26VerifiedFunctor Maybe where
29VerifiedFunctor Maybe where
27− functorIdentity Nothing = Refl
30+ functorIdentity _ _ Nothing = Refl
28− functorIdentity (Just x) = Refl
31+ functorIdentity g p (Just x) = rewrite p x in Refl
29 functorComposition Nothing g1 g2 = Refl
32 functorComposition Nothing g1 g2 = Refl
30 functorComposition (Just x) g1 g2 = Refl
33 functorComposition (Just x) g1 g2 = Refl
32VerifiedFunctor (Vect n) where
35VerifiedFunctor (Vect n) where
33− functorIdentity [] = Refl
36+ functorIdentity _ _ [] = Refl
34− functorIdentity (x :: xs) = rewrite functorIdentity xs in Refl
37+ functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
35 functorComposition [] _ _ = Refl
38 functorComposition [] _ _ = Refl
36 functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
39 functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
@@ -49,7 +52,7 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
49VerifiedApplicative (Vect n) where
52VerifiedApplicative (Vect n) where
50 applicativeMap [] f = Refl
53 applicativeMap [] f = Refl
51 applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
54 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
53 applicativeComposition [] [] [] = Refl
56 applicativeComposition [] [] [] = Refl
54 applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
57 applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl
55 applicativeHomomorphism = prf
58 applicativeHomomorphism = prf