{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ConstraintKinds #-}


-- |

-- Module      : OAlg.Category.SDuality

-- Description : functor for dualisable structured types.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- functor for dualisable parameterized types over structured types.

module OAlg.Category.SDuality
  (
    -- * Dual

    -- ** Dualisable

    SVal(..), smap
    
    -- ** Bi-Dualisable

  , SDualBi(..), smapBi, vmapBi
  
  , ShowDual1, EqDual1, ValidableDual1

    -- * Duality Operator

  , SHom()
  , sCov
  , sForget
  , sToDual, sToDual'
  , sFromDual, sFromDual'
    
  , SMorphism(..)
  , PathSMorphism, rdcPathSMorphism

    -- * X

  , xSDualBi
  , xSctSomeMrph
  , xSctSomeCmpb2

  ) where

import Control.Monad
import Control.Applicative ((<|>))

import Data.List ((++))

import OAlg.Prelude

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

import OAlg.Data.Reducible
import OAlg.Data.Constructable
import OAlg.Data.Either
import OAlg.Data.Variant

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

-- SMorphism -


-- | adjoining to a type family @__h__@ of morphisms two auxiliary morphisms 'SToDual' and 'SFromDual'.

data SMorphism r s o h x y where
  SCov      :: Transformable (ObjectClass h) s => h x y -> SMorphism r s o h x y
  SToDual   :: (Structure s x, Structure s (o x)) => SMorphism r s o h x (o x)
  SFromDual :: (Structure s x, Structure s (o x)) =>  SMorphism r s o h (o x) x

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

-- smpBaseDomain -


smpBaseDomain :: (Morphism h, Transformable s r) => SMorphism r s o h x y -> Struct r x
smpBaseDomain :: forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r x
smpBaseDomain = Struct s x -> Struct r x
forall x. Struct s x -> Struct r x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s x -> Struct r x)
-> (SMorphism r s o h x y -> Struct s x)
-> SMorphism r s o h x y
-> Struct r 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
. SMorphism r s o h x y -> Struct s x
SMorphism r s o h x y -> Struct (ObjectClass (SMorphism r s o h)) x
forall x y.
SMorphism r s o h x y -> Struct (ObjectClass (SMorphism r s o h)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain

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

-- smpBaseRange -


smpBaseRange :: (Morphism h, Transformable s r) => SMorphism r s o h x y -> Struct r y
smpBaseRange :: forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r y
smpBaseRange = Struct s y -> Struct r y
forall x. Struct s x -> Struct r x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (Struct s y -> Struct r y)
-> (SMorphism r s o h x y -> Struct s y)
-> SMorphism r s o h x y
-> Struct r y
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
. SMorphism r s o h x y -> Struct s y
SMorphism r s o h x y -> Struct (ObjectClass (SMorphism r s o h)) y
forall x y.
SMorphism r s o h x y -> Struct (ObjectClass (SMorphism r s o h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range

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

-- SCov - Disjunctive -


instance Disjunctive (SMorphism r s o h x y) where
  variant :: SMorphism r s o h x y -> Variant
variant (SCov h x y
_) = Variant
Covariant
  variant SMorphism r s o h x y
_        = Variant
Contravariant

instance Disjunctive2 (SMorphism r s o h)

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

-- SCov - Entity2 -


instance Show2 h => Show2 (SMorphism r s o h) where
  show2 :: forall a b. SMorphism r s o h a b -> String
show2 (SCov h a b
h)  = String
"SCov (" String -> String -> String
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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  show2 SMorphism r s o h a b
SToDual   = String
"SToDual"
  show2 SMorphism r s o h a b
SFromDual = String
"SFromDual"

instance Eq2 h => Eq2 (SMorphism r s o h) where
  eq2 :: forall x y. SMorphism r s o h x y -> SMorphism r s o h x y -> Bool
eq2 (SCov h x y
f) (SCov h x y
g)   = h x y -> h x y -> Bool
forall x y. h x y -> h x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2 h x y
f h x y
g
  eq2 SMorphism r s o h x y
SToDual SMorphism r s o h x y
SToDual     = Bool
True
  eq2 SMorphism r s o h x y
SFromDual SMorphism r s o h x y
SFromDual = Bool
True
  eq2 SMorphism r s o h x y
_ SMorphism r s o h x y
_                 = Bool
False

instance Validable2 h => Validable2 (SMorphism r s o h) where
  valid2 :: forall x y. SMorphism r s o h x y -> Statement
valid2 (SCov h x y
h) = h x y -> Statement
forall x y. h x y -> Statement
forall (h :: * -> * -> *) x y. Validable2 h => h x y -> Statement
valid2 h x y
h
  valid2 SMorphism r s o h x y
_        = Statement
SValid

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

-- SCov - Morphism -


instance Morphism h => Morphism (SMorphism r s o h) where
  type ObjectClass (SMorphism r s o h) = s

  homomorphous :: forall x y.
SMorphism r s o h x y
-> Homomorphous (ObjectClass (SMorphism r s o h)) x y
homomorphous (SCov h x y
h)  = Homomorphous (ObjectClass h) x y -> Homomorphous s x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (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 SMorphism r s o h x y
SToDual   = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct
  homomorphous SMorphism r s o h x y
SFromDual = Struct s x
forall s x. Structure s x => Struct s x
Struct Struct s x -> Struct s y -> Homomorphous s x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct s y
forall s x. Structure s x => Struct s x
Struct

instance Transformable s Typ => TransformableObjectClassTyp (SMorphism r s o h)

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

-- smpForget -


smpForgetStruct :: (Transformable (ObjectClass h) t)
  => Homomorphous t x y -> SMorphism r s o h x y -> SMorphism r t o h x y
smpForgetStruct :: forall (h :: * -> * -> *) t x y r s (o :: * -> *).
Transformable (ObjectClass h) t =>
Homomorphous t x y
-> SMorphism r s o h x y -> SMorphism r t o h x y
smpForgetStruct (Struct t x
Struct:>:Struct t y
Struct) SMorphism r s o h x y
m = case SMorphism r s o h x y
m of
  SCov h x y
h -> h x y -> SMorphism r t o h x y
forall (h :: * -> * -> *) s x y r (o :: * -> *).
Transformable (ObjectClass h) s =>
h x y -> SMorphism r s o h x y
SCov h x y
h
  SMorphism r s o h x y
SToDual     -> SMorphism r t o h x y
SMorphism r t o h x (o x)
forall s x (o :: * -> *) r (h :: * -> * -> *).
(Structure s x, Structure s (o x)) =>
SMorphism r s o h x (o x)
SToDual
  SMorphism r s o h x y
SFromDual   -> SMorphism r t o h x y
SMorphism r t o h (o y) y
forall s x (o :: * -> *) r (h :: * -> * -> *).
(Structure s x, Structure s (o x)) =>
SMorphism r s o h (o x) x
SFromDual

smpForget :: (Morphism h, Transformable (ObjectClass h) t, Transformable s t)
  => SMorphism r s o h x y -> SMorphism r t o h x y
smpForget :: forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
SMorphism r s o h x y -> SMorphism r t o h x y
smpForget SMorphism r s o h x y
m = Homomorphous t x y
-> SMorphism r s o h x y -> SMorphism r t o h x y
forall (h :: * -> * -> *) t x y r s (o :: * -> *).
Transformable (ObjectClass h) t =>
Homomorphous t x y
-> SMorphism r s o h x y -> SMorphism r t o h x y
smpForgetStruct (Homomorphous s x y -> Homomorphous t x y
forall s t x y.
Transformable s t =>
Homomorphous s x y -> Homomorphous t x y
tauHom (Homomorphous s x y -> Homomorphous t x y)
-> Homomorphous s x y -> Homomorphous t x y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SMorphism r s o h x y
-> Homomorphous (ObjectClass (SMorphism r s o h)) x y
forall x y.
SMorphism r s o h x y
-> Homomorphous (ObjectClass (SMorphism r s o h)) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous SMorphism r s o h x y
m) SMorphism r s o h x y
m

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

-- PathSCov -


-- | path of 'SCov'.

type PathSMorphism r s o h = Path (SMorphism r s o h)

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

-- smpPathForget -


smpPathForget :: (Morphism h, Transformable (ObjectClass h) t, Transformable s t)
  => PathSMorphism r s o h x y -> PathSMorphism r t o h x y
smpPathForget :: forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
PathSMorphism r s o h x y -> PathSMorphism r t o h x y
smpPathForget PathSMorphism r s o h x y
p = case PathSMorphism r s o h x y
p of
  IdPath Struct (ObjectClass (SMorphism r s o h)) x
s -> Struct (ObjectClass (SMorphism r t o h)) x
-> Path (SMorphism r t o h) x x
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath (Struct s x -> Struct t x
forall x. Struct s x -> Struct t x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct s x
Struct (ObjectClass (SMorphism r s o h)) x
s)
  SMorphism r s o h y1 y
m :. Path (SMorphism r s o h) x y1
p'  -> SMorphism r s o h y1 y -> SMorphism r t o h y1 y
forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
SMorphism r s o h x y -> SMorphism r t o h x y
smpForget SMorphism r s o h y1 y
m SMorphism r t o h y1 y
-> Path (SMorphism r t o h) x y1 -> PathSMorphism r t o h x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Path (SMorphism r s o h) x y1 -> Path (SMorphism r t o h) x y1
forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
PathSMorphism r s o h x y -> PathSMorphism r t o h x y
smpPathForget Path (SMorphism r s o h) x y1
p'

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

-- rdcPathSMorphism -


-- | reducing a path of 'SMorphism' according to the rules:

--

-- (1) @'SFromDual' ':.' 'SToDual' ':.' p'@ reduces to @p'@.

--

-- (2) @'SToDual' ':.' 'SFromDual' ':.' p'@ reduces to @p'@.

rdcPathSMorphism :: PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism PathSMorphism r s o h x y
p = case PathSMorphism r s o h x y
p of
  SMorphism r s o h y1 y
SFromDual :. SMorphism r s o h y1 y1
SToDual :. Path (SMorphism r s o h) x y1
p' -> Path (SMorphism r s o h) x y1
-> Rdc (Path (SMorphism r s o h) x y1)
forall x. x -> Rdc x
reducesTo Path (SMorphism r s o h) x y1
p' Rdc (Path (SMorphism r s o h) x y1)
-> (Path (SMorphism r s o h) x y1
    -> Rdc (PathSMorphism r s o h x y))
-> Rdc (PathSMorphism r s o h x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Path (SMorphism r s o h) x y1 -> Rdc (PathSMorphism r s o h x y)
Path (SMorphism r s o h) x y1
-> Rdc (Path (SMorphism r s o h) x y1)
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism
  SMorphism r s o h y1 y
SToDual :. SMorphism r s o h y1 y1
SFromDual :. Path (SMorphism r s o h) x y1
p' -> Path (SMorphism r s o h) x y1
-> Rdc (Path (SMorphism r s o h) x y1)
forall x. x -> Rdc x
reducesTo Path (SMorphism r s o h) x y1
p' Rdc (Path (SMorphism r s o h) x y1)
-> (Path (SMorphism r s o h) x y1
    -> Rdc (PathSMorphism r s o h x y))
-> Rdc (PathSMorphism r s o h x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Path (SMorphism r s o h) x y1 -> Rdc (PathSMorphism r s o h x y)
Path (SMorphism r s o h) x y1
-> Rdc (Path (SMorphism r s o h) x y1)
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism
  SMorphism r s o h y1 y
p' :. Path (SMorphism r s o h) x y1
p''                  -> Path (SMorphism r s o h) x y1
-> Rdc (Path (SMorphism r s o h) x y1)
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism Path (SMorphism r s o h) x y1
p'' Rdc (Path (SMorphism r s o h) x y1)
-> (Path (SMorphism r s o h) x y1
    -> Rdc (PathSMorphism r s o h x y))
-> Rdc (PathSMorphism r s o h x y)
forall a b.
Action RdcState a -> (a -> Action RdcState b) -> Action RdcState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return (PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y))
-> (Path (SMorphism r s o h) x y1 -> PathSMorphism r s o h x y)
-> Path (SMorphism r s o h) x y1
-> Rdc (PathSMorphism r s o h x y)
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
. (SMorphism r s o h y1 y
p' SMorphism r s o h y1 y
-> Path (SMorphism r s o h) x y1 -> PathSMorphism r s o h x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:.)
  PathSMorphism r s o h x y
_                          -> PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
forall x. x -> Rdc x
forall (m :: * -> *) a. Monad m => a -> m a
return PathSMorphism r s o h x y
p

instance Reducible (PathSMorphism r s o h x y) where
  reduce :: PathSMorphism r s o h x y -> PathSMorphism r s o h x y
reduce = (PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y))
-> PathSMorphism r s o h x y -> PathSMorphism r s o h x y
forall x. (x -> Rdc x) -> x -> x
reduceWith PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> Rdc (PathSMorphism r s o h x y)
rdcPathSMorphism

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

-- SHom -


-- | category for structural dualities.

--

-- __Property__ Let @h@ be in @'SHom __r s o h x y__@ with

-- @'Morphism' __h__@, @'ApplicativeG' __d h c__@, @'DualisableG' __r c o d__@, then holds:

--

-- (1) @'amapG' h '.=.' 'amapG' ('sForget' h)@

-- where @'Transformable' __s t__@, @'Transformable' ('ObjectClass' __h__) __t__@

-- @'Transformable' __s r__, @'TransformableGObjectClassRange' __d s c__@ and

-- @'Transformable' __t r__, @'TransformableGObjectClassRange' __d t c__@.

--

-- __Note__ The property above states that relaxing the constraints given by @__s__@ to the

-- constraints given by @__r__@ dose not alter the applicative behavior.

newtype SHom r s o h x y = SHom (PathSMorphism r s o h x y)
  deriving (Int -> SHom r s o h x y -> String -> String
[SHom r s o h x y] -> String -> String
SHom r s o h x y -> String
(Int -> SHom r s o h x y -> String -> String)
-> (SHom r s o h x y -> String)
-> ([SHom r s o h x y] -> String -> String)
-> Show (SHom r s o h x y)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
Int -> SHom r s o h x y -> String -> String
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
[SHom r s o h x y] -> String -> String
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
SHom r s o h x y -> String
$cshowsPrec :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
Int -> SHom r s o h x y -> String -> String
showsPrec :: Int -> SHom r s o h x y -> String -> String
$cshow :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
SHom r s o h x y -> String
show :: SHom r s o h x y -> String
$cshowList :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
Show2 h =>
[SHom r s o h x y] -> String -> String
showList :: [SHom r s o h x y] -> String -> String
Show,(forall a b. SHom r s o h a b -> String) -> Show2 (SHom r s o h)
forall a b. SHom r s o h a b -> String
forall r s (o :: * -> *) (h :: * -> * -> *) a b.
Show2 h =>
SHom r s o h a b -> String
forall (h :: * -> * -> *). (forall a b. h a b -> String) -> Show2 h
$cshow2 :: forall r s (o :: * -> *) (h :: * -> * -> *) a b.
Show2 h =>
SHom r s o h a b -> String
show2 :: forall a b. SHom r s o h a b -> String
Show2,SHom r s o h x y -> Statement
(SHom r s o h x y -> Statement) -> Validable (SHom r s o h x y)
forall a. (a -> Statement) -> Validable a
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
SHom r s o h x y -> Statement
$cvalid :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
SHom r s o h x y -> Statement
valid :: SHom r s o h x y -> Statement
Validable,(forall x y. SHom r s o h x y -> Statement)
-> Validable2 (SHom r s o h)
forall x y. SHom r s o h x y -> Statement
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
SHom r s o h x y -> Statement
forall (h :: * -> * -> *).
(forall x y. h x y -> Statement) -> Validable2 h
$cvalid2 :: forall r s (o :: * -> *) (h :: * -> * -> *) x y.
(Morphism h, Validable2 h) =>
SHom r s o h x y -> Statement
valid2 :: forall x y. SHom r s o h x y -> Statement
Validable2)

deriving instance (Morphism h, Transformable s Typ, Eq2 h) => Eq (SHom r s o h x y)
deriving instance (Morphism h, Transformable s Typ, Eq2 h) => Eq2 (SHom r s o h)

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

-- SHom - Constructable -


instance Exposable (SHom r s o h x y) where
  type Form (SHom r s o h x y) = PathSMorphism r s o h x y
  form :: SHom r s o h x y -> Form (SHom r s o h x y)
form (SHom PathSMorphism r s o h x y
p) = Form (SHom r s o h x y)
PathSMorphism r s o h x y
p

instance Constructable (SHom r s o h x y) where make :: Form (SHom r s o h x y) -> SHom r s o h x y
make = PathSMorphism r s o h x y -> SHom r s o h x y
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> SHom r s o h x y
SHom (PathSMorphism r s o h x y -> SHom r s o h x y)
-> (PathSMorphism r s o h x y -> PathSMorphism r s o h x y)
-> PathSMorphism r s o h x y
-> SHom r s o h x y
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
. PathSMorphism r s o h x y -> PathSMorphism r s o h x y
forall e. Reducible e => e -> e
reduce

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

-- SHom - Disjunctive -


instance Disjunctive2 (SHom r s o h)    where variant2 :: forall x y. SHom r s o h x y -> Variant
variant2 = (Form (SHom r s o h x y) -> Variant) -> SHom r s o h x y -> Variant
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (SHom r s o h x y) -> Variant
Path (SMorphism r s o h) x y -> Variant
forall x y. Path (SMorphism r s o h) x y -> Variant
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
Disjunctive2 h =>
h x y -> Variant
variant2
instance Disjunctive (SHom r s o h x y) where variant :: SHom r s o h x y -> Variant
variant  = (Form (SHom r s o h x y) -> Variant) -> SHom r s o h x y -> Variant
forall x y. Exposable x => (Form x -> y) -> x -> y
restrict Form (SHom r s o h x y) -> Variant
PathSMorphism r s o h x y -> Variant
forall x. Disjunctive x => x -> Variant
variant

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

-- SHom - Category -


instance Morphism h => Morphism (SHom r s o h) where
  type ObjectClass (SHom r s o h) = s
  homomorphous :: forall x y.
SHom r s o h x y -> Homomorphous (ObjectClass (SHom r s o h)) x y
homomorphous (SHom PathSMorphism r s o h x y
p) = PathSMorphism r s o h x y
-> Homomorphous (ObjectClass (Path (SMorphism r s o h))) x y
forall x y.
Path (SMorphism r s o h) x y
-> Homomorphous (ObjectClass (Path (SMorphism r s o h))) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous PathSMorphism r s o h x y
p

instance Morphism h => Category (SHom r s o h) where
  cOne :: forall x. Struct (ObjectClass (SHom r s o h)) x -> SHom r s o h x x
cOne = Form (SHom r s o h x x) -> SHom r s o h x x
PathSMorphism r s o h x x -> SHom r s o h x x
forall x. Constructable x => Form x -> x
make (PathSMorphism r s o h x x -> SHom r s o h x x)
-> (Struct s x -> PathSMorphism r s o h x x)
-> Struct s x
-> SHom r s o 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 s x -> PathSMorphism r s o h x x
Struct (ObjectClass (SMorphism r s o h)) x
-> PathSMorphism r s o h x x
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath
  SHom PathSMorphism r s o h y z
f . :: forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
. SHom PathSMorphism r s o h x y
g = Form (SHom r s o h x z) -> SHom r s o h x z
forall x. Constructable x => Form x -> x
make (PathSMorphism r s o h y z
f PathSMorphism r s o h y z
-> PathSMorphism r s o h x y -> Path (SMorphism r s o h) x z
forall y z x.
Path (SMorphism r s o h) y z
-> Path (SMorphism r s o h) x y -> Path (SMorphism r s o h) x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. PathSMorphism r s o h x y
g)

instance Morphism h => CategoryDisjunctive (SHom r s o h)

instance TransformableObjectClass s (SHom r s o h)

instance TransformableG d s t => TransformableGObjectClassDomain d (SHom r s o h) t

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

-- sCov -


-- | the induced morphism.

--

-- __Note__ The resulting morphism is 'Covariant'.

sCov :: (Morphism h, Transformable (ObjectClass h) s)
  => h x y -> Variant2 Covariant (SHom r s o h) x y
sCov :: forall (h :: * -> * -> *) s x y r (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (SHom r s o h) x y
sCov h x y
h = SHom r s o h x y -> Variant2 'Covariant (SHom r s o h) x y
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Covariant h x y
Covariant2 (SHom r s o h x y -> Variant2 'Covariant (SHom r s o h) x y)
-> SHom r s o h x y -> Variant2 'Covariant (SHom r s o h) x y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Form (SHom r s o h x y) -> SHom r s o h x y
forall x. Constructable x => Form x -> x
make (h x y -> SMorphism r s o h x y
forall (h :: * -> * -> *) s x y r (o :: * -> *).
Transformable (ObjectClass h) s =>
h x y -> SMorphism r s o h x y
SCov h x y
h SMorphism r s o h x y
-> Path (SMorphism r s o h) x x -> Path (SMorphism r s o h) x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass (SMorphism r s o h)) x
-> Path (SMorphism r s o h) x x
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath (Struct (ObjectClass h) x -> Struct s x
forall x. Struct (ObjectClass h) x -> Struct s x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (h x y -> 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 y
h)))

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

-- sForget -


-- | casting a @__s__@ morphism to a @__t__@ morphism.

sForget :: (Morphism h, Transformable (ObjectClass h) t, Transformable s t)
  => SHom r s o h x y -> SHom r t o h x y
sForget :: forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
SHom r s o h x y -> SHom r t o h x y
sForget (SHom PathSMorphism r s o h x y
p) = PathSMorphism r t o h x y -> SHom r t o h x y
forall r s (o :: * -> *) (h :: * -> * -> *) x y.
PathSMorphism r s o h x y -> SHom r s o h x y
SHom (PathSMorphism r s o h x y -> PathSMorphism r t o h x y
forall (h :: * -> * -> *) t s r (o :: * -> *) x y.
(Morphism h, Transformable (ObjectClass h) t, Transformable s t) =>
PathSMorphism r s o h x y -> PathSMorphism r t o h x y
smpPathForget PathSMorphism r s o h x y
p)

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

-- sToDual -


-- | using the structural constraints to constract the 'Contravariant' morphism of 'SToDual'

-- in'SHom'.

sToDualStruct :: Struct s x -> Struct s (o x)
  -> Variant2 Contravariant (SHom r s o h) x (o x)
sToDualStruct :: forall s x (o :: * -> *) r (h :: * -> * -> *).
Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDualStruct s :: Struct s x
s@Struct s x
Struct Struct s (o x)
Struct = SHom r s o h x (o x)
-> Variant2 'Contravariant (SHom r s o h) x (o x)
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (SHom r s o h x (o x)
 -> Variant2 'Contravariant (SHom r s o h) x (o x))
-> SHom r s o h x (o x)
-> Variant2 'Contravariant (SHom r s o h) x (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Form (SHom r s o h x (o x)) -> SHom r s o h x (o x)
forall x. Constructable x => Form x -> x
make (SMorphism r s o h x (o x)
forall s x (o :: * -> *) r (h :: * -> * -> *).
(Structure s x, Structure s (o x)) =>
SMorphism r s o h x (o x)
SToDual SMorphism r s o h x (o x)
-> Path (SMorphism r s o h) x x -> Path (SMorphism r s o h) x (o x)
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass (SMorphism r s o h)) x
-> Path (SMorphism r s o h) x x
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct s x
Struct (ObjectClass (SMorphism r s o h)) x
s)

-- | 'SToDual' as a 'Contravariant' morphism in 'SHom'.

sToDual :: Transformable1 o s
  => Struct s x -> Variant2 Contravariant (SHom r s o h) x (o x)
sToDual :: forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual Struct s x
s = Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) x (o x)
forall s x (o :: * -> *) r (h :: * -> * -> *).
Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDualStruct Struct s x
s (Struct s x -> Struct s (o x)
forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s x
s)

-- | prefixing a proxy.

sToDual' :: Transformable1 o s
  => q o h -> Struct s x -> Variant2 Contravariant (SHom r s o h) x (o x)
sToDual' :: forall (o :: * -> *) s (q :: (* -> *) -> (* -> * -> *) -> *)
       (h :: * -> * -> *) x r.
Transformable1 o s =>
q o h
-> Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual' q o h
_ = Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual

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

-- sFromDual -


-- | using the structural constraints to constract the 'Contravariant' morphism of 'SFromDual'

-- in'SHom'.

sFromDualStruct :: Struct s x -> Struct s (o x)
  -> Variant2 Contravariant (SHom r s o h) (o x) x
sFromDualStruct :: forall s x (o :: * -> *) r (h :: * -> * -> *).
Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDualStruct Struct s x
Struct s' :: Struct s (o x)
s'@Struct s (o x)
Struct = SHom r s o h (o x) x
-> Variant2 'Contravariant (SHom r s o h) (o x) x
forall {k} {k1} (h :: k -> k1 -> *) (x :: k) (y :: k1).
h x y -> Variant2 'Contravariant h x y
Contravariant2 (SHom r s o h (o x) x
 -> Variant2 'Contravariant (SHom r s o h) (o x) x)
-> SHom r s o h (o x) x
-> Variant2 'Contravariant (SHom r s o h) (o x) x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Form (SHom r s o h (o x) x) -> SHom r s o h (o x) x
forall x. Constructable x => Form x -> x
make (SMorphism r s o h (o x) x
forall s x (o :: * -> *) r (h :: * -> * -> *).
(Structure s x, Structure s (o x)) =>
SMorphism r s o h (o x) x
SFromDual SMorphism r s o h (o x) x
-> Path (SMorphism r s o h) (o x) (o x)
-> Path (SMorphism r s o h) (o x) x
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Struct (ObjectClass (SMorphism r s o h)) (o x)
-> Path (SMorphism r s o h) (o x) (o x)
forall (m :: * -> * -> *) x. Struct (ObjectClass m) x -> Path m x x
IdPath Struct s (o x)
Struct (ObjectClass (SMorphism r s o h)) (o x)
s')

-- | 'SFromDual' as a 'Contravariant' morphism in 'SHom'.

sFromDual :: Transformable1 o s
  => Struct s x -> Variant2 Contravariant (SHom r s o h) (o x) x
sFromDual :: forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual Struct s x
s = Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) (o x) x
forall s x (o :: * -> *) r (h :: * -> * -> *).
Struct s x
-> Struct s (o x) -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDualStruct Struct s x
s (Struct s x -> Struct s (o x)
forall (f :: * -> *) s x.
Transformable1 f s =>
Struct s x -> Struct s (f x)
tau1 Struct s x
s)

-- | prefixing a proxy.

sFromDual' :: Transformable1 o s
  => q o h -> Struct s x -> Variant2 Contravariant (SHom r s o h) (o x) x
sFromDual' :: forall (o :: * -> *) s (q :: (* -> *) -> (* -> * -> *) -> *)
       (h :: * -> * -> *) x r.
Transformable1 o s =>
q o h
-> Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual' q o h
_ = Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual

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

-- SHom - CategoryDualisable -


instance (Morphism h, TransformableGRefl o s) => CategoryDualisable o (SHom r s o h) where
  cToDual :: forall x.
Struct (ObjectClass (SHom r s o h)) x
-> Variant2 'Contravariant (SHom r s o h) x (o x)
cToDual   = Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
Struct (ObjectClass (SHom r s o h)) x
-> Variant2 'Contravariant (SHom r s o h) x (o x)
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual
  cFromDual :: forall x.
Struct (ObjectClass (SHom r s o h)) x
-> Variant2 'Contravariant (SHom r s o h) (o x) x
cFromDual = Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
Struct (ObjectClass (SHom r s o h)) x
-> Variant2 'Contravariant (SHom r s o h) (o x) x
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual

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

-- SVal -


-- | duality for 'DualisableG' types.

newtype SVal d x = SVal (d x)

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

-- SHom - FunctorialG -


instance ( Morphism h, ApplicativeG d h c, DualisableG r c o d, Transformable s r, c ~ (->))
  => ApplicativeG (SVal d) (SMorphism r s o h) c where
  amapG :: forall x y. SMorphism r s o h x y -> c (SVal d x) (SVal d y)
amapG (SCov h x y
h) (SVal d x
d)    = d y -> SVal d y
forall (d :: * -> *) x. d x -> SVal d x
SVal (h x y -> d x -> d y
forall x y. h x y -> d x -> d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h d x
d)
  amapG t :: SMorphism r s o h x y
t@SMorphism r s o h x y
SToDual (SVal d x
d)   = d y -> SVal d y
forall (d :: * -> *) x. d x -> SVal d x
SVal (Struct r x -> d x -> d (o x)
forall x. Struct r x -> d x -> d (o x)
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d x) (d (o x))
toDualG (SMorphism r s o h x y -> Struct r x
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r x
smpBaseDomain SMorphism r s o h x y
t) d x
d)
  amapG f :: SMorphism r s o h x y
f@SMorphism r s o h x y
SFromDual (SVal d x
d) = d y -> SVal d y
forall (d :: * -> *) x. d x -> SVal d x
SVal (Struct r y -> d (o y) -> d y
forall x. Struct r x -> d (o x) -> d x
forall r (c :: * -> * -> *) (o :: * -> *) (d :: * -> *) x.
DualisableG r c o d =>
Struct r x -> c (d (o x)) (d x)
fromDualG (SMorphism r s o h x y -> Struct r y
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r y
smpBaseRange SMorphism r s o h x y
f) d x
d)

instance (Morphism h, ApplicativeG d h c, DualisableG r c o d, Transformable s r, c ~ (->))
  => ApplicativeG (SVal d) (SHom r s o h) c where
  amapG :: forall x y. SHom r s o h x y -> c (SVal d x) (SVal d y)
amapG = Path (SMorphism r s o h) x y -> SVal d x -> SVal d y
forall x y. Path (SMorphism r s o h) x y -> SVal d x -> SVal d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Path (SMorphism r s o h) x y -> SVal d x -> SVal d y)
-> (SHom r s o h x y -> Path (SMorphism r s o h) x y)
-> SHom r s o h x y
-> SVal d x
-> SVal d y
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
. SHom r s o h x y -> Form (SHom r s o h x y)
SHom r s o h x y -> Path (SMorphism r s o h) x y
forall x. Exposable x => x -> Form x
form

instance (Morphism h, ApplicativeG d h c, DualisableG r c o d, Transformable s r, c ~ (->)
         )
  => FunctorialG (SVal d) (SHom r s o h) c

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

-- smap -


-- | the induced mapping.

smap :: ApplicativeG (SVal d) (SHom r s o h) (->) => SHom r s o h x y -> d x -> d y
smap :: forall (d :: * -> *) r s (o :: * -> *) (h :: * -> * -> *) x y.
ApplicativeG (SVal d) (SHom r s o h) (->) =>
SHom r s o h x y -> d x -> d y
smap SHom r s o h x y
h d x
d = d y
d' where SVal d y
d' = SHom r s o h x y -> SVal d x -> SVal d y
forall x y. SHom r s o h x y -> SVal d x -> SVal d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG SHom r s o h x y
h (d x -> SVal d x
forall (d :: * -> *) x. d x -> SVal d x
SVal d x
d)

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

-- SDualBi -


-- | duality for 'DualisableGPair' types @__d__@.

newtype SDualBi d x = SDualBi (Either1 (Dual1 d) d x)

deriving instance (Show (d x), ShowDual1 d x) => Show (SDualBi d x)
deriving instance (Eq (d x), EqDual1 d x) => Eq (SDualBi d x)
deriving instance (Validable (d x), ValidableDual1 d x) => Validable (SDualBi d x)

type instance Dual1 (SDualBi d) = SDualBi (Dual1 d)

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

-- smpPathMapSDualBi -


smpMapSDualBi ::
  ( Morphism h
  , ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->)
  , DualisableGPair r (->) o d (Dual1 d)
  , Transformable s r
  )
  => SMorphism r s o h x y -> SDualBi d x -> SDualBi d y
smpMapSDualBi :: forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGPair r (->) o d (Dual1 d), Transformable s r) =>
SMorphism r s o h x y -> SDualBi d x -> SDualBi d y
smpMapSDualBi SMorphism r s o h x y
sh (SDualBi Either1 (Dual1 d) d x
e)
  =              case SMorphism r s o h x y
sh of
  SCov h x y
h      -> Either1 (Dual1 d) d y -> SDualBi d y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Either1 (Dual1 d) d y -> SDualBi d y)
-> Either1 (Dual1 d) d y -> SDualBi d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ case Either1 (Dual1 d) d x
e of
    Right1 d x
