module Pandora.Paradigm.Primary.Functor.Exactly where

import Pandora.Core.Interpreted ((<~))
import Pandora.Pattern.Semigroupoid ((.))
import Pandora.Pattern.Category ((<--), (<---), (<----))
import Pandora.Pattern.Morphism.Flip (Flip (Flip))
import Pandora.Pattern.Morphism.Straight (Straight (Straight))
import Pandora.Pattern.Functor.Covariant (Covariant ((<-|-)))
import Pandora.Pattern.Functor.Traversable (Traversable ((<-/-)))
import Pandora.Pattern.Functor.Semimonoidal (Semimonoidal (mult))
import Pandora.Pattern.Functor.Monoidal (Monoidal (unit))
import Pandora.Pattern.Functor.Bindable (Bindable ((=<<)))
import Pandora.Pattern.Functor.Extendable (Extendable ((<<=)))
import Pandora.Pattern.Functor.Representable (Representable (Representation, (<#>), tabulate))
import Pandora.Pattern.Functor.Monad (Monad)
import Pandora.Pattern.Functor.Comonad (Comonad)
import Pandora.Pattern.Functor.Adjoint (Adjoint ((-|), (|-)))
import Pandora.Pattern.Object.Setoid (Setoid ((==)))
import Pandora.Pattern.Object.Chain (Chain ((<=>)))
import Pandora.Pattern.Object.Semigroup (Semigroup ((+)))
import Pandora.Pattern.Object.Monoid (Monoid (zero))
import Pandora.Pattern.Object.Ringoid (Ringoid ((*)))
import Pandora.Pattern.Object.Quasiring (Quasiring (one))
import Pandora.Pattern.Object.Semilattice (Infimum ((/\)), Supremum ((\/)))
import Pandora.Pattern.Object.Lattice (Lattice)
import Pandora.Pattern.Object.Group (Group (invert))
import Pandora.Paradigm.Algebraic.Exponential (type (<--), type (-->))
import Pandora.Paradigm.Algebraic.Product ((:*:) ((:*:)))
import Pandora.Paradigm.Algebraic.One (One (One))
import Pandora.Paradigm.Algebraic (extract, (<-||-))

newtype Exactly a = Exactly a

instance Covariant (->) (->) Exactly where
	a -> b
f <-|- :: (a -> b) -> Exactly a -> Exactly b
<-|- Exactly a
x = b -> Exactly b
forall a. a -> Exactly a
Exactly (b -> Exactly b) -> b -> Exactly b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> b
f a
x

instance Semimonoidal (-->) (:*:) (:*:) Exactly where
	mult :: (Exactly a :*: Exactly b) --> Exactly (a :*: b)
mult = ((Exactly a :*: Exactly b) -> Exactly (a :*: b))
-> (Exactly a :*: Exactly b) --> Exactly (a :*: b)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (((Exactly a :*: Exactly b) -> Exactly (a :*: b))
 -> (Exactly a :*: Exactly b) --> Exactly (a :*: b))
-> ((Exactly a :*: Exactly b) -> Exactly (a :*: b))
-> (Exactly a :*: Exactly b) --> Exactly (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- (a :*: b) -> Exactly (a :*: b)
forall a. a -> Exactly a
Exactly ((a :*: b) -> Exactly (a :*: b))
-> ((Exactly a :*: Exactly b) -> a :*: b)
-> (Exactly a :*: Exactly b)
-> Exactly (a :*: b)
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Exactly a -> a
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly a -> a) -> (Exactly a :*: b) -> a :*: b
forall (m :: * -> * -> *) (p :: * -> * -> *) a b c.
(Covariant m m (Flip p c), Interpreted m (Flip p c)) =>
m a b -> m (p a c) (p b c)
<-||-) ((Exactly a :*: b) -> a :*: b)
-> ((Exactly a :*: Exactly b) -> Exactly a :*: b)
-> (Exactly a :*: Exactly b)
-> a :*: b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
.  (Exactly b -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly b -> b) -> (Exactly a :*: Exactly b) -> Exactly a :*: b
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|-)

instance Monoidal (-->) (-->) (:*:) (:*:) Exactly where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) --> Exactly a
unit Proxy (:*:)
_ = (Straight (->) One a -> Exactly a)
-> Straight (->) (Straight (->) One a) (Exactly a)
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight ((Straight (->) One a -> Exactly a)
 -> Straight (->) (Straight (->) One a) (Exactly a))
-> (Straight (->) One a -> Exactly a)
-> Straight (->) (Straight (->) One a) (Exactly a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a)
-> (Straight (->) One a -> a) -> Straight (->) One a -> Exactly a
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. (Straight (->) One a -> One -> a
forall (m :: * -> * -> *) (t :: * -> *) a.
Interpreted m t =>
(m < t a) < Primary t a
<~ One
One)

instance Semimonoidal (<--) (:*:) (:*:) Exactly where
	mult :: (Exactly a :*: Exactly b) <-- Exactly (a :*: b)
mult = (Exactly (a :*: b) -> Exactly a :*: Exactly b)
-> (Exactly a :*: Exactly b) <-- Exactly (a :*: b)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Exactly (a :*: b) -> Exactly a :*: Exactly b)
 -> (Exactly a :*: Exactly b) <-- Exactly (a :*: b))
-> (Exactly (a :*: b) -> Exactly a :*: Exactly b)
-> (Exactly a :*: Exactly b) <-- Exactly (a :*: b)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Exactly (a
x :*: b
y)) -> a -> Exactly a
forall a. a -> Exactly a
Exactly a
x Exactly a -> Exactly b -> Exactly a :*: Exactly b
forall s a. s -> a -> s :*: a
:*: b -> Exactly b
forall a. a -> Exactly a
Exactly b
y

