@@ -26,6 +26,10 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
26functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
26functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x
27functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
27functorIdentity' {f} = functorIdentity {f} id (\x => Refl)
29+VerifiedFunctor (Pair a) where
30+ functorIdentity g p (a,b) = rewrite p b in Refl
31+ functorComposition (a,b) g1 g2 = Refl
29VerifiedFunctor Maybe where
33VerifiedFunctor Maybe where
30 functorIdentity _ _ Nothing = Refl
34 functorIdentity _ _ Nothing = Refl
31 functorIdentity g p (Just x) = rewrite p x in Refl
35 functorIdentity g p (Just x) = rewrite p x in Refl