d  -> d y -> Either1 (Dual1 d) d y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d y -> Either1 (Dual1 d) d y) -> d y -> Either1 (Dual1 d) d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> d x -> d y
forall x y. h x y -> d x -> d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h d x
d
    Left1 Dual1 d x
d'  -> Dual1 d y -> Either1 (Dual1 d) d y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Dual1 d y -> Either1 (Dual1 d) d y)
-> Dual1 d y -> Either1 (Dual1 d) d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ h x y -> Dual1 d x -> Dual1 d y
forall x y. h x y -> Dual1 d x -> Dual1 d y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h Dual1 d x
d'
  t :: SMorphism r s o h x y
t@SMorphism r s o h x y
SToDual   -> Either1 (Dual1 d) d (o x) -> SDualBi d y
Either1 (Dual1 d) d (o x) -> SDualBi d (o x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Either1 (Dual1 d) d (o x) -> SDualBi d y)
-> Either1 (Dual1 d) d (o x) -> SDualBi d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ case Either1 (Dual1 d) d x
e of
    Right1 d x
d  -> Dual1 d (o x) -> Either1 (Dual1 d) d (o x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Dual1 d (o x) -> Either1 (Dual1 d) d (o x))
-> Dual1 d (o x) -> Either1 (Dual1 d) d (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct r x -> d x -> Dual1 d (o x)
forall x. Struct r x -> d x -> Dual1 d (o x)
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (a x) (b (o x))
toDualGLft (SMorphism r s o h x y -> Struct r x
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r x
smpBaseDomain SMorphism r s o h x y
t) d x
d
    Left1 Dual1 d x
d'  -> d (o x) -> Either1 (Dual1 d) d (o x)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d (o x) -> Either1 (Dual1 d) d (o x))
-> d (o x) -> Either1 (Dual1 d) d (o x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct r x -> Dual1 d x -> d (o x)
forall x. Struct r x -> Dual1 d x -> d (o x)
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (b x) (a (o x))
toDualGRgt (SMorphism r s o h x y -> Struct r x
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r x
smpBaseDomain SMorphism r s o h x y
t) Dual1 d x
d'
  f :: SMorphism r s o h x y
f@SMorphism r s o h x y
SFromDual -> Either1 (Dual1 d) d y -> SDualBi d y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Either1 (Dual1 d) d y -> SDualBi d y)
-> Either1 (Dual1 d) d y -> SDualBi d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ case Either1 (Dual1 d) d x
e of
    Right1 d x
d  -> Dual1 d y -> Either1 (Dual1 d) d y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Dual1 d y -> Either1 (Dual1 d) d y)
-> Dual1 d y -> Either1 (Dual1 d) d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct r y -> d (o y) -> Dual1 d y
forall x. Struct r x -> d (o x) -> Dual1 d x
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (a (o x)) (b x)
fromDualGRgt (SMorphism r s o h x y -> Struct r y
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r y
smpBaseRange SMorphism r s o h x y
f) d x
d
    Left1 Dual1 d x
