module Pandora.Paradigm.Primary.Transformer.Kan where

import Pandora.Core.Interpreted (Interpreted (Primary, run, unite))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--))
import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-)))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Paradigm.Primary.Auxiliary (Horizontal (Left, Right))
import Pandora.Paradigm.Algebraic.Exponential ()

data family Kan (v :: * -> k) (t :: * -> *) (u :: * -> *) b a

data instance Kan Left t u b a = Lan ((t b -> a) -> u b)

instance Contravariant (->) (->) (Kan Left t u b) where
	a -> b
f >-|- :: (a -> b) -> Kan 'Left t u b b -> Kan 'Left t u b a
>-|- Lan x = ((t b -> a) -> u b) -> Kan 'Left t u b a
forall (t :: * -> *) (u :: * -> *) b a.
((t b -> a) -> u b) -> Kan 'Left t u b a
Lan (((t b -> a) -> u b) -> Kan 'Left t u b a)
-> ((t b -> a) -> u b) -> Kan 'Left t u b a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (t b -> b) -> u b
x ((t b -> b) -> u b)
-> ((t b -> a) -> t b -> b) -> (t b -> a) -> u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (a -> b
f (a -> b) -> (t b -> a) -> t b -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
.)

instance Interpreted (->) (Kan Left t u b) where
	type Primary (Kan Left t u b) a = (t b -> a) -> u b
	run :: ((->) < Kan 'Left t u b a) < Primary (Kan 'Left t u b) a
run ~(Lan x) = Primary (Kan 'Left t u b) a
(t b -> a) -> u b
x
	unite :: ((->) < Primary (Kan 'Left t u b) a) < Kan 'Left t u b a
unite = ((->) < Primary (Kan 'Left t u b) a) < Kan 'Left t u b a
forall (t :: * -> *) (u :: * -> *) b a.
((t b -> a) -> u b) -> Kan 'Left t u b a
Lan

data instance Kan Right t u b a = Ran ((a -> t b) -> u b)

instance Covariant (->) (->) (Kan Right t u b) where
	a -> b
f <-|- :: (a -> b) -> Kan 'Right t u b a -> Kan 'Right t u b b
<-|- Ran x = ((b -> t b) -> u b) -> Kan 'Right t u b b
forall (t :: * -> *) (u :: * -> *) b a.
((a -> t b) -> u b) -> Kan 'Right t u b a
Ran (((b -> t b) -> u b) -> Kan 'Right t u b b)
-> ((b -> t b) -> u b) -> Kan 'Right t u b b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (a -> t b) -> u b
x ((a -> t b) -> u b)
-> ((b -> t b) -> a -> t b) -> (b -> t b) -> u b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. ((b -> t b) -> (a -> b) -> a -> t b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> b
f)

instance Interpreted (->) (Kan Right t u b) where
	type Primary (Kan Right t u b) a = (a -> t b) -> u b
	run :: ((->) < Kan 'Right t u b a) < Primary (Kan 'Right t u b) a
run ~(Ran x) = Primary (Kan 'Right t u b) a
(a -> t b) -> u b
x
	unite :: ((->) < Primary (Kan 'Right t u b) a) < Kan 'Right t u b a
unite = ((->) < Primary (Kan 'Right t u b) a) < Kan 'Right t u b a
forall (t :: * -> *) (u :: * -> *) b a.
((a -> t b) -> u b) -> Kan 'Right t u b a
Ran