module Proarrow.Profunctor.Initial where

import Proarrow.Category.Dagger (DaggerProfunctor (..))
import Proarrow.Core (CategoryOf, Profunctor (..), type (+->))

type InitialProfunctor :: j +-> k
data InitialProfunctor a b

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

instance (CategoryOf k) => DaggerProfunctor (InitialProfunctor :: k +-> k) where
  dagger :: forall (a :: k) (b :: k).
InitialProfunctor a b -> InitialProfunctor b a
dagger = \case {}