{-# OPTIONS_GHC -fno-warn-orphans #-} module Pandora.Paradigm.Schemes (module Exports, Schematic) where import Pandora.Paradigm.Schemes.PQ_ as Exports import Pandora.Paradigm.Schemes.P_Q_T as Exports import Pandora.Paradigm.Schemes.P_T as Exports import Pandora.Paradigm.Schemes.PTU as Exports import Pandora.Paradigm.Schemes.U_T as Exports import Pandora.Paradigm.Schemes.T_U 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.Paradigm.Schemes.TT as Exports import Pandora.Core.Interpreted (run) import Pandora.Pattern.Semigroupoid ((.)) import Pandora.Pattern.Category ((<--)) import Pandora.Pattern.Functor.Covariant (Covariant) import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-))) type family Schematic (c :: (* -> * -> *) -> (* -> *) -> k) (t :: * -> *) = (r :: (* -> *) -> * -> *) | r -> t instance (Covariant (->) (->) (v <:.> t), Covariant (->) (->) (u <:.> w), Adjoint (->) (->) t u, Adjoint (->) (->) v w) => Adjoint (->) (->) (v <:.> t) (u <:.> w) where a -> (<:.>) u w b g |- :: (a -> (<:.>) u w b) -> (<:.>) v t a -> b |- TU (v :. t) >>> a y = ((<:.>) u w b -> (u :. w) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < 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. Semigroupoid m => m b c -> m a b -> m a c . a -> (<:.>) u w b g (a -> (u :. w) >>> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (t a -> w b) -> ((v :. t) >>> a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- (v :. t) >>> a y (<:.>) v t a -> b f -| :: ((<:.>) v t a -> b) -> a -> (<:.>) u w b -| a x = ((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 (m a b) (m a 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. Semigroupoid 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 (v (t a) -> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (t a -> w b) -> a -> (u :. w) >>> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -| a x instance (Covariant (->) (->) (v <:.> t), Covariant (->) (->) (w <.:> u), Adjoint (->) (->) t u, Adjoint (->) (->) v w) => Adjoint (->) (->) (v <:.> t) (w <.:> u) where a -> (<.:>) w u b g |- :: (a -> (<.:>) w u b) -> (<:.>) v t a -> b |- TU (v :. t) >>> a t = ((<.:>) w u b -> (u :. w) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < 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. Semigroupoid m => m b c -> m a b -> m a c . a -> (<.:>) w u b g (a -> (u :. w) >>> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (t a -> w b) -> ((v :. t) >>> a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- (v :. t) >>> a t (<:.>) v t a -> b f -| :: ((<:.>) v t a -> b) -> a -> (<.:>) w u b -| a x = ((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 (m a b) (m a 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. Semigroupoid 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 (v (t a) -> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (t a -> w b) -> a -> (u :. w) >>> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -| a x instance (Covariant (->) (->) (t <.:> v), Covariant (->) (->) (w <.:> u), Adjoint (->) (->) t u, Adjoint (->) (->) v w) => Adjoint (->) (->) (t <.:> v) (w <.:> u) where a -> (<.:>) w u b g |- :: (a -> (<.:>) w u b) -> (<.:>) t v a -> b |- UT (v :. t) >>> a t = ((<.:>) w u b -> (u :. w) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < 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. Semigroupoid m => m b c -> m a b -> m a c . a -> (<.:>) w u b g (a -> (u :. w) >>> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (t a -> w b) -> ((v :. t) >>> a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- (v :. t) >>> a t (<.:>) t v a -> b f -| :: ((<.:>) t v a -> b) -> a -> (<.:>) w u b -| a x = ((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 (m a b) (m a 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. Semigroupoid 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 (v (t a) -> b) -> t a -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (t a -> w b) -> a -> (u :. w) >>> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -| a x instance (Covariant (->) (->) (t <.:> v), Covariant (->) (->) (w <:.> u), Adjoint (->) (->) v u, Adjoint (->) (->) t w) => Adjoint (->) (->) (t <.:> v) (w <:.> u) where a -> (<:.>) w u b g |- :: (a -> (<:.>) w u b) -> (<.:>) t v a -> b |- UT (v :. t) >>> a x = ((<:.>) w u b -> (w :. u) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < 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. Semigroupoid m => m b c -> m a b -> m a c . a -> (<:.>) w u b g (a -> (w :. u) >>> b) -> t a -> u b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (t a -> u b) -> ((v :. t) >>> a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- (v :. t) >>> a x (<.:>) t v a -> b f -| :: ((<.:>) t v a -> b) -> a -> (<:.>) w u b -| a x = ((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 (m a b) (m a 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. Semigroupoid 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 (v (t a) -> b) -> t a -> u b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (t a -> u b) -> a -> (w :. u) >>> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -| a x 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 a -> (<:<.>:>) v w v' b g |- :: (a -> (<:<.>:>) v w v' b) -> (<:<.>:>) t u t' a -> b |- TUT (t :. (t' :. u)) >>> a x = (((<:<.>:>) v w v' b -> (v :. (v' :. w)) >>> b forall (m :: * -> * -> *) (t :: * -> *) a. Interpreted m t => (m < 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. Semigroupoid m => m b c -> m a b -> m a c . a -> (<:<.>:>) v w v' b g (a -> (v :. (v' :. w)) >>> b) -> u a -> v' (w b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (u a -> v' (w b)) -> t' (u a) -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |-) (t' (u a) -> w b) -> ((t :. (t' :. u)) >>> a) -> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => target a (u b) -> source (t a) b |- (t :. (t' :. u)) >>> a x (<:<.>:>) t u t' a -> b f -| :: ((<:<.>:>) t u t' a -> b) -> a -> (<:<.>:>) v w v' b -| a x = ((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 (m a b) (m a 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. Semigroupoid 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 (t (t' (u a)) -> b) -> t' (u a) -> w b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (t' (u a) -> w b) -> u a -> v' (w b) forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -|) (u a -> v' (w b)) -> a -> (v :. (v' :. w)) >>> b forall (source :: * -> * -> *) (target :: * -> * -> *) (t :: * -> *) (u :: * -> *) a b. Adjoint source target t u => source (t a) b -> target a (u b) -| a x