{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Structure.Distributive.Proposition
-- Description : propositions on distributive structures
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- propositions about 'Distributive' structure.
module OAlg.Structure.Distributive.Proposition
  (

    -- * Distributive
    prpDst, XDst(..)
  , prpDst1, prpDst2, prpDst3, prpDst4
  , DstRootSide(..), DstSide(..)


    -- * X
  , XStandardDst(..)
  , xDstStalkStartEnd
  
    -- ** Total
  , xDstTtl
    -- ** Orientation
  , xDstOrnt

    -- ** Oriented Direction
  , xoDst
    -- * Tools
  , dstDst

  )
  where

import Control.Monad

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Distributive.Definition

--------------------------------------------------------------------------------
-- DstRootSide -

-- | predicate for a root and a factor at the root.
--
-- __Properties__ Let @p@ be in @'DstRootSide' __s__ __d__@ for a 'Distributive' structure @__d__@,
-- then holds:
--
-- (1) If @p@ matches @'LDstRoot' r f@ then holds: @'start' r '==' 'end' f@.
--
-- (2) If @p@ matches @'RDstRoot' f r@ then holds: @'start' f '==' 'end' r@.
data DstRootSide (s :: Side) d where
  LDstRoot :: Root d -> d -> DstRootSide LeftSide d
  RDstRoot :: d -> Root d -> DstRootSide RightSide d

deriving instance Distributive d => Show (DstRootSide s d)

--------------------------------------------------------------------------------
-- DstRootSide - Dualisable -

type instance Dual (DstRootSide s d) = DstRootSide (Dual s) (Op d)

instance Distributive d => Dualisable (DstRootSide RightSide d) where
  toDual :: DstRootSide 'RightSide d -> Dual (DstRootSide 'RightSide d)
