{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Schemes (module Exports) where import Pandora.Paradigm.Schemes.U_T as Exports import Pandora.Paradigm.Schemes.T_U as Exports import Pandora.Paradigm.Schemes.T_ as Exports import Pandora.Paradigm.Schemes.UTU as Exports import Pandora.Paradigm.Schemes.UT as Exports import Pandora.Paradigm.Schemes.TUVW as Exports import Pandora.Paradigm.Schemes.TUT as Exports import Pandora.Paradigm.Schemes.TU as Exports import Pandora.Pattern.Category ((.), ($)) import Pandora.Pattern.Functor.Covariant (Covariant) import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-))) import Pandora.Paradigm.Controlflow.Effect.Interpreted (run) instance (Covariant (v <:.> t), Covariant (u <:.> w), Adjoint t u, Adjoint v w) => Adjoint (v <:.> t) (u <:.> w) where TU (v :. t) := a y |- :: (<:.>) v t a -> (a -> (<:.>) u w b) -> b |- a -> (<:.>) u w b g = (v :. t) := a y ((v :. t) := a) -> (t a -> w b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (t a -> (a -> u (w b)) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (<:.>) u w b -> u (w b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:.>) u w b -> u (w b)) -> (a -> (<:.>) u w b) -> a -> u (w b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (<:.>) u w b g) a x -| :: a -> ((<:.>) v t a -> b) -> (<:.>) u w b -| (<:.>) v t a -> b f = ((u :. w) := b) -> (<:.>) u w b forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((u :. w) := b) -> (<:.>) u w b) -> ((u :. w) := b) -> (<:.>) u w b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (t a -> w b) -> (u :. w) := b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (t a -> (v (t a) -> b) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (<:.>) v t a -> b f ((<:.>) v t a -> b) -> (v (t a) -> (<:.>) v t a) -> v (t a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . v (t a) -> (<:.>) v t a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU) instance (Covariant (v <:.> t), Covariant (w <.:> u), Adjoint t u, Adjoint v w) => Adjoint (v <:.> t) (w <.:> u) where TU (v :. t) := a t |- :: (<:.>) v t a -> (a -> (<.:>) w u b) -> b |- a -> (<.:>) w u b g = (v :. t) := a t ((v :. t) := a) -> (t a -> w b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (t a -> (a -> u (w b)) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (<.:>) w u b -> u (w b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<.:>) w u b -> u (w b)) -> (a -> (<.:>) w u b) -> a -> u (w b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (<.:>) w u b g) a x -| :: a -> ((<:.>) v t a -> b) -> (<.:>) w u b -| (<:.>) v t a -> b f = ((u :. w) := b) -> (<.:>) w u b forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. w) := b) -> (<.:>) w u b) -> ((u :. w) := b) -> (<.:>) w u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (t a -> w b) -> (u :. w) := b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (t a -> (v (t a) -> b) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (<:.>) v t a -> b f ((<:.>) v t a -> b) -> (v (t a) -> (<:.>) v t a) -> v (t a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . v (t a) -> (<:.>) v t a forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU) instance (Covariant (t <.:> v), Covariant (w <.:> u), Adjoint t u, Adjoint v w) => Adjoint (t <.:> v) (w <.:> u) where UT (v :. t) := a t |- :: (<.:>) t v a -> (a -> (<.:>) w u b) -> b |- a -> (<.:>) w u b g = (v :. t) := a t ((v :. t) := a) -> (t a -> w b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (t a -> (a -> u (w b)) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (<.:>) w u b -> u (w b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<.:>) w u b -> u (w b)) -> (a -> (<.:>) w u b) -> a -> u (w b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (<.:>) w u b g) a x -| :: a -> ((<.:>) t v a -> b) -> (<.:>) w u b -| (<.:>) t v a -> b f = ((u :. w) := b) -> (<.:>) w u b forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT (((u :. w) := b) -> (<.:>) w u b) -> ((u :. w) := b) -> (<.:>) w u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (t a -> w b) -> (u :. w) := b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (t a -> (v (t a) -> b) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (<.:>) t v a -> b f ((<.:>) t v a -> b) -> (v (t a) -> (<.:>) t v a) -> v (t a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . v (t a) -> (<.:>) t v a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT) instance (Covariant (t <.:> v), Covariant (w <:.> u) , Adjoint v u, Adjoint t w) => Adjoint (t <.:> v) (w <:.> u) where UT (v :. t) := a t |- :: (<.:>) t v a -> (a -> (<:.>) w u b) -> b |- a -> (<:.>) w u b g = (v :. t) := a t ((v :. t) := a) -> (t a -> u b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (t a -> (a -> w (u b)) -> u b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (<:.>) w u b -> w (u b) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:.>) w u b -> w (u b)) -> (a -> (<:.>) w u b) -> a -> w (u b) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (<:.>) w u b g) a x -| :: a -> ((<.:>) t v a -> b) -> (<:.>) w u b -| (<.:>) t v a -> b f = ((w :. u) := b) -> (<:.>) w u b forall k k k k (ct :: k) (cu :: k) (t :: k -> *) (u :: k -> k) (a :: k). ((t :. u) := a) -> TU ct cu t u a TU (((w :. u) := b) -> (<:.>) w u b) -> ((w :. u) := b) -> (<:.>) w u b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (t a -> u b) -> (w :. u) := b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (t a -> (v (t a) -> b) -> u b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (<.:>) t v a -> b f ((<.:>) t v a -> b) -> (v (t a) -> (<.:>) t v a) -> v (t a) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . v (t a) -> (<.:>) t v a forall k k k k (ct :: k) (cu :: k) (t :: k -> k) (u :: k -> *) (a :: k). ((u :. t) := a) -> UT ct cu t u a UT) instance (Covariant ((t <:<.>:> u) t'), Covariant ((v <:<.>:> w) v') , Adjoint t w, Adjoint t' v', Adjoint t v, Adjoint u v, Adjoint v' t') => Adjoint ((t <:<.>:> u) t') ((v <:<.>:> w) v') where TUT (t :. (t' :. u)) := a t |- :: (<:<.>:>) t u t' a -> (a -> (<:<.>:>) v w v' b) -> b |- a -> (<:<.>:>) v w v' b g = (t :. (t' :. u)) := a t ((t :. (t' :. u)) := a) -> ((:.) t' u a -> w b) -> b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- ((:.) t' u a -> (u a -> v' (w b)) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (u a -> (a -> v (v' (w b))) -> v' (w b) forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => t a -> (a -> u b) -> b |- (<:<.>:>) v w v' b -> v (v' (w b)) forall (t :: * -> *) a. Interpreted t => t a -> Primary t a run ((<:<.>:>) v w v' b -> v (v' (w b))) -> (a -> (<:<.>:>) v w v' b) -> a -> v (v' (w b)) forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . a -> (<:<.>:>) v w v' b g)) a x -| :: a -> ((<:<.>:>) t u t' a -> b) -> (<:<.>:>) v w v' b -| (<:<.>:>) t u t' a -> b f = ((v :. (v' :. w)) := b) -> (<:<.>:>) v w v' b forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT (((v :. (v' :. w)) := b) -> (<:<.>:>) v w v' b) -> ((v :. (v' :. w)) := b) -> (<:<.>:>) v w v' b forall (m :: * -> * -> *) a b. Category m => m a b -> m a b $ a x a -> (u a -> v' (w b)) -> (v :. (v' :. w)) := b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (u a -> (t' (u a) -> w b) -> v' (w b) forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (t' (u a) -> (t (t' (u a)) -> b) -> w b forall (t :: * -> *) (u :: * -> *) a b. Adjoint t u => a -> (t a -> b) -> u b -| (<:<.>:>) t u t' a -> b f ((<:<.>:>) t u t' a -> b) -> (t (t' (u a)) -> (<:<.>:>) t u t' a) -> t (t' (u a)) -> b forall (m :: * -> * -> *) b c a. Category m => m b c -> m a b -> m a c . t (t' (u a)) -> (<:<.>:>) t u t' a forall k k k k k k (ct :: k) (ct' :: k) (cu :: k) (t :: k -> *) (t' :: k -> k) (u :: k -> k) (a :: k). ((t :. (u :. t')) := a) -> TUT ct ct' cu t t' u a TUT))