d'  -> d y -> Either1 (Dual1 d) d y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d y -> Either1 (Dual1 d) d y) -> d y -> Either1 (Dual1 d) d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct r y -> Dual1 d (o y) -> d y
forall x. Struct r x -> Dual1 d (o x) -> d x
forall r (c :: * -> * -> *) (o :: * -> *) (a :: * -> *)
       (b :: * -> *) x.
DualisableGPair r c o a b =>
Struct r x -> c (b (o x)) (a x)
fromDualGLft (SMorphism r s o h x y -> Struct r y
forall (h :: * -> * -> *) s r (o :: * -> *) x y.
(Morphism h, Transformable s r) =>
SMorphism r s o h x y -> Struct r y
smpBaseRange SMorphism r s o h x y
f) Dual1 d x
Dual1 d (o y)
d'

smpPathMapSDualBi ::
  ( Morphism h
  , ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->)
  , DualisableGBi r (->) o d
  , Transformable s r
  )
  => Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y
smpPathMapSDualBi :: forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGBi r (->) o d, Transformable s r) =>
Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y
smpPathMapSDualBi Path (SMorphism r s o h) x y
h
  =           case Path (SMorphism r s o h) x y
h of
  IdPath Struct (ObjectClass (SMorphism r s o h)) x
_ -> SDualBi d x -> SDualBi d x
SDualBi d x -> SDualBi d y
forall x. x -> x
id
  SMorphism r s o h y1 y
