module Pandora.Paradigm.Primary.Functor.Convergence where import Pandora.Pattern.Category (($), (/)) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>$<))) import Pandora.Pattern.Functor.Divisible (Divisible ((>*<))) import Pandora.Pattern.Object.Ringoid (Ringoid ((*))) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:))) data Convergence r a = Convergence (a -> a -> r) instance Contravariant (Convergence r) where a -> b f >$< :: (a -> b) -> Convergence r b -> Convergence r a >$< Convergence b -> b -> r g = (a -> a -> r) -> Convergence r a forall r a. (a -> a -> r) -> Convergence r a Convergence ((a -> a -> r) -> Convergence r a) -> (a -> a -> r) -> Convergence r a forall (m :: * -> * -> *). Category m => m ~~> m $ \a x a y -> b -> b -> r g (b -> b -> r) -> b -> b -> r forall (m :: * -> * -> *). Category m => m ~~> m / a -> b f a x (b -> r) -> b -> r forall (m :: * -> * -> *). Category m => m ~~> m / a -> b f a y instance Ringoid r => Divisible (Convergence r) where Convergence b -> b -> r g >*< :: Convergence r b -> Convergence r c -> Convergence r (b :*: c) >*< Convergence c -> c -> r h = ((b :*: c) -> (b :*: c) -> r) -> Convergence r (b :*: c) forall r a. (a -> a -> r) -> Convergence r a Convergence (((b :*: c) -> (b :*: c) -> r) -> Convergence r (b :*: c)) -> ((b :*: c) -> (b :*: c) -> r) -> Convergence r (b :*: c) forall (m :: * -> * -> *). Category m => m ~~> m $ \(b x :*: c x') (b y :*: c y') -> b -> b -> r g b x b y r -> r -> r forall a. Ringoid a => a -> a -> a * c -> c -> r h c x' c y'