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