VeryFun.idr

module VeryFun

class VeryFun (f : Type -> Type) (dict : Functor f) | f where
  funIdentity : {a : Type} -> (x : f a) ->
                map @{dict} id x = id x
  funComposition : {a : Type} -> {b : Type} ->
                   (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) ->
                   map @{dict} (g2 . g1) x = (map @{dict} g2 . map @{dict} g1) x

instance VeryFun List %instance where
  funIdentity []        = Refl
  funIdentity (x :: xs) = cong $ funIdentity xs
  funComposition []        g1 g2 = Refl
  funComposition (x :: xs) g1 g2 = cong $ funComposition xs g1 g2

test : (xs : List Nat) -> map ((+1) . (+2)) xs = map (+1) (map (+2) xs)
test xs = funComposition xs (+2) (+1)