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