Dependent Profunctor

hiprofun.idr

interface HiProfunctor (0 p : (0 xt : Type) -> (xt -> Type) -> Type) where
    dimap : (a, b : Type) -> (c : b -> Type) -> (d : (a -> Type))
         -> (ab : (a -> b)) -> ((y : a) -> c (ab y) -> d y)
         -> p b c -> p a d

data DepFun : (0 xt : Type) -> (xt -> Type) -> Type where
    DF : (0 xt : Type) -> (yt : xt -> Type) -> ((x : xt) -> yt x) -> DepFun xt yt

HiProfunctor DepFun where
    dimap a b c d ab acd (DF _ _ bc) = DF a d (\av : a => acd av (bc (ab av)))