{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Coexponential where

import Proarrow.Category.Instance.Unit (Unit (..))
import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (CategoryOf (..))
import Proarrow.Object.BinaryCoproduct (Cocartesian)

class (Monoidal k) => Coclosed k where
  type (a :: k) <~~ (b :: k) :: k
  withObCoExp :: (Ob (a :: k), Ob b) => ((Ob (a <~~ b)) => r) -> r
  coeval :: (Ob (a :: k), Ob b) => a ~> (a <~~ b) ** b
  coevalUniv :: (Ob (b :: k), Ob c) => a ~> c ** b -> (a <~~ b) ~> c

instance Coclosed () where
  type (a :: ()) <~~ (b :: ()) = '()
  withObCoExp :: forall (a :: ()) (b :: ()) r.
(Ob a, Ob b) =>
(Ob (a <~~ b) => r) -> r
withObCoExp Ob (a <~~ b) => r
f = r
Ob (a <~~ b) => r
f
  coeval :: forall (a :: ()) (b :: ()). (Ob a, Ob b) => a ~> ((a <~~ b) ** b)
coeval = a ~> ((a <~~ b) ** b)
Unit '() '()
Unit
  coevalUniv :: forall (b :: ()) (c :: ()) (a :: ()).
(Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv a ~> (c ** b)
Unit a '()
Unit = (a <~~ b) ~> c
Unit '() '()
Unit

class (Cocartesian k, Coclosed k) => CoCCC k
instance (Cocartesian k, Coclosed k) => CoCCC k