{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE
    TypeFamilies
  , TypeOperators
  , MultiParamTypeClasses
  , FlexibleInstances
  , FlexibleContexts
  , GADTs
  , StandaloneDeriving
  , DeriveAnyClass
  , PolyKinds
  , DefaultSignatures
  , DataKinds
#-}

-- |

-- Module      : OAlg.Data.Variant

-- Description : concept of co- and contra.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- concept of co- and contra.

module OAlg.Data.Variant
  ( -- * Variant

    Variant(..)
  , Variant2(..), toVariant2, vmap2
  , amapVariant2

    -- * Disjunctive

  , Disjunctive(..), Disjunctive2(..)
  , CategoryDisjunctive, CategoryDualisable(..)
  , vInv2

    -- * Proposition

  , prpCategoryDisjunctive
  , prpCategoryDualisable
  ) where

import Data.List ((++))

import OAlg.Prelude

import OAlg.Category.Path
import OAlg.Category.Unify

import OAlg.Data.Either
import OAlg.Data.Proxy

import OAlg.Structure.Oriented  hiding (Path(..))
import OAlg.Structure.Fibred.Root
import OAlg.Structure.Multiplicative
import OAlg.Structure.Number

--------------------------------------------------------------------------------

-- Variant -


-- | concept of co- and contravariant.

data Variant = Covariant | Contravariant
  deriving (Int -> Variant -> ShowS
[Variant] -> ShowS
Variant -> String
(Int -> Variant -> ShowS)
-> (Variant -> String) -> ([Variant] -> ShowS) -> Show Variant
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Variant -> ShowS
showsPrec :: Int -> Variant -> ShowS
$cshow :: Variant -> String
show :: Variant -> String
$cshowList :: [Variant] -> ShowS
showList :: [Variant] -> ShowS
Show,ReadPrec [Variant]
ReadPrec Variant
Int -> ReadS Variant
ReadS [Variant]
(Int -> ReadS Variant)
-> ReadS [Variant]
-> ReadPrec Variant
-> ReadPrec [Variant]
-> Read Variant
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Variant
readsPrec :: Int -> ReadS Variant
$creadList :: ReadS [Variant]
readList :: ReadS [Variant]
$creadPrec :: ReadPrec Variant
readPrec :: ReadPrec Variant
$creadListPrec :: ReadPrec [Variant]
readListPrec :: ReadPrec [Variant]
Read,Variant -> Variant -> Bool
(Variant -> Variant -> Bool)
-> (Variant -> Variant -> Bool) -> Eq Variant
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Variant -> Variant -> Bool
== :: Variant -> Variant -> Bool
$c/= :: Variant -> Variant -> Bool
/= :: Variant -> Variant -> Bool
Eq,Eq Variant
Eq Variant =>
(Variant -> Variant -> Ordering)
-> (Variant -> Variant -> Bool)
-> (Variant -> Variant -> Bool)
-> (Variant -> Variant -> Bool)
-> (Variant -> Variant -> Bool)
-> (Variant -> Variant -> Variant)
-> (Variant -> Variant -> Variant)
-> Ord Variant
Variant -> Variant -> Bool
Variant -> Variant -> Ordering
Variant -> Variant -> Variant
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Variant -> Variant -> Ordering
compare :: Variant -> Variant -> Ordering
$c< :: Variant -> Variant -> Bool
< :: Variant -> Variant -> Bool
$c<= :: Variant -> Variant -> Bool
<= :: Variant -> Variant -> Bool
$c> :: Variant -> Variant -> Bool
> :: Variant -> Variant -> Bool
$c>= :: Variant -> Variant -> Bool
>= :: Variant -> Variant -> Bool
$cmax :: Variant -> Variant -> Variant
max :: Variant -> Variant -> Variant
$cmin :: Variant -> Variant -> Variant
min :: Variant -> Variant -> Variant
Ord,Int -> Variant
Variant -> Int
Variant -> [Variant]
Variant -> Variant
Variant -> Variant -> [Variant]
Variant -> Variant -> Variant -> [Variant]
(Variant -> Variant)
-> (Variant -> Variant)
-> (Int -> Variant)
-> (Variant -> Int)
-> (Variant -> [Variant])
-> (Variant -> Variant -> [Variant])
-> (Variant -> Variant -> [Variant])
-> (Variant -> Variant -> Variant -> [Variant])
-> Enum Variant
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: Variant -> Variant
succ :: Variant -> Variant
$cpred :: Variant -> Variant
pred :: Variant -> Variant
$ctoEnum :: Int -> Variant
toEnum :: Int -> Variant
$cfromEnum :: Variant -> Int
fromEnum :: Variant -> Int
$cenumFrom :: Variant -> [Variant]
enumFrom :: Variant -> [Variant]
$cenumFromThen :: Variant -> Variant -> [Variant]
enumFromThen :: Variant -> Variant -> [Variant]
$cenumFromTo :: Variant -> Variant -> [Variant]
enumFromTo :: Variant -> Variant -> [Variant]
$cenumFromThenTo :: Variant -> Variant -> Variant -> [Variant]
enumFromThenTo :: Variant -> Variant -> Variant -> [Variant]
Enum,Variant
Variant -> Variant -> Bounded Variant
forall a. a -> a -> Bounded a
$cminBound :: Variant
minBound :: Variant
$cmaxBound :: Variant
maxBound :: Variant
Bounded)

instance Validable Variant where
  valid :: Variant -> Statement
valid Variant
Covariant = Statement
SValid
  valid Variant
_         = Statement
SValid

--------------------------------------------------------------------------------

-- Variant - Multiplicative -


type instance Point Variant = ()
instance ShowPoint Variant
instance EqPoint Variant
instance ValidablePoint Variant
instance TypeablePoint Variant
instance Oriented Variant where
  orientation :: Variant -> Orientation (Point Variant)
orientation Variant
_ = () () -> () -> Orientation ()
forall p. p -> p -> Orientation p
:> ()

instance Multiplicative Variant where
  one :: Point Variant -> Variant
one Point Variant
_ = Variant
Covariant
  
  Variant
Covariant * :: Variant -> Variant -> Variant
* Variant
v                 = Variant
v
  Variant
v * Variant
Covariant                 = Variant
v
  Variant
Contravariant * Variant
Contravariant = Variant
Covariant

  npower :: Variant -> N -> Variant
npower Variant
Covariant N
_                      = Variant
Covariant
  npower Variant
Contravariant N
n | N
n N -> N -> N
forall a. Integral a => a -> a -> a
`mod` N
2 N -> N -> Bool
forall a. Eq a => a -> a -> Bool
== N
0 = Variant
Covariant
                         | Bool
otherwise      = Variant
Contravariant

--------------------------------------------------------------------------------

-- Disjunctive -


-- | object having an associated variant.

class Disjunctive x where
  variant :: x -> Variant

--------------------------------------------------------------------------------

-- Disjunctive2 -


-- | two parameterized object having a associated variant.

class Disjunctive2 h where
  variant2 :: h x y -> Variant
  default variant2 :: Disjunctive (h x y) => h x y -> Variant
  variant2 = h x y -> Variant
forall x. Disjunctive x => x -> Variant
variant

instance Disjunctive2 h => Disjunctive2 (Path h) where
  variant2 :: forall x y. Path h x y -> Variant
variant2 (IdPath Struct (ObjectClass h) x
_) = Variant
Covariant
  variant2 (h y1 y
f :. Path h x y1
p)   = h y1 y -> Variant
forall x y. h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h y1 y
f Variant -> Variant -> Variant
forall c. Multiplicative c => c -> c -> c
* Path h x y1 -> Variant
forall x y. Path h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 Path h x y1
p

instance Disjunctive2 h => Disjunctive (Path h x y) where
  variant :: Path h x y -> Variant
variant = Path h x y -> Variant
forall x y. Path h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2

--------------------------------------------------------------------------------

-- Variant2 -


-- | concept of co- and contravariant for two parameterized types.

data Variant2 v h x y where
  Covariant2     :: h x y -> Variant2 Covariant h x y
  Contravariant2 :: h x y -> Variant2 Contravariant h x y

deriving instance Show (h x y) => Show (Variant2 v h x y)

instance Show2 h => Show2 (Variant2 v h) where
  show2 :: forall a b. Variant2 v h a b -> String
show2 (Covariant2 h a b
h) = String
"Covariant2 (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ h a b -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  show2 (Contravariant2 h a b
h) = String
"Contravariant2 (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ h a b -> String
forall a b. h a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 h a b
h String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance Disjunctive2 (Variant2 v h) where
  variant2 :: forall (x :: k) (y :: k). Variant2 v h x y -> Variant