instance Monoidal (<--) (-->) (:*:) (:*:) Exactly where
	unit :: Proxy (:*:) -> (Unit (:*:) --> a) <-- Exactly a
unit Proxy (:*:)
_ = (Exactly a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Exactly a)
forall (v :: * -> * -> *) a e. v e a -> Flip v a e
Flip ((Exactly a -> Straight (->) One a)
 -> Flip (->) (Straight (->) One a) (Exactly a))
-> (Exactly a -> Straight (->) One a)
-> Flip (->) (Straight (->) One a) (Exactly a)
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- \(Exactly a
x) -> (One -> a) -> Straight (->) One a
forall (v :: * -> * -> *) a e. v a e -> Straight v a e
Straight (\One
_ -> a
x)

instance Traversable (->) (->) Exactly where
	a -> u b
f <-/- :: (a -> u b) -> Exactly a -> u (Exactly b)
<-/- Exactly a
x = b -> Exactly b
forall a. a -> Exactly a
Exactly (b -> Exactly b) -> u b -> u (Exactly b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- a -> u b
f a
x

instance Bindable (->) Exactly where
	a -> Exactly b
f =<< :: (a -> Exactly b) -> Exactly a -> Exactly b
=<< Exactly a
x = a -> Exactly b
f a
x

instance Monad (->) Exactly

instance Extendable (->) Exactly where
	Exactly a -> b
f <<= :: (Exactly a -> b) -> Exactly a -> Exactly b
<<= Exactly a
x = b -> Exactly b
forall a. a -> Exactly a
Exactly (b -> Exactly b) -> (Exactly a -> b) -> Exactly a -> Exactly b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> b
f (Exactly a -> Exactly b) -> Exactly a -> Exactly b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Exactly a
x

instance Comonad (->) Exactly

instance Representable Exactly where
	type Representation Exactly = ()
	() <#> :: Representation Exactly -> a <:= Exactly
<#> Exactly a
x = a
x
	tabulate :: (Representation Exactly -> a) -> Exactly a
tabulate Representation Exactly -> a
f = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- Representation Exactly -> a
f ()

instance Adjoint (->) (->) Exactly Exactly where
	Exactly a -> b
f -| :: (Exactly a -> b) -> a -> Exactly b
-| a
x = b -> Exactly b
forall a. a -> Exactly a
Exactly (b -> Exactly b) -> (a -> b) -> a -> Exactly b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly a -> b
f (Exactly a -> b) -> (a -> Exactly a) -> a -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly b) -> a -> Exactly b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
x
	a -> Exactly b
g |- :: (a -> Exactly b) -> Exactly a -> b
|- Exactly a
x = Exactly b -> b
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly b -> b)
-> (Exactly (Exactly b) -> Exactly b) -> Exactly (Exactly b) -> b
forall (m :: * -> * -> *) b c a.
Semigroupoid m =>
m b c -> m a b -> m a c
. Exactly (Exactly b) -> Exactly b
forall (t :: * -> *) a. Extractable t => t a -> a
extract (Exactly (Exactly b) -> b) -> Exactly (Exactly b) -> b
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<---- a -> Exactly b
g (a -> Exactly b) -> Exactly a -> Exactly (Exactly b)
forall (source :: * -> * -> *) (target :: * -> * -> *)
       (t :: * -> *) a b.
Covariant source target t =>
source a b -> target (t a) (t b)
<-|- Exactly a
x

instance Setoid a => Setoid (Exactly a) where
	Exactly a
x == :: Exactly a -> Exactly a -> Boolean
== Exactly a
y = a
x a -> a -> Boolean
forall a. Setoid a => a -> a -> Boolean
== a
y

instance Chain a => Chain (Exactly a) where
	Exactly a
x <=> :: Exactly a -> Exactly a -> Ordering
<=> Exactly a
y = a
x a -> a -> Ordering
forall a. Chain a => a -> a -> Ordering
<=> a
y

instance Semigroup a => Semigroup (Exactly a) where
	Exactly a
x + :: Exactly a -> Exactly a -> Exactly a
+ Exactly a
y = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
+ a
y

instance Monoid a => Monoid (Exactly a) where
	 zero :: Exactly a
zero = a -> Exactly a
forall a. a -> Exactly a
Exactly a
forall a. Monoid a => a
zero

instance Ringoid a => Ringoid (Exactly a) where
	Exactly a
x * :: Exactly a -> Exactly a -> Exactly a
* Exactly a
y = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<--- a
x a -> a -> a
forall a. Ringoid a => a -> a -> a
* a
y

instance Quasiring a => Quasiring (Exactly a) where
	 one :: Exactly a
one = a -> Exactly a
forall a. a -> Exactly a
Exactly a
forall a. Quasiring a => a
one

instance Infimum a => Infimum (Exactly a) where
	Exactly a
x /\ :: Exactly a -> Exactly a -> Exactly a
/\ Exactly a
y = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
x a -> a -> a
forall a. Infimum a => a -> a -> a
/\ a
y

instance Supremum a => Supremum (Exactly a) where
	Exactly a
x \/ :: Exactly a -> Exactly a -> Exactly a
\/ Exactly a
y = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a
x a -> a -> a
forall a. Supremum a => a -> a -> a
\/ a
y

instance Lattice a => Lattice (Exactly a) where

instance Group a => Group (Exactly a) where
	invert :: Exactly a -> Exactly a
invert (Exactly a
x) = a -> Exactly a
forall a. a -> Exactly a
Exactly (a -> Exactly a) -> a -> Exactly a
forall (m :: * -> * -> *) a b. Category m => m (m a b) (m a b)
<-- a -> a
forall a. Group a => a -> a
invert a
x