module Pandora.Paradigm.Primary.Functor.Convergence where import Pandora.Pattern.Category ((<--)) import Pandora.Pattern.Morphism.Straight (Straight (Straight)) import Pandora.Pattern.Functor.Contravariant (Contravariant ((>-|-))) import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult)) import Pandora.Pattern.Functor.Monoidal (Monoidal (unit)) import Pandora.Pattern.Object.Semigroup (Semigroup ((+))) import Pandora.Pattern.Object.Monoid (Monoid (zero)) import Pandora.Paradigm.Algebraic.Exponential (type (-->), type (<--)) import Pandora.Paradigm.Algebraic.Product ((:*:)((:*:))) import Pandora.Paradigm.Algebraic () 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 :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \a x a y -> b -> b -> r g (b -> b -> r) -> b -> b -> r forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- a -> b f a x (b -> r) -> b -> r forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- a -> b f a y instance Semigroup r => Semimonoidal (-->) (:*:) (:*:) (Convergence r) where mult :: (Convergence r a :*: Convergence r b) --> Convergence r (a :*: b) mult = ((Convergence r a :*: Convergence r b) -> Convergence r (a :*: b)) -> (Convergence r a :*: Convergence r b) --> Convergence r (a :*: b) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((Convergence r a :*: Convergence r b) -> Convergence r (a :*: b)) -> (Convergence r a :*: Convergence r b) --> Convergence r (a :*: b)) -> ((Convergence r a :*: Convergence r b) -> Convergence r (a :*: b)) -> (Convergence r a :*: Convergence r b) --> Convergence r (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(Convergence a -> a -> r f :*: Convergence b -> b -> r g) -> ((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b) forall r a. (a -> a -> r) -> Convergence r a Convergence (((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b)) -> ((a :*: b) -> (a :*: b) -> r) -> Convergence r (a :*: b) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \(a a :*: b b) (a a' :*: b b') -> a -> a -> r f a a a a' r -> r -> r forall a. Semigroup a => a -> a -> a + b -> b -> r g b b b b' instance Monoid r => Monoidal (-->) (<--) (:*:) (:*:) (Convergence r) where unit :: Proxy (:*:) -> (Unit (:*:) <-- a) --> Convergence r a unit Proxy (:*:) _ = ((One <-- a) -> Convergence r a) -> Straight (->) (One <-- a) (Convergence r a) forall (v :: * -> * -> *) a e. v a e -> Straight v a e Straight (((One <-- a) -> Convergence r a) -> Straight (->) (One <-- a) (Convergence r a)) -> ((One <-- a) -> Convergence r a) -> Straight (->) (One <-- a) (Convergence r a) forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \One <-- a _ -> (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 :: * -> * -> *) a b. Category m => m (m a b) (m a b) <-- \a _ a _ -> r forall a. Monoid a => a zero