m :. Path (SMorphism r s o h) x y1
h'  -> SMorphism r s o h y1 y -> SDualBi d y1 -> SDualBi d y
forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGPair r (->) o d (Dual1 d), Transformable s r) =>
SMorphism r s o h x y -> SDualBi d x -> SDualBi d y
smpMapSDualBi SMorphism r s o h y1 y
m (SDualBi d y1 -> SDualBi d y)
-> (SDualBi d x -> SDualBi d y1) -> SDualBi d x -> SDualBi d y
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
. Path (SMorphism r s o h) x y1 -> SDualBi d x -> SDualBi d y1
forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGBi r (->) o d, Transformable s r) =>
Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y
smpPathMapSDualBi Path (SMorphism r s o h) x y1
h'

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

-- smapBi -


-- | application of 'SHom' on 'SDualBi'

--

-- __Properties__ Let @'Morphism' __h__@, @'ApplicativeG' __d h__ (->)@,

-- @'ApplicativeG' ('Dual1' __d__) __h__ (->)@, @'DualisableGBi' __r__ (->) __o d__@

-- and @'Transformable' __s r__@, then holds:

--

-- (1) 'smapBi' is functorial.

--

-- (2) For all @__x__@, @__y__@ and @h@ in @__h x y__@ holds:

--

