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'