variant2 (Covariant2 h x y
_)     = Variant
Covariant
  variant2 (Contravariant2 h x y
_) = Variant
Contravariant

instance (Disjunctive2 h, Validable (h x y)) => Validable (Variant2 v h x y) where
  valid :: Variant2 v h x y -> Statement
valid Variant2 v h x y
h = String -> Label
Label String
"Variant2" Label -> Statement -> Statement
:<=>: case Variant2 v h x y
h of
    Covariant2 h x y
hCov     -> h x y -> Statement
forall a. Validable a => a -> Statement
valid h x y
hCov Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (h x y -> Variant
forall (x :: k) (y :: k). h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
hCov Variant -> Variant -> Bool
forall a. Eq a => a -> a -> Bool
== Variant
Covariant) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []
    Contravariant2 h x y
hCnt -> h x y -> Statement
forall a. Validable a => a -> Statement
valid h x y
hCnt Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& (h x y -> Variant
forall (x :: k) (y :: k). h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
hCnt Variant -> Variant -> Bool
forall a. Eq a => a -> a -> Bool
== Variant
Contravariant) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []


instance ApplicativeG Id h c => ApplicativeG Id (Variant2 v h) c where
  amapG :: forall x y. Variant2 v h x y -> c (Id x) (Id y)
amapG (Covariant2 h x y
h)     = h x y -> c (Id x) (Id y)
forall x y. h x y -> c (Id x) (Id y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
  amapG (Contravariant2 h x y
h) = h x y -> c (Id x) (Id y)
forall x y. h x y -> c (Id x) (Id y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
  
instance ApplicativeG Pnt h c => ApplicativeG Pnt (Variant2 v h) c where
  amapG :: forall x y. Variant2 v h x y -> c (Pnt x) (Pnt y)
amapG (Covariant2 h x y
h)     = h x y -> c (Pnt x) (Pnt y)
forall x y. h x y -> c (Pnt x) (Pnt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
  amapG (Contravariant2 h x y
h) = h x y -> c (Pnt x) (Pnt y)
forall x y. h x y -> c (Pnt x) (Pnt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h

instance ApplicativeG Rt h c => ApplicativeG Rt (Variant2 v h) c where
  amapG :: forall x y. Variant2 v h x y -> c (Rt x) (Rt y)
amapG (Covariant2 h x y
h)     = h x y -> c (Rt x) (Rt y)
forall x y. h x y -> c (Rt x) (Rt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
  amapG (Contravariant2 h x y
h) = h x y -> c (Rt x) (Rt y)
forall x y. h x y -> c (Rt x) (Rt y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h

instance Disjunctive2 h => Disjunctive2 (Sub s h) where variant2 :: forall x y. Sub s h x y -> Variant
variant2 (Sub h x y
h) = h x y -> Variant
forall x y. h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
h

--------------------------------------------------------------------------------

-- toVariant2 -


-- | mapping to 'Variant2' for a @'Disjunctive2' __h__@.

toVariant2 :: Disjunctive2 h
  => h x y -> Either2 (Variant2 Contravariant h) (Variant2 Covariant h) x y
toVariant2 :: forall (h :: * -> * -> *) x y.
Disjunctive2 h =>
h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
toVariant2 h x y
h = case h x y -> Variant
forall x y. h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
h of
  Variant
Contravariant -> Variant2 'Contravariant h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
forall (f :: * -> * -> *) a b (g :: * -> * -> *).
f a b -> Either2 f g a b
Left2 (h x y -> Variant2 'Contravariant h x y
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Contravariant h x y
Contravariant2 h x y
h)
  Variant
Covariant     -> Variant2 'Covariant h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
forall (g :: * -> * -> *) a b (f :: * -> * -> *).
g a b -> Either2 f g a b
Right2 (h x y -> Variant2 'Covariant h x y
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Covariant h x y
Covariant2 h x y
h)

--------------------------------------------------------------------------------

-- vmap2 -


-- | application on 'Variant2'.

vmap2 :: ApplicativeG t h b => Variant2 v h x y -> b (t x) (t y)
vmap2 :: forall (t :: * -> *) (h :: * -> * -> *) (b :: * -> * -> *)
       (v :: Variant) x y.
ApplicativeG t h b =>
Variant2 v h x y -> b (t x) (t y)
vmap2 (Covariant2 h x y
h)     = h x y -> b (t x) (t y)
forall x y. h x y -> b (t x) (t y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h
vmap2 (Contravariant2 h x y
h) = h x y -> b (t x) (t y)
forall x y. h x y -> b (t x) (t y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h

--------------------------------------------------------------------------------

-- amapVariant2 -


-- | mapping the 'Variant2' by preserving the variance.

amapVariant2 :: (f x y -> g x y) -> Variant2 v f x y -> Variant2 v g x y
amapVariant2 :: forall {k} {k} (f :: k -> k -> *) (x :: k) (y :: k)
       (g :: k -> k -> *) (v :: Variant).
(f x y -> g x y) -> Variant2 v f x y -> Variant2 v g x y
amapVariant2 f x y -> g x y
g (Covariant2 f x y
f)    = g x y -> Variant2 'Covariant g x y
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Covariant h x y
Covariant2 (f x y -> g x y
g f x y
f)
amapVariant2 f x y -> g x y
g (Contravariant2 f x y
f) = g x y -> Variant2 'Contravariant g x y
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (f x y -> g x y
g f x y
f)


--------------------------------------------------------------------------------

-- Variant2 - Morphism -


instance Morphism h => Morphism (Variant2 v h) where
  type ObjectClass (Variant2 v h) = ObjectClass h
  homomorphous :: forall x y.
Variant2 v h x y -> Homomorphous (ObjectClass (Variant2 v h)) x y
homomorphous (Covariant2 h x y
h)     = h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h
  homomorphous (Contravariant2 h x y
h) = h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h

--------------------------------------------------------------------------------

-- CategoryDisjunctive -


-- | disjunctive category.

--

--  __Properties__ Let @'CategoryDisjunctive' __c__@, then holds:

--

-- (1) For all @__x__@ and @s@ in @'Struct' ('ObjectClass' __c__) __x__@ holds:

-- @'variant2' ('cOne' s) '==' 'Covariant'@.

--

-- (2) For all @__x__@, @__y__@, @__z__@, @f@ in @__c y z__@ and @g@ in @__c x y__@ holds:

-- @'variant2' (f '.' g) '==' 'variant2' f '*' 'variant2' g@.

class (Category c, Disjunctive2 c) => CategoryDisjunctive c

instance (Morphism h, Disjunctive2 h) => CategoryDisjunctive (Path h)

instance CategoryDisjunctive h => Category (Variant2 Covariant h) where
  cOne :: forall x.
Struct (ObjectClass (Variant2 'Covariant h)) x
-> Variant2 'Covariant h x x
cOne = h x x -> Variant2 'Covariant h x x
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Covariant h x y
Covariant2 (h x x -> Variant2 'Covariant h x x)
-> (Struct (ObjectClass h) x -> h x x)
-> Struct (ObjectClass h) x
-> Variant2 'Covariant h x x
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (ObjectClass h) x -> h x x
forall x. Struct (ObjectClass h) x -> h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne
  Covariant2 h y z
f . :: forall y z x.
Variant2 'Covariant h y z
-> Variant2 'Covariant h x y -> Variant2 'Covariant h x z
. Covariant2 h x y
g = h x z -> Variant2 'Covariant h x z
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Covariant h x y
Covariant2 (h y z
f h y z -> h x y -> h x z
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x y
g)

instance CategoryDisjunctive h => Disjunctive2 (Inv2 h) where
  variant2 :: forall x y. Inv2 h x y -> Variant
variant2 (Inv2 h x y
f h y x
_) = h x y -> Variant
forall x y. h x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 h x y
f

instance CategoryDisjunctive c => CategoryDisjunctive (Inv2 c)

instance (CategoryDisjunctive c, TransformableObjectClass s c) => CategoryDisjunctive (Sub s c)
--------------------------------------------------------------------------------

-- vInv2 -


-- | the inverse 'Variant2'.

vInv2 :: CategoryDisjunctive c => Variant2 v (Inv2 c) x y -> Variant2 v (Inv2 c) y x
vInv2 :: forall (c :: * -> * -> *) (v :: Variant) x y.
CategoryDisjunctive c =>
Variant2 v (Inv2 c) x y -> Variant2 v (Inv2 c) y x
vInv2 (Covariant2 Inv2 c x y
i) = Inv2 c y x -> Variant2 'Covariant (Inv2 c) y x
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Covariant h x y
Covariant2 (Inv2 c x y -> Inv2 c y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 c x y
i)
vInv2 (Contravariant2 Inv2 c x y
i) = Inv2 c y x -> Variant2 'Contravariant (Inv2 c) y x
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (Inv2 c x y -> Inv2 c y x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 Inv2 c x y
i)

--------------------------------------------------------------------------------

-- prpCategoryDisjunctiveOne -


relCategoryDisjunctiveOne :: (CategoryDisjunctive c, ObjectClass c ~ s)
  => q c -> Struct s x -> Statement
relCategoryDisjunctiveOne :: forall (c :: * -> * -> *) s (q :: (* -> * -> *) -> *) x.
(CategoryDisjunctive c, ObjectClass c ~ s) =>
q c -> Struct s x -> Statement
relCategoryDisjunctiveOne q c
q Struct s x
s = (c x x -> Variant
forall x y. c x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 (q c -> Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' q c
q Struct s x
Struct (ObjectClass c) x
s) Variant -> Variant -> Bool
forall a. Eq a => a -> a -> Bool
== Variant
Covariant) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params []

relCategoryDisjunctiveMlt :: (CategoryDisjunctive c, Show2 c)
  => c y z -> c x y -> Statement
relCategoryDisjunctiveMlt :: forall (c :: * -> * -> *) y z x.
(CategoryDisjunctive c, Show2 c) =>
c y z -> c x y -> Statement
relCategoryDisjunctiveMlt c y z
f c x y
g
  = (c x z -> Variant
forall x y. c x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 (c y z
f c y z -> c x y -> c x z
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
g) Variant -> Variant -> Bool
forall a. Eq a => a -> a -> Bool
== c y z -> Variant
forall x y. c x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 c y z
f Variant -> Variant -> Variant
forall c. Multiplicative c => c -> c -> c
* c x y -> Variant
forall x y. c x y -> Variant
forall {k} {k} (h :: k -> k -> *) (x :: k) (y :: k).
Disjunctive2 h =>
h x y -> Variant
variant2 c x y
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c y z -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y z
f,String
"g"String -> String -> Parameter
:=c x y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
g]

-- | validity according to 'CategoryDisjunctive'.

prpCategoryDisjunctive :: (CategoryDisjunctive c, Show2 c)
  => X (SomeObjectClass c) -> X (SomeCmpb2 c) -> Statement
prpCategoryDisjunctive :: forall (c :: * -> * -> *).
(CategoryDisjunctive c, Show2 c) =>
X (SomeObjectClass c) -> X (SomeCmpb2 c) -> Statement
prpCategoryDisjunctive X (SomeObjectClass c)
xs X (SomeCmpb2 c)
xfg = String -> Label
Prp String
"CategoryDisjunctive" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: X (SomeObjectClass c)
-> (SomeObjectClass c -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeObjectClass c)
xs (\(SomeObjectClass Struct (ObjectClass c) x
s) -> Proxy c -> Struct (ObjectClass c) x -> Statement
forall (c :: * -> * -> *) s (q :: (* -> * -> *) -> *) x.
(CategoryDisjunctive c, ObjectClass c ~ s) =>
q c -> Struct s x -> Statement
relCategoryDisjunctiveOne Proxy c
q Struct (ObjectClass c) x
s)
      , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: X (SomeCmpb2 c) -> (SomeCmpb2 c -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeCmpb2 c)
xfg (\(SomeCmpb2 c y z
f c x y
g) -> c y z -> c x y -> Statement
forall (c :: * -> * -> *) y z x.
(CategoryDisjunctive c, Show2 c) =>
c y z -> c x y -> Statement
relCategoryDisjunctiveMlt c y z
f c x y
g)
      ]
  where
    q :: Proxy c
q = X (SomeObjectClass c) -> Proxy c
forall (c :: * -> * -> *). X (SomeObjectClass c) -> Proxy c
qCat X (SomeObjectClass c)
xs
    
    qCat :: X (SomeObjectClass c) -> Proxy c
    qCat :: forall (c :: * -> * -> *). X (SomeObjectClass c) -> Proxy c
qCat X (SomeObjectClass c)
_ = Proxy c
forall {k} (t :: k). Proxy t
Proxy

--------------------------------------------------------------------------------

-- CategoryDualisable -


-- | disjunctive category admitting duality morphisms.

--

-- __Property__ Let @'CategoryDualisable' __o h__@, then for all @__x__@ and @s@ in

-- @'Struct' ('ObjectClass __h__) __x__@holds:

--

-- (1) @f '.' t '.=.' 'cOne' ('domain' t)@.

--

-- (2) @t '.' f '.=.' 'cOne' ('domain' f)@.

--

-- where @'Contravariant2' t = 'cToDual' s@ and @'Contravariant2' f = 'cFromDual' s@.

class CategoryDisjunctive h => CategoryDualisable o h where
  cToDual :: Struct (ObjectClass h) x -> Variant2 Contravariant h x (o x)
  cFromDual :: Struct (ObjectClass h) x -> Variant2 Contravariant h (o x) x

--------------------------------------------------------------------------------

-- cToDual' -


cToDual' :: CategoryDualisable o h
  => q o h -> Struct (ObjectClass h) x -> Variant2 Contravariant h x (o x)
cToDual' :: forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
CategoryDualisable o h =>
q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
cToDual' q o h
_ = Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
forall x.
Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
cToDual

--------------------------------------------------------------------------------

-- cFromDual' -


cFromDual' :: CategoryDualisable o h
  => q o h -> Struct (ObjectClass h) x -> Variant2 Contravariant h (o x) x
cFromDual' :: forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
CategoryDualisable o h =>
q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
cFromDual' q o h
_ = Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
forall x.
Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
forall (o :: * -> *) (h :: * -> * -> *) x.
CategoryDualisable o h =>
Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
cFromDual

--------------------------------------------------------------------------------

-- prpCategoryDualisable o h -


relCategoryDualisable :: (CategoryDualisable o h, EqExt h)
  => q o h -> Struct (ObjectClass h) x -> Statement
relCategoryDualisable :: forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
(CategoryDualisable o h, EqExt h) =>
q o h -> Struct (ObjectClass h) x -> Statement
relCategoryDualisable q o h
q Struct (ObjectClass h) x
s 
  = [Statement] -> Statement
And [ String -> Label
Label String
"1" Label -> Statement -> Statement
:<=>: (h (o x) x
f h (o x) x -> h x (o x) -> h x x
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h x (o x)
t h x x -> h x x -> Statement
forall x y. h x y -> h x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. Struct (ObjectClass h) x -> h x x
forall x. Struct (ObjectClass h) x -> h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (h x (o x) -> Struct (ObjectClass h) x
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h x (o x)
t))
        , String -> Label
Label String
"2" Label -> Statement -> Statement
:<=>: (h x (o x)
t h x (o x) -> h (o x) x -> h (o x) (o x)
forall y z x. h y z -> h x y -> h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. h (o x) x
f h (o x) (o x) -> h (o x) (o x) -> Statement
forall x y. h x y -> h x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. Struct (ObjectClass h) (o x) -> h (o x) (o x)
forall x. Struct (ObjectClass h) x -> h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (h (o x) x -> Struct (ObjectClass h) (o x)
forall x y. h x y -> Struct (ObjectClass h) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain h (o x) x
f))
        ]
  where Contravariant2 h x (o x)
t = q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
CategoryDualisable o h =>
q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
cToDual' q o h
q Struct (ObjectClass h) x
s
        Contravariant2 h (o x) x
f = q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
CategoryDualisable o h =>
q o h
-> Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
cFromDual' q o h
q Struct (ObjectClass h) x
s

-- | validity according to 'CategoryDualisable'.

prpCategoryDualisable :: (CategoryDualisable o h, EqExt h)
  -- => q o h -> Struct (ObjectClass h) x -> Statement

  => q o h -> X (SomeObjectClass h) -> Statement
prpCategoryDualisable :: forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *).
(CategoryDualisable o h, EqExt h) =>
q o h -> X (SomeObjectClass h) -> Statement
prpCategoryDualisable q o h
q X (SomeObjectClass h)
xo = String -> Label
Prp String
"CategoryDualisable" Label -> Statement -> Statement
:<=>: X (SomeObjectClass h)
-> (SomeObjectClass h -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeObjectClass h)
xo
  (\(SomeObjectClass Struct (ObjectClass h) x
s) -> q o h -> Struct (ObjectClass h) x -> Statement
forall (o :: * -> *) (h :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> *) x.
(CategoryDualisable o h, EqExt h) =>
q o h -> Struct (ObjectClass h) x -> Statement
relCategoryDualisable q o h
q Struct (ObjectClass h) x
s)