{-# 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