module Proarrow.Profunctor.Initial where

import Proarrow.Core (PRO, Profunctor (..), CategoryOf)

type InitialProfunctor :: PRO j k
data InitialProfunctor a b

instance (CategoryOf j, CategoryOf k) => Profunctor (InitialProfunctor :: PRO j k) where
  dimap :: forall (c :: j) (a :: j) (b :: k) (d :: k).
(c ~> a)
-> (b ~> d) -> InitialProfunctor a b -> InitialProfunctor c d
dimap c ~> a
_ b ~> d
_ = InitialProfunctor a b -> InitialProfunctor c d
\case
  \\ :: forall (a :: j) (b :: k) r.
((Ob a, Ob b) => r) -> InitialProfunctor a b -> r
(\\) (Ob a, Ob b) => r
_ = InitialProfunctor a b -> r
\case