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