module Pandora.Paradigm.Primary.Functor.Equivalence 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.Object.Boolean (Boolean) import Pandora.Paradigm.Primary.Functor.Product (Product ((:*:))) data Equivalence a = Equivalence (a -> a -> Boolean) instance Contravariant Equivalence where a -> b f >$< :: (a -> b) -> Equivalence b -> Equivalence a >$< Equivalence b -> b -> Boolean g = (a -> a -> Boolean) -> Equivalence a forall a. (a -> a -> Boolean) -> Equivalence a Equivalence ((a -> a -> Boolean) -> Equivalence a) -> (a -> a -> Boolean) -> Equivalence a forall (m :: * -> * -> *). Category m => m ~~> m $ \a x a y -> b -> b -> Boolean g (b -> b -> Boolean) -> b -> b -> Boolean forall (m :: * -> * -> *). Category m => m ~~> m / a -> b f a x (b -> Boolean) -> b -> Boolean forall (m :: * -> * -> *). Category m => m ~~> m / a -> b f a y instance Divisible Equivalence where Equivalence b -> b -> Boolean g >*< :: Equivalence b -> Equivalence c -> Equivalence (b :*: c) >*< Equivalence c -> c -> Boolean h = ((b :*: c) -> (b :*: c) -> Boolean) -> Equivalence (b :*: c) forall a. (a -> a -> Boolean) -> Equivalence a Equivalence (((b :*: c) -> (b :*: c) -> Boolean) -> Equivalence (b :*: c)) -> ((b :*: c) -> (b :*: c) -> Boolean) -> Equivalence (b :*: c) forall (m :: * -> * -> *). Category m => m ~~> m $ \(b x :*: c x') (b y :*: c y') -> b -> b -> Boolean g b x b y Boolean -> Boolean -> Boolean forall a. Ringoid a => a -> a -> a * c -> c -> Boolean h c x' c y'