{-# LANGUAGE AllowAmbiguousTypes #-}

module Proarrow.Object.Coexponential where

import Proarrow.Category.Monoidal (Monoidal (..))
import Proarrow.Core (CategoryOf (..), Obj, obj)
import Proarrow.Object.BinaryCoproduct (Cocartesian)

class (Monoidal k) => Coclosed k where
  type (a :: k) <~~ (b :: k) :: k
  coeval' :: Obj (a :: k) -> Obj b -> a ~> (a <~~ b) ** b
  coevalUniv' :: Obj (b :: k) -> Obj c -> a ~> c ** b -> (a <~~ b) ~> c

coeval :: forall {k} (a :: k) b. (Coclosed k, Ob a, Ob b) => a ~> (a <~~ b) ** b
coeval :: forall {k} (a :: k) (b :: k).
(Coclosed k, Ob a, Ob b) =>
a ~> ((a <~~ b) ** b)
coeval = Obj a -> Obj b -> a ~> ((a <~~ b) ** b)
forall (a :: k) (b :: k). Obj a -> Obj b -> a ~> ((a <~~ b) ** b)
forall k (a :: k) (b :: k).
Coclosed k =>
Obj a -> Obj b -> a ~> ((a <~~ b) ** b)
coeval' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @a) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b)

coevalUniv :: forall {k} (a :: k) b c. (Coclosed k, Ob b, Ob c) => a ~> c ** b -> (a <~~ b) ~> c
coevalUniv :: forall {k} (a :: k) (b :: k) (c :: k).
(Coclosed k, Ob b, Ob c) =>
(a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv = Obj b -> Obj c -> (a ~> (c ** b)) -> (a <~~ b) ~> c
forall (b :: k) (c :: k) (a :: k).
Obj b -> Obj c -> (a ~> (c ** b)) -> (a <~~ b) ~> c
forall k (b :: k) (c :: k) (a :: k).
Coclosed k =>
Obj b -> Obj c -> (a ~> (c ** b)) -> (a <~~ b) ~> c
coevalUniv' (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @b) (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @c)

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