module Proarrow.Profunctor.Initial where

import Proarrow.Category.Dagger (Dagger, DaggerProfunctor (..))
import Proarrow.Core (CategoryOf, Profunctor (..), type (+->))
import Proarrow.Preorder.ThinCategory (ThinProfunctor (..), Thin)
import Proarrow.Category.Instance.Zero (Bottom (..))

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 (Dagger k) => DaggerProfunctor (InitialProfunctor :: k +-> k) where
  dagger :: forall (a :: k) (b :: k).
InitialProfunctor a b -> InitialProfunctor b a
dagger = \case {}

instance (Thin j, Thin k) => (ThinProfunctor (InitialProfunctor :: j +-> k)) where
  type HasArrow (InitialProfunctor :: j +-> k) a b = Bottom
  arr :: forall (a :: k) (b :: j).
(Ob a, Ob b, HasArrow InitialProfunctor a b) =>
InitialProfunctor a b
arr = InitialProfunctor a b
forall a. Bottom => a
forall a. a
no
  withArr :: forall (a :: k) (b :: j) r.
InitialProfunctor a b -> (HasArrow InitialProfunctor a b => r) -> r
withArr = \case {}