{-# OPTIONS_GHC -fno-warn-orphans #-}

module Pandora.Paradigm.Schemes (module Exports) where

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))