toDual (RDstRoot d
f Root d
r)         = forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot (forall x. Transposable x => x -> x
transpose Root d
r) (forall x. x -> Op x
Op d
f)
  fromDual :: Dual (DstRootSide 'RightSide d) -> DstRootSide 'RightSide d
fromDual (LDstRoot Root (Op d)
r' (Op d
f)) = forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot d
f (forall x. Transposable x => x -> x
transpose Root (Op d)
r')
  
--------------------------------------------------------------------------------
-- DstRootSide - Validable -

instance Distributive d => Validable (DstRootSide s d) where
  valid :: DstRootSide s d -> Statement
valid (LDstRoot Root d
r d
f)    = forall a. Validable a => a -> Statement
valid (Root d
r,d
f) forall b. Boolean b => b -> b -> b
&& (forall q. Oriented q => q -> Point q
start Root d
r forall a. Eq a => a -> a -> Statement
.==. forall q. Oriented q => q -> Point q
end d
f )
  valid rd :: DstRootSide s d
rd@(RDstRoot d
_ Root d
_) = forall a. Validable a => a -> Statement
valid (forall x. Dualisable x => x -> Dual x
toDual DstRootSide s d
rd)


--------------------------------------------------------------------------------
-- prpDst1 -

-- | validity according to "OAlg.Structure.Distributive#Dst1".
prpDst1 :: Distributive d => X (DstRootSide LeftSide d) -> Statement
prpDst1 :: forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 X (DstRootSide 'LeftSide d)
xrg = String -> Label
Prp String
"Dst1"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (DstRootSide 'LeftSide d)
xrg (\rg :: DstRootSide 'LeftSide d
rg@(LDstRoot Root d
r d
g)
                    -> (forall a. Additive a => Root a -> a
zero Root d
r forall c. Multiplicative c => c -> c -> c
* d
g forall a. Eq a => a -> a -> Bool
== forall a. Additive a => Root a -> a
zero (forall q. Oriented q => q -> Point q
start d
g forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end Root d
r))
                       Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"rg"String -> String -> Parameter
:=forall a. Show a => a -> String
show DstRootSide 'LeftSide d
rg]
                   )

--------------------------------------------------------------------------------
-- prpDst3 -

-- | validity according to "OAlg.Structure.Distributive#Dst3".
prpDst3 :: Distributive d => X (DstRootSide RightSide d) -> Statement
prpDst3 :: forall d.
Distributive d =>
X (DstRootSide 'RightSide d) -> Statement
prpDst3 X (DstRootSide 'RightSide d)
xfr = String -> Label
Prp String
"Dst3" Label -> Statement -> Statement
:<=>: forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => x -> Dual x
toDual X (DstRootSide 'RightSide d)
xfr)

--------------------------------------------------------------------------------
-- DstSide -

-- | predicate for two addable summands together with a matching factor.
--
-- __Properties__ Let @p@ be in @'DstSide' __s__ __d__@ for a 'Distributive' structure, then holds:
--
-- (1) If @p@ matches @'LDst' (a,b) g@ then holds:
--
--     (1) @'root' a '==' 'root' b@.
--
--     (2) @'start' a '==' 'end' g@.
--
-- (2) If @p@ matches @'RDst' f (a,b)@ then holds:
--
--     (1) @'root' a '==' 'root' b@.
--
--     (2) @'start' f '==' 'end' a@.
data DstSide (s :: Side) d where
  LDst :: (d,d) -> d -> DstSide LeftSide d
  RDst :: d -> (d,d) -> DstSide RightSide d

deriving instance Distributive d => Show (DstSide s d)

--------------------------------------------------------------------------------
-- DstSide - Dualisable -

type instance Dual (DstSide s d) = DstSide (Dual s) (Op d)

instance Distributive d => Dualisable (DstSide RightSide d) where
  toDual :: DstSide 'RightSide d -> Dual (DstSide 'RightSide d)
toDual (RDst d
f (d
a,d
b)) = forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (forall x. x -> Op x
Op d
a,forall x. x -> Op x
Op d
b) (forall x. x -> Op x
Op d
f)
  fromDual :: Dual (DstSide 'RightSide d) -> DstSide 'RightSide d
fromDual (LDst (Op d
a,Op d
b) (Op d
f)) = forall d. d -> (d, d) -> DstSide 'RightSide d
RDst d
f (d
a,d
b)

--------------------------------------------------------------------------------
-- DstSide - Validable -

instance Distributive d => Validable (DstSide s d) where
  valid :: DstSide s d -> Statement
valid (LDst (d
a,d
b) d
g) = forall a. Validable a => a -> Statement
valid (forall a. a -> a -> Adbl2 a
Adbl2 d
a d
b) forall b. Boolean b => b -> b -> b
&& forall a. Validable a => a -> Statement
valid (forall c. c -> c -> Mltp2 c
Mltp2 d
a d
g)
  valid rd :: DstSide s d
rd@(RDst d
_ (d, d)
_)  = forall a. Validable a => a -> Statement
valid (forall x. Dualisable x => x -> Dual x
toDual DstSide s d
rd)
  
--------------------------------------------------------------------------------
-- prpDst2 -

-- | validity according to "OAlg.Structure.Distributive#Dst2".
prpDst2 :: Distributive d => X (DstSide LeftSide d) -> Statement
prpDst2 :: forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 X (DstSide 'LeftSide d)
xabg = String -> Label
Prp String
"Dst2"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (DstSide 'LeftSide d)
xabg
          (\abg :: DstSide 'LeftSide d
abg@(LDst (d
a,d
b) d
g)
           -> ((d
a forall a. Additive a => a -> a -> a
+ d
b) forall c. Multiplicative c => c -> c -> c
* d
g forall a. Eq a => a -> a -> Bool
== d
aforall c. Multiplicative c => c -> c -> c
*d
g forall a. Additive a => a -> a -> a
+ d
bforall c. Multiplicative c => c -> c -> c
*d
g) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"abg"String -> String -> Parameter
:=forall a. Show a => a -> String
show DstSide 'LeftSide d
abg]
          )
          
--------------------------------------------------------------------------------
-- prpDst4 -

-- | validity according to "OAlg.Structure.Distributive#Dst4".
prpDst4 :: Distributive d => X (DstSide RightSide d) -> Statement
prpDst4 :: forall d. Distributive d => X (DstSide 'RightSide d) -> Statement
prpDst4 X (DstSide 'RightSide d)
xfab = String -> Label
Prp String
"Dst4" Label -> Statement -> Statement
:<=>: forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => x -> Dual x
toDual X (DstSide 'RightSide d)
xfab) 
                               

--------------------------------------------------------------------------------
-- XDst -

-- | random variable for validating 'Distributive' structures.
data XDst d = XDst (X (DstRootSide LeftSide d))  (X (DstSide LeftSide d))
                   (X (DstRootSide RightSide d)) (X (DstSide RightSide d))

--------------------------------------------------------------------------------
-- XStandardDst -

-- | standard random variable for 'Distributive' structures.
class XStandardDst d where
  xStandardDst :: XDst d
  
--------------------------------------------------------------------------------
-- prpDst -

-- | validity for the 'Distributive' structure of the type @a@.
prpDst :: Distributive d => XDst d -> Statement
prpDst :: forall d. Distributive d => XDst d -> Statement
prpDst (XDst X (DstRootSide 'LeftSide d)
xrg X (DstSide 'LeftSide d)
xabg X (DstRootSide 'RightSide d)
xfr X (DstSide 'RightSide d)
xfab) = String -> Label
Prp String
"Dst"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall d.
Distributive d =>
X (DstRootSide 'LeftSide d) -> Statement
prpDst1 X (DstRootSide 'LeftSide d)
xrg
            , forall d. Distributive d => X (DstSide 'LeftSide d) -> Statement
prpDst2 X (DstSide 'LeftSide d)
xabg
            , forall d.
Distributive d =>
X (DstRootSide 'RightSide d) -> Statement
prpDst3 X (DstRootSide 'RightSide d)
xfr
            , forall d. Distributive d => X (DstSide 'RightSide d) -> Statement
prpDst4 X (DstSide 'RightSide d)
xfab
            ]

--------------------------------------------------------------------------------
-- xDstTtl -

-- | random variable to validate 'Total' 'Distributive' structures.
xDstTtl :: Singleton (Root m) => X m -> XDst m
xDstTtl :: forall m. Singleton (Root m) => X m -> XDst m
xDstTtl X m
xm = forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide m)
xrg X (DstSide 'LeftSide m)
xabg X (DstRootSide 'RightSide m)
xfr X (DstSide 'RightSide m)
xfab where
  xrg :: X (DstRootSide 'LeftSide m)
xrg = do
    m
g <- X m
xm
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot forall s. Singleton s => s
unit m
g
  xabg :: X (DstSide 'LeftSide m)
xabg = do
    m
a <- X m
xm
    m
b <- X m
xm
    m
g <- X m
xm
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (m
a,m
b) m
g
  xfr :: X (DstRootSide 'RightSide m)
xfr  = do
    m
f <- X m
xm
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot m
f forall s. Singleton s => s
unit
  xfab :: X (DstSide 'RightSide m)
xfab = do
    m
f <- X m
xm
    m
a <- X m
xm
    m
b <- X m
xm
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. d -> (d, d) -> DstSide 'RightSide d
RDst m
f (m
a,m
b)

instance XStandardDst N where
  xStandardDst :: XDst N
xStandardDst = forall m. Singleton (Root m) => X m -> XDst m
xDstTtl forall x. XStandard x => X x
xStandard
  
instance XStandardDst Z where
  xStandardDst :: XDst Z
xStandardDst = forall m. Singleton (Root m) => X m -> XDst m
xDstTtl forall x. XStandard x => X x
xStandard
  
instance XStandardDst Q where
  xStandardDst :: XDst Q
xStandardDst = forall m. Singleton (Root m) => X m -> XDst m
xDstTtl forall x. XStandard x => X x
xStandard
  
--------------------------------------------------------------------------------
-- xDstStalkStartEnd -

-- | the induced random variable for 'Distributive' structures.
xDstStalkStartEnd :: Distributive m
     => XStalk m
     -> XOrtSite From m
     -> XOrtSite To m
     -> XDst m
xDstStalkStartEnd :: forall m.
Distributive m =>
XStalk m -> XOrtSite 'From m -> XOrtSite 'To m -> XDst m
xDstStalkStartEnd XStalk m
xa XOrtSite 'From m
xs XOrtSite 'To m
xe = forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide m)
xrg X (DstSide 'LeftSide m)
xabg X (DstRootSide 'RightSide m)
xfr X (DstSide 'RightSide m)
xfab where
  xrg :: X (DstRootSide 'LeftSide m)
xrg = do
    Orientation (Point m)
r          <- forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
g] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'To m
xe N
1 (forall q. Oriented q => q -> Point q
start Orientation (Point m)
r)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Orientation (Point m)
r m
g
  xabg :: X (DstSide 'LeftSide m)
xabg = do
    Orientation (Point m)
r          <- forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Adbl2 m
a m
b  <- forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk m
xa Orientation (Point m)
r
    Path Point m
_ [m
g] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'To m
xe N
1 (forall q. Oriented q => q -> Point q
start Orientation (Point m)
r)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (m
a,m
b) m
g
  xfr :: X (DstRootSide 'RightSide m)
xfr = do
    Orientation (Point m)
r          <- forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
f] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'From m
xs N
1 (forall q. Oriented q => q -> Point q
end Orientation (Point m)
r)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. d -> Root d -> DstRootSide 'RightSide d
RDstRoot m
f Orientation (Point m)
r
    
  xfab :: X (DstSide 'RightSide m)
xfab = do
    Orientation (Point m)
r          <- forall x. XStalk x -> X (Root x)
xRoot XStalk m
xa
    Path Point m
_ [m
f] <- forall c (s :: Site).
Multiplicative c =>
XOrtSite s c -> N -> Point c -> X (Path c)
xosPathAt XOrtSite 'From m
xs N
1 (forall q. Oriented q => q -> Point q
end Orientation (Point m)
r)
    Adbl2 m
a m
b  <- forall a. Additive a => XStalk a -> Root a -> X (Adbl2 a)
xStalkAdbl2 XStalk m
xa Orientation (Point m)
r
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d. d -> (d, d) -> DstSide 'RightSide d
RDst m
f (m
a,m
b)

--------------------------------------------------------------------------------
-- xDstOrnt -

-- | random variable for the 'Distributive' structure of @'Orientation' __p__@.
xDstOrnt :: Entity p => X p -> XDst (Orientation p)
xDstOrnt :: forall p. Entity p => X p -> XDst (Orientation p)
xDstOrnt X p
xp = forall m.
Distributive m =>
XStalk m -> XOrtSite 'From m -> XOrtSite 'To m -> XDst m
xDstStalkStartEnd XStalk (Orientation p)
xa XOrtSite 'From (Orientation p)
xs XOrtSite 'To (Orientation p)
xe where
  xa :: XStalk (Orientation p)
xa = forall p. X p -> XStalk (Orientation p)
xStalkOrnt X p
xp
  xs :: XOrtSite 'From (Orientation p)
xs = forall p. X p -> XOrtSite 'From (Orientation p)
xStartOrnt X p
xp
  xe :: XOrtSite 'To (Orientation p)
xe = forall p. X p -> XOrtSite 'To (Orientation p)
xEndOrnt X p
xp
  
instance (Entity p, XStandard p) => XStandardDst (Orientation p) where
  xStandardDst :: XDst (Orientation p)
xStandardDst = forall p. Entity p => X p -> XDst (Orientation p)
xDstOrnt forall x. XStandard x => X x
xStandard
  
--------------------------------------------------------------------------------
-- dstDst -

-- | distribution of @'XDst' __d__@.
dstDst :: Distributive d => Int -> XDst d -> IO ()
dstDst :: forall d. Distributive d => Int -> XDst d -> IO ()
dstDst Int
n (XDst X (DstRootSide 'LeftSide d)
xrg X (DstSide 'LeftSide d)
xabg X (DstRootSide 'RightSide d)
xfr X (DstSide 'RightSide d)
xfab) = do
  Omega
o <- IO Omega
getOmega
  String -> IO ()
putStrLn String
"xrg"
  forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> String
show X (DstRootSide 'LeftSide d)
xrg) Omega
o
  String -> IO ()
putStrLn String
"xabg"
  forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> String
show X (DstSide 'LeftSide d)
xabg) Omega
o
  String -> IO ()
putStrLn String
"xfr"
  forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> String
show X (DstRootSide 'RightSide d)
xfr) Omega
o
  String -> IO ()
putStrLn String
"xfab"
  forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Show a => a -> String
show X (DstSide 'RightSide d)
xfab) Omega
o

--------------------------------------------------------------------------------
-- xoDstRootSideL -

-- | the induced random variable for @'DstRootSide' 'LeftSide' __d__'@.
xoDstRootSideL :: Distributive d
  => XOrtOrientation d -> XOrtSite To d -> X (DstRootSide LeftSide d)
xoDstRootSideL :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL XOrtOrientation d
xo XOrtSite 'To d
xt = do
  Orientation (Point d)
r <- forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot XOrtOrientation d
xo
  d
f <- forall q. XOrtSite 'To q -> Point q -> X q
xosEnd XOrtSite 'To d
xt (forall q. Oriented q => q -> Point q
start Orientation (Point d)
r)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall d. Root d -> d -> DstRootSide 'LeftSide d
LDstRoot Orientation (Point d)
r d
f)

--------------------------------------------------------------------------------
-- xoDstRootSideR -

-- | the induced random variable for @'DstRootSide' 'RightSide' __d__'@.
xoDstRootSideR :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> X (DstRootSide RightSide d)
xoDstRootSideR :: forall d.
Distributive d =>
XOrtOrientation d
-> XOrtSite 'From d -> X (DstRootSide 'RightSide d)
xoDstRootSideR XOrtOrientation d
xo XOrtSite 'From d
xs
  = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL (forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation d
xo) (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From d
xs)

--------------------------------------------------------------------------------
-- xoDstSideL -

-- | the induced random variable for @'DstSide' 'LeftSide' __d__'@.
xoDstSideL :: Distributive d
  => XOrtOrientation d -> XOrtSite To d -> X (DstSide LeftSide d)
xoDstSideL :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL XOrtOrientation d
xo XOrtSite 'To d
xt = do
  Adbl2 d
a d
b <- forall a. FibredOriented a => XOrtOrientation a -> X (Adbl2 a)
xoAdbl2 XOrtOrientation d
xo
  d
f <- forall q. XOrtSite 'To q -> Point q -> X q
xosEnd XOrtSite 'To d
xt (forall q. Oriented q => q -> Point q
start d
a)
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall d. (d, d) -> d -> DstSide 'LeftSide d
LDst (d
a,d
b) d
f)

--------------------------------------------------------------------------------
-- xoDstSideR -

-- | the induced random variable for @'DstSide' 'RightSide' __d__'@.
xoDstSideR :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> X (DstSide RightSide d)
xoDstSideR :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> X (DstSide 'RightSide d)
xoDstSideR XOrtOrientation d
xo XOrtSite 'From d
xf = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL (forall q. XOrtOrientation q -> Dual (XOrtOrientation q)
coXOrtOrientation XOrtOrientation d
xo) (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From d
xf)

--------------------------------------------------------------------------------
-- xodDst -

-- | the induced random variable for 'Distributive' structures.
xoDst :: Distributive d
  => XOrtOrientation d -> XOrtSite From d -> XOrtSite To d -> XDst d
xoDst :: forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> XOrtSite 'To d -> XDst d
xoDst XOrtOrientation d
xo XOrtSite 'From d
xf XOrtSite 'To d
xt = forall d.
X (DstRootSide 'LeftSide d)
-> X (DstSide 'LeftSide d)
-> X (DstRootSide 'RightSide d)
-> X (DstSide 'RightSide d)
-> XDst d
XDst X (DstRootSide 'LeftSide d)
xrsl X (DstSide 'LeftSide d)
xsl X (DstRootSide 'RightSide d)
xrsr X (DstSide 'RightSide d)
xsr where
  xrsl :: X (DstRootSide 'LeftSide d)
xrsl = forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstRootSide 'LeftSide d)
xoDstRootSideL XOrtOrientation d
xo XOrtSite 'To d
xt
  xsl :: X (DstSide 'LeftSide d)
xsl = forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'To d -> X (DstSide 'LeftSide d)
xoDstSideL XOrtOrientation d
xo XOrtSite 'To d
xt
  xrsr :: X (DstRootSide 'RightSide d)
xrsr = forall d.
Distributive d =>
XOrtOrientation d
-> XOrtSite 'From d -> X (DstRootSide 'RightSide d)
xoDstRootSideR XOrtOrientation d
xo XOrtSite 'From d
xf
  xsr :: X (DstSide 'RightSide d)
xsr = forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> X (DstSide 'RightSide d)
xoDstSideR XOrtOrientation d
xo XOrtSite 'From d
xf