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'