--     (1) If @'variant2' h '==' 'Covariant'@, then for all @d@ in @__d x__@ holds:

--     @'smapBi' h ('SDualBi' ('Right1' d)) '==' 'SDualBi' ('Right1' d')@ where @d' = 'amapG' h d@.

--

--     (2) If @'variant2' h '==' 'Covariant'@, then for all @d'@ in @'Dual1' __d x__@ holds:

--     @'smapBi' h ('SDualBi' ('Left1' d')) '==' 'SDualBi' ('Left1' d)@ where @d = 'amapG' h d'@.

--

--     (3) If @'variant2' h '==' 'Contravariant'@, then for all @d@ in @__d x__@ holds:

--     @'smapBi' h ('SDualBi' ('Right1' d)) '==' 'SDualBi' ('Left1' d')@.

--

--     (4) If @'variant2' h '==' 'Covariant'@, then for all @d'@ in @'Dual1' __d x__@ holds:

--     @'smapBi' h ('SDualBi' ('Left1' d')) '==' 'SDualBi' ('Right1' d)@.

smapBi ::
  ( Morphism h
  , ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->)
  , DualisableGBi r (->) o d
  , Transformable s r
  )
  => SHom r s o h x y -> SDualBi d x -> SDualBi d y
smapBi :: forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGBi r (->) o d, Transformable s r) =>
SHom r s o h x y -> SDualBi d x -> SDualBi d y
smapBi = Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y
forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGBi r (->) o d, Transformable s r) =>
Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y
smpPathMapSDualBi (Path (SMorphism r s o h) x y -> SDualBi d x -> SDualBi d y)
-> (SHom r s o h x y -> Path (SMorphism r s o h) x y)
-> SHom r s o h x y
-> SDualBi d x
-> SDualBi d y
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
. SHom r s o h x y -> Form (SHom r s o h x y)
SHom r s o h x y -> Path (SMorphism r s o h) x y
forall x. Exposable x => x -> Form x
form

instance
  ( Morphism h
  , ApplicativeGBi d h (->)
  , DualisableGBi r (->) o d
  , Transformable s r
  )
  => ApplicativeG (SDualBi d) (SHom r s o h) (->) where
  amapG :: forall x y. SHom r s o h x y -> SDualBi d x -> SDualBi d y
amapG = SHom r s o h x y -> SDualBi d x -> SDualBi d y
forall (h :: * -> * -> *) (d :: * -> *) r (o :: * -> *) s x y.
(Morphism h, ApplicativeG d h (->), ApplicativeG (Dual1 d) h (->),
 DualisableGBi r (->) o d, Transformable s r) =>
SHom r s o h x y -> SDualBi d x -> SDualBi d y
smapBi

instance
  ( Morphism h
  , ApplicativeGBi d h (->)
  , DualisableGBi r (->) o d
  , Transformable s r
  )
  => FunctorialG (SDualBi d) (SHom r s o h) (->)

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

-- vmapBi -


-- | mapping of 'SDualBi' given by 'Variant2' mappings.

vmapBi :: Disjunctive2 h
  => (Variant2 Covariant h x y -> d x -> d y)
  -> (Variant2 Covariant h x y -> Dual1 d x -> Dual1 d y)
  -> (Variant2 Contravariant h x y -> d x -> Dual1 d y)
  -> (Variant2 Contravariant h x y -> Dual1 d x -> d y)
  -> h x y -> SDualBi d x -> SDualBi d y
vmapBi :: forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant h x y -> d x -> d y
dd Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y
d'd' Variant2 'Contravariant h x y -> d x -> Dual1 d y
dd' Variant2 'Contravariant h x y -> Dual1 d x -> d y
d'd h x y
h (SDualBi Either1 (Dual1 d) d x
s)
  = Either1 (Dual1 d) d y -> SDualBi d y
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi    (Either1 (Dual1 d) d y -> SDualBi d y)
-> Either1 (Dual1 d) d y -> SDualBi d y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ case h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
forall (h :: * -> * -> *) x y.
Disjunctive2 h =>
h x y
-> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
toVariant2 h x y
h of
  Right2 Variant2 'Covariant h x y
hCov -> case Either1 (Dual1 d) d x
s of
    Right1 d x
d  -> d y -> Either1 (Dual1 d) d y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Variant2 'Covariant h x y -> d x -> d y
dd Variant2 'Covariant h x y
hCov d x
d)
    Left1 Dual1 d x
d'  -> Dual1 d y -> Either1 (Dual1 d) d y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y
d'd' Variant2 'Covariant h x y
hCov Dual1 d x
d')
  Left2 Variant2 'Contravariant h x y
hCnt  -> case Either1 (Dual1 d) d x
s of
    Right1 d x
d  -> Dual1 d y -> Either1 (Dual1 d) d y
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Variant2 'Contravariant h x y -> d x -> Dual1 d y
dd' Variant2 'Contravariant h x y
hCnt d x
d)
    Left1 Dual1 d x
d'  -> d y -> Either1 (Dual1 d) d y
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Variant2 'Contravariant h x y -> Dual1 d x -> d y
d'd Variant2 'Contravariant h x y
hCnt Dual1 d x
d')

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

-- xSDualBi -


-- | random variable for 'SDualBi'.

xSDualBi :: X (d x) -> X (Dual1 d x) -> X (SDualBi d x)
xSDualBi :: forall (d :: * -> *) x. X (d x) -> X (Dual1 d x) -> X (SDualBi d x)
xSDualBi X (d x)
xd X (Dual1 d x)
xd'
  = (Either1 (Dual1 d) d x -> SDualBi d x)
-> X (Either1 (Dual1 d) d x) -> X (SDualBi d x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Either1 (Dual1 d) d x -> SDualBi d x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi
  (X (Either1 (Dual1 d) d x) -> X (SDualBi d x))
-> X (Either1 (Dual1 d) d x) -> X (SDualBi d x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ [X (Either1 (Dual1 d) d x)] -> X (Either1 (Dual1 d) d x)
forall a. [X a] -> X a
xOneOfX [ (d x -> Either1 (Dual1 d) d x)
-> X (d x) -> X (Either1 (Dual1 d) d x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 d x -> Either1 (Dual1 d) d x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 X (d x)
xd
            , (Dual1 d x -> Either1 (Dual1 d) d x)
-> X (Dual1 d x) -> X (Either1 (Dual1 d) d x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Dual1 d x -> Either1 (Dual1 d) d x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 X (Dual1 d x)
xd'
            ]

instance (XStandard (d x), XStandardDual1 d x)
  => XStandard (SDualBi d x) where
  xStandard :: X (SDualBi d x)
xStandard = X (d x) -> X (Dual1 d x) -> X (SDualBi d x)
forall (d :: * -> *) x. X (d x) -> X (Dual1 d x) -> X (SDualBi d x)
xSDualBi X (d x)
forall x. XStandard x => X x
xStandard X (Dual1 d x)
forall x. XStandard x => X x
xStandard

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

-- xSomeMrphSHom -


-- | random variable for some morphism for @'SHom' __s o h__@.

--

-- [Pre] Not both input random variables are empty.

--

-- [Post] The resulting random variable is not empty

xSomeMrphSHom :: (Morphism h, Transformable (ObjectClass h) s)
  => X (SomeObjectClass (SHom r s o h)) -> X (SomeMorphism h)
  -> X (SomeMorphism (SHom r s o h))
xSomeMrphSHom :: forall (h :: * -> * -> *) s r (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h) -> X (SomeMorphism (SHom r s o h))
xSomeMrphSHom X (SomeObjectClass (SHom r s o h))
xso X (SomeMorphism h)
xsh
  =   (SomeObjectClass (SHom r s o h) -> SomeMorphism (SHom r s o h))
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeObjectClass (SHom r s o h) -> SomeMorphism (SHom r s o h)
forall (c :: * -> * -> *).
Category c =>
SomeObjectClass c -> SomeMorphism c
someOne X (SomeObjectClass (SHom r s o h))
xso
  X (SomeMorphism (SHom r s o h))
-> X (SomeMorphism (SHom r s o h))
-> X (SomeMorphism (SHom r s o h))
forall a. X a -> X a -> X a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (SomeMorphism h -> SomeMorphism (SHom r s o h))
-> X (SomeMorphism h) -> X (SomeMorphism (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeMorphism h x y
h) -> let Covariant2 SHom r s o h x y
h' = h x y -> Variant2 'Covariant (SHom r s o h) x y
forall (h :: * -> * -> *) s x y r (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
h x y -> Variant2 'Covariant (SHom r s o h) x y
sCov h x y
h in SHom r s o h x y -> SomeMorphism (SHom r s o h)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism SHom r s o h x y
h') X (SomeMorphism h)
xsh

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

-- xSctAdjOne -


xSctAdjOne :: Morphism h
  => SomeMorphism (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjOne :: forall (h :: * -> * -> *) r s (o :: * -> *).
Morphism h =>
SomeMorphism (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjOne (SomeMorphism SHom r s o h x y
f)
  = [SomeCmpb2 (SHom r s o h)] -> X (SomeCmpb2 (SHom r s o h))
forall a. [a] -> X a
xOneOf [SHom r s o h x y -> SHom r s o h x x -> SomeCmpb2 (SHom r s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 SHom r s o h x y
f (Struct (ObjectClass (SHom r s o h)) x -> SHom r s o h x x
forall x. Struct (ObjectClass (SHom r s o h)) x -> SHom r s o h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) x
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain SHom r s o h x y
f)), SHom r s o h y y -> SHom r s o h x y -> SomeCmpb2 (SHom r s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (Struct (ObjectClass (SHom r s o h)) y -> SHom r s o h y y
forall x. Struct (ObjectClass (SHom r s o h)) x -> SHom r s o h x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range SHom r s o h x y
f)) SHom r s o h x y
f]

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

-- xSctAdjDual -


-- | adjoining @n@-times 'SToDual' to the left or 'SFromDual' to the right or

-- @'SFromDual' '.' 'SToDual'@

-- in the middle.

xSctAdjDual :: (Morphism h, Transformable1 o s)
  => N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual :: forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual N
0 SomeCmpb2 (SHom r s o h)
fg = SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return SomeCmpb2 (SHom r s o h)
fg
xSctAdjDual N
n SomeCmpb2 (SHom r s o h)
fg = [X (SomeCmpb2 (SHom r s o h))] -> X (SomeCmpb2 (SHom r s o h))
forall a. [X a] -> X a
xOneOfX [ (SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjToDual (X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual (N -> N
forall a. Enum a => a -> a
pred N
n) SomeCmpb2 (SHom r s o h)
fg
                           , (SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjFromDual (X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual (N -> N
forall a. Enum a => a -> a
pred N
n) SomeCmpb2 (SHom r s o h)
fg
                           , (SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjFromToDual (X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual (N -> N
forall a. Enum a => a -> a
pred N
n) SomeCmpb2 (SHom r s o h)
fg
                           ]
  where
  
    adjToDual :: (Morphism h, Transformable1 o s)
      => SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
    adjToDual :: forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjToDual (SomeCmpb2 SHom r s o h y z
f SHom r s o h x y
g) = SHom r s o h y (o z)
-> SHom r s o h x y -> SomeCmpb2 (SHom r s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (SHom r s o h z (o z)
d SHom r s o h z (o z) -> SHom r s o h y z -> SHom r s o h y (o z)
forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom r s o h y z
f) SHom r s o h x y
g where
      Contravariant2 SHom r s o h z (o z)
d = Struct s z -> Variant2 'Contravariant (SHom r s o h) z (o z)
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual (SHom r s o h y z -> Struct (ObjectClass (SHom r s o h)) z
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range SHom r s o h y z
f)

    adjFromDual :: (Morphism h, Transformable1 o s)
      => SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
    adjFromDual :: forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjFromDual (SomeCmpb2 SHom r s o h y z
f SHom r s o h x y
g) = SHom r s o h y z
-> SHom r s o h (o x) y -> SomeCmpb2 (SHom r s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 SHom r s o h y z
f (SHom r s o h x y
g SHom r s o h x y -> SHom r s o h (o x) x -> SHom r s o h (o x) y
forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom r s o h (o x) x
d) where
      Contravariant2 SHom r s o h (o x) x
d = Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual (SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) x
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain SHom r s o h x y
g)

    adjFromToDual :: (Morphism h, Transformable1 o s)
      => SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
    adjFromToDual :: forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
SomeCmpb2 (SHom r s o h) -> SomeCmpb2 (SHom r s o h)
adjFromToDual (SomeCmpb2 SHom r s o h y z
f SHom r s o h x y
g) = SHom r s o h (o y) z
-> SHom r s o h x (o y) -> SomeCmpb2 (SHom r s o h)
forall (c :: * -> * -> *) y z x. c y z -> c x y -> SomeCmpb2 c
SomeCmpb2 (SHom r s o h y z
f SHom r s o h y z -> SHom r s o h (o y) y -> SHom r s o h (o y) z
forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom r s o h (o y) y
df) (SHom r s o h y (o y)
dg SHom r s o h y (o y) -> SHom r s o h x y -> SHom r s o h x (o y)
forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom r s o h x y
g) where
      Contravariant2 SHom r s o h y (o y)
dg = Struct s y -> Variant2 'Contravariant (SHom r s o h) y (o y)
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) x (o x)
sToDual (SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range SHom r s o h x y
g)
      Contravariant2 SHom r s o h (o y) y
df = Struct s y -> Variant2 'Contravariant (SHom r s o h) (o y) y
forall (o :: * -> *) s x r (h :: * -> * -> *).
Transformable1 o s =>
Struct s x -> Variant2 'Contravariant (SHom r s o h) (o x) x
sFromDual (SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall x y.
SHom r s o h x y -> Struct (ObjectClass (SHom r s o h)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range SHom r s o h x y
g)

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

-- xSctSomeCmpb2 -


-- | random variable for some composable morphism in @'SHom' __s o h__@ where 'cOne' and @h@ are

-- adjoined with maximal @n@ times 'SToDual' or 'SFromDual' or @'SFromDual' '.' 'SToDual'@

--

-- [Pre] Not both input random variables are empty.

--

-- [Post] The resulting random variable is not empty

xSctSomeCmpb2 :: (Morphism h, Transformable (ObjectClass h) s, Transformable1 o s)
  => N -> X (SomeObjectClass (SHom r s o h)) -> X (SomeMorphism h)
  -> X (SomeCmpb2 (SHom r s o h))
xSctSomeCmpb2 :: forall (h :: * -> * -> *) s (o :: * -> *) r.
(Morphism h, Transformable (ObjectClass h) s,
 Transformable1 o s) =>
N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom r s o h))
xSctSomeCmpb2 N
n X (SomeObjectClass (SHom r s o h))
xo X (SomeMorphism h)
xf = N -> N -> X N
xNB N
0 N
n X N
-> (N -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h))
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \N
n' -> X (SomeCmpb2 (SHom r s o h))
xfg X (SomeCmpb2 (SHom r s o h))
-> (SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h))
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) (o :: * -> *) s r.
(Morphism h, Transformable1 o s) =>
N -> SomeCmpb2 (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjDual N
n' where
  xfg :: X (SomeCmpb2 (SHom r s o h))
xfg = X (X (SomeCmpb2 (SHom r s o h))) -> X (SomeCmpb2 (SHom r s o h))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeCmpb2 (SHom r s o h))) -> X (SomeCmpb2 (SHom r s o h)))
-> X (X (SomeCmpb2 (SHom r s o h))) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SomeMorphism (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h)))
-> X (SomeMorphism (SHom r s o h))
-> X (X (SomeCmpb2 (SHom r s o h)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeMorphism (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) r s (o :: * -> *).
Morphism h =>
SomeMorphism (SHom r s o h) -> X (SomeCmpb2 (SHom r s o h))
xSctAdjOne (X (SomeMorphism (SHom r s o h))
 -> X (X (SomeCmpb2 (SHom r s o h))))
-> X (SomeMorphism (SHom r s o h))
-> X (X (SomeCmpb2 (SHom r s o h)))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h) -> X (SomeMorphism (SHom r s o h))
forall (h :: * -> * -> *) s r (o :: * -> *).
(Morphism h, Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h) -> X (SomeMorphism (SHom r s o h))
xSomeMrphSHom X (SomeObjectClass (SHom r s o h))
xo X (SomeMorphism h)
xf

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

-- xSctSomeMrph -


-- | random variable for some 'SHom's between the given object classes.

xSctSomeMrph :: (Morphism h, Transformable (ObjectClass h) s, Transformable1 o s)
  => N -> X (SomeObjectClass (SHom r s o h)) -> X (SomeMorphism (SHom r s o h))
xSctSomeMrph :: forall (h :: * -> * -> *) s (o :: * -> *) r.
(Morphism h, Transformable (ObjectClass h) s,
 Transformable1 o s) =>
N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism (SHom r s o h))
xSctSomeMrph N
n X (SomeObjectClass (SHom r s o h))
xo = (SomeCmpb2 (SHom r s o h) -> SomeMorphism (SHom r s o h))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeMorphism (SHom r s o h))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(SomeCmpb2 SHom r s o h y z
f SHom r s o h x y
g) -> SHom r s o h x z -> SomeMorphism (SHom r s o h)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (SHom r s o h y z
f SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall y z x.
SHom r s o h y z -> SHom r s o h x y -> SHom r s o h x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. SHom r s o h x y
g)) (X (SomeCmpb2 (SHom r s o h)) -> X (SomeMorphism (SHom r s o h)))
-> X (SomeCmpb2 (SHom r s o h)) -> X (SomeMorphism (SHom r s o h))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom r s o h))
forall (h :: * -> * -> *) s (o :: * -> *) r.
(Morphism h, Transformable (ObjectClass h) s,
 Transformable1 o s) =>
N
-> X (SomeObjectClass (SHom r s o h))
-> X (SomeMorphism h)
-> X (SomeCmpb2 (SHom r s o h))
xSctSomeCmpb2 N
n X (SomeObjectClass (SHom r s o h))
xo X (SomeMorphism h)
forall x. X x
XEmpty