{-# LANGUAGE NoImplicitPrelude #-}

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


-- |
-- Module      : OAlg.Limes.Cone.EligibleFactor
-- Description : eligible factors between cones
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- eligible factors between 'Cone's.
module OAlg.Limes.Cone.EligibleFactor
  (
     -- * Eligible Factor
    cnEligibleFactor
  , EligibleFactor(..), elfFactorCone
  , elfMap
  
    -- ** Duality
  , coEligibleFactor, coEligibleFactorInv
  , elfFromOpOp

    -- ** X
  , xopEligibleFactor
  , XOrtPerspective(..)
  , XStandardOrtPerspective(..)
  
  , xosEligibleFactorPrj
  , xosEligibleFactorInj
  ) where

import Control.Monad

import Data.Typeable

import OAlg.Prelude

import OAlg.Entity.FinList
import OAlg.Entity.Diagram

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive

import OAlg.Hom.Multiplicative
import OAlg.Hom.Distributive
import OAlg.Hom.Definition

import OAlg.Limes.Perspective
import OAlg.Limes.Cone.Definition

--------------------------------------------------------------------------------
-- cnEligibleFactor -

-- | eligibility of a factor between two cones.
--
-- __Property__ Let @x@ be in __@a@__ and
-- @f@, @t@ in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ with
-- @'cnDiagram' f '==' 'cnDiagram' t@, then holds:
-- 
-- (1) If __@p@__ is equal to __'Projective'__ then holds:
-- @'cnEligibleFactor' x f t@ is 'True' if and only if
--
--     (1) @'orientation' x '==' 'tip' f ':>' 'tip' t@.
--
--     (2) @ti v'*' x '==' fi@ for all @ti@ in @'shell' t@ and @fi@ in @'shell' f@.
--
-- (2) If __@p@__ is equal to __'Injective'__ then holds:
-- @'cnEligibleFactor' x f t@ is 'True' if and only if
--
--     (1) @'orientation' x '==' 'tip' f ':>' 'tip' t@.
--
--     (2) @x v'*' ti '==' fi@ for all @ti@ in @'shell' t@ and @fi@ in @'shell' f@.
cnEligibleFactor :: a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor :: forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor a
x (ConeProjective Diagram t n m a
_ Point a
f FinList n a
fs) (ConeProjective Diagram t n m a
_ Point a
t FinList n a
ts)
  = forall q. Oriented q => q -> Orientation (Point q)
orientation a
x forall a. Eq a => a -> a -> Bool
== Point a
fforall p. p -> p -> Orientation p
:>Point a
t forall b. Boolean b => b -> b -> b
&& forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList n a -> Bool
comPrj a
x FinList n a
fs FinList n a
ts where
    comPrj :: Multiplicative a => a -> FinList n a -> FinList n a -> Bool
    comPrj :: forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList n a -> Bool
comPrj a
_ FinList n a
Nil FinList n a
Nil         = Bool
True
    comPrj a
x (a
f:|FinList n a
fs) (a
t:|FinList n a
ts) = a
tforall c. Multiplicative c => c -> c -> c
*a
x forall a. Eq a => a -> a -> Bool
== a
f forall b. Boolean b => b -> b -> b
&& forall a (n :: N').
Multiplicative a =>
a -> FinList n a -> FinList n a -> Bool
comPrj a
x FinList n a
fs FinList n a
ts
cnEligibleFactor a
x (ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
f) (ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
t)
  = forall q. Oriented q => q -> Orientation (Point q)
orientation a
x forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
start a
f forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
start a
t forall b. Boolean b => b -> b -> b
&& a
tforall c. Multiplicative c => c -> c -> c
*a
x forall a. Eq a => a -> a -> Bool
== a
f
cnEligibleFactor a
x Cone s p t n m a
f Cone s p t n m a
t = forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor (forall x. x -> Op x
Op a
x) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s p t n m a
t) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s p t n m a
f)

--------------------------------------------------------------------------------
-- EligibleFactor -

-- | predicate for eligible factors between cones.
--
-- __Property__ Let @e@ be in @'EligibleFactor' __s__ __p__ __t__ __n__ __m__ __a__@
-- for a 'Multiplicative' structure __@a@__, then holds:
--
-- (1) If @e@ matches @'EligibleFactorTo' l x c@ then holds:
-- @'cnDiagram' l '==' 'cnDiagram' c@ and @'cnEligibleFactor' x c l@.
--
-- (2) If @e@ matches @'EligibleFactorFrom' l x c@ then holds:
-- @'cnDiagram' l '==' 'cnDiagram' c@ and @'cnEligibleFactor' x l c@.
data EligibleFactor s p t n m a where
  EligibleFactorTo :: Cone s Projective t n m a -> a -> Cone s Projective t n m a
    -> EligibleFactor s Projective t n m a
  EligibleFactorFrom :: Cone s Injective t n m a -> a -> Cone s Injective t n m a
    -> EligibleFactor s Injective t n m a

deriving instance Show a => Show (EligibleFactor s p t n m a)
--------------------------------------------------------------------------------
-- elfFactorCone -

-- | the underlying factor together with its cone.
elfFactorCone :: EligibleFactor s p t n m a -> (a,Cone s p t n m a)
elfFactorCone :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
EligibleFactor s p t n m a -> (a, Cone s p t n m a)
elfFactorCone (EligibleFactorTo Cone s 'Projective t n m a
_ a
x Cone s 'Projective t n m a
c)   = (a
x,Cone s 'Projective t n m a
c)
elfFactorCone (EligibleFactorFrom Cone s 'Injective t n m a
_ a
x Cone s 'Injective t n m a
c) = (a
x,Cone s 'Injective t n m a
c)

--------------------------------------------------------------------------------
-- elfMap -

-- | mapping of a eligible factor within a 'Multiplicative' structure.
elfMapMlt :: Hom Mlt h
  => h a b -> EligibleFactor Mlt p t n m a -> EligibleFactor Mlt p t n m b
elfMapMlt :: forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b
-> EligibleFactor Mlt p t n m a -> EligibleFactor Mlt p t n m b
elfMapMlt h a b
h EligibleFactor Mlt p t n m a
elf = case EligibleFactor Mlt p t n m a
elf of
  EligibleFactorTo Cone Mlt 'Projective t n m a
l a
x Cone Mlt 'Projective t n m a
c   -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a
-> Cone s 'Projective t n m a
-> EligibleFactor s 'Projective t n m a
EligibleFactorTo (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone Mlt 'Projective t n m a
l) (h a b
hforall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$a
x) (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone Mlt 'Projective t n m a
c)
  EligibleFactorFrom Cone Mlt 'Injective t n m a
l a
x Cone Mlt 'Injective t n m a
c -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> a
-> Cone s 'Injective t n m a
-> EligibleFactor s 'Injective t n m a
EligibleFactorFrom (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone Mlt 'Injective t n m a
l) (h a b
hforall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$a
x) (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b -> Cone Mlt p t n m a -> Cone Mlt p t n m b
cnMapMlt h a b
h Cone Mlt 'Injective t n m a
c)

-- | mapping of a eligible factor within a 'Distributive' structure.
elfMapDst :: Hom Dst h
  => h a b -> EligibleFactor Dst p t n m a -> EligibleFactor Dst p t n m b
elfMapDst :: forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b
-> EligibleFactor Dst p t n m a -> EligibleFactor Dst p t n m b
elfMapDst h a b
h EligibleFactor Dst p t n m a
elf = case EligibleFactor Dst p t n m a
elf of
  EligibleFactorTo Cone Dst 'Projective t n m a
l a
x Cone Dst 'Projective t n m a
c   -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a
-> Cone s 'Projective t n m a
-> EligibleFactor s 'Projective t n m a
EligibleFactorTo (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone Dst 'Projective t n m a
l) (h a b
hforall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$a
x) (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone Dst 'Projective t n m a
c)
  EligibleFactorFrom Cone Dst 'Injective t n m a
l a
x Cone Dst 'Injective t n m a
c -> forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> a
-> Cone s 'Injective t n m a
-> EligibleFactor s 'Injective t n m a
EligibleFactorFrom (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone Dst 'Injective t n m a
l) (h a b
hforall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$a
x) (forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b -> Cone Dst p t n m a -> Cone Dst p t n m b
cnMapDst h a b
h Cone Dst 'Injective t n m a
c)

-- | mapping of a eligible factor.  
elfMap :: Hom s h
  => h a b -> EligibleFactor s p t n m a -> EligibleFactor s p t n m b
elfMap :: forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
Hom s h =>
h a b -> EligibleFactor s p t n m a -> EligibleFactor s p t n m b
elfMap h a b
h elf :: EligibleFactor s p t n m a
elf@(EligibleFactorTo Cone s 'Projective t n m a
l a
_ Cone s 'Projective t n m a
_) = case Cone s 'Projective t n m a
l of
  ConeProjective Diagram t n m a
_ Point a
_ FinList n a
_ -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b
-> EligibleFactor Mlt p t n m a -> EligibleFactor Mlt p t n m b
elfMapMlt h a b
h EligibleFactor s p t n m a
elf  
  ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
_ a
_       -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b
-> EligibleFactor Dst p t n m a -> EligibleFactor Dst p t n m b
elfMapDst h a b
h EligibleFactor s p t n m a
elf  
elfMap h a b
h elf :: EligibleFactor s p t n m a
elf@(EligibleFactorFrom Cone s 'Injective t n m a
l a
_ Cone s 'Injective t n m a
_) = case Cone s 'Injective t n m a
l of  
  ConeInjective Diagram t n m a
_ Point a
_ FinList n a
_  -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b
-> EligibleFactor Mlt p t n m a -> EligibleFactor Mlt p t n m b
elfMapMlt h a b
h EligibleFactor s p t n m a
elf  
  ConeCokernel Diagram ('Parallel 'RightToLeft) ('S N1) m a
_ a
_     -> forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b
-> EligibleFactor Dst p t n m a -> EligibleFactor Dst p t n m b
elfMapDst h a b
h EligibleFactor s p t n m a
elf

--------------------------------------------------------------------------------
-- EligibleFactor - Duality -

type instance Dual (EligibleFactor s p t n m a)
  = EligibleFactor s (Dual p) (Dual t) n m (Op a)

-- | to the dual, with its inverse 'coEligibleFactorInv'.
coEligibleFactor :: EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)
coEligibleFactor :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)
coEligibleFactor (EligibleFactorTo Cone s 'Projective t n m a
l a
x Cone s 'Projective t n m a
c) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> a
-> Cone s 'Injective t n m a
-> EligibleFactor s 'Injective t n m a
EligibleFactorFrom Dual (Cone s 'Projective t n m a)
l' (forall x. x -> Op x
Op a
x) Dual (Cone s 'Projective t n m a)
c' where
  l' :: Dual (Cone s 'Projective t n m a)
l' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Projective t n m a
l
  c' :: Dual (Cone s 'Projective t n m a)
c' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Projective t n m a
c
coEligibleFactor (EligibleFactorFrom Cone s 'Injective t n m a
l a
x Cone s 'Injective t n m a
c) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a
-> Cone s 'Projective t n m a
-> EligibleFactor s 'Projective t n m a
EligibleFactorTo Dual (Cone s 'Injective t n m a)
l' (forall x. x -> Op x
Op a
x) Dual (Cone s 'Injective t n m a)
c' where
  l' :: Dual (Cone s 'Injective t n m a)
l' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Injective t n m a
l
  c' :: Dual (Cone s 'Injective t n m a)
c' = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone Cone s 'Injective t n m a
c

-- | from the bidual.
elfFromOpOp :: ConeStruct s a
  -> EligibleFactor s p t n m (Op (Op a)) -> EligibleFactor s p t n m a
elfFromOpOp :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> EligibleFactor s p t n m (Op (Op a))
-> EligibleFactor s p t n m a
elfFromOpOp ConeStruct s a
ConeStructMlt = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Mlt h =>
h a b
-> EligibleFactor Mlt p t n m a -> EligibleFactor Mlt p t n m b
elfMapMlt forall a. Multiplicative a => IsoOp Mlt (Op (Op a)) a
isoFromOpOpMlt
elfFromOpOp ConeStruct s a
ConeStructDst = forall (h :: * -> * -> *) a b (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N').
Hom Dst h =>
h a b
-> EligibleFactor Dst p t n m a -> EligibleFactor Dst p t n m b
elfMapDst forall a. Distributive a => IsoOp Dst (Op (Op a)) a
isoFromOpOpDst

-- | from the dual, with its inverse 'coEligibleFactor'.
coEligibleFactorInv :: ConeStruct s a -> Dual (Dual p) :~: p -> Dual (Dual t) :~: t
  -> Dual (EligibleFactor s p t n m a) -> EligibleFactor s p t n m a
coEligibleFactorInv :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (EligibleFactor s p t n m a)
-> EligibleFactor s p t n m a
coEligibleFactorInv ConeStruct s a
cs Dual (Dual p) :~: p
Refl Dual (Dual t) :~: t
Refl = forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> EligibleFactor s p t n m (Op (Op a))
-> EligibleFactor s p t n m a
elfFromOpOp ConeStruct s a
cs forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)
coEligibleFactor

--------------------------------------------------------------------------------
-- EligibleFactor - Validable -

instance Oriented a => Validable (EligibleFactor s p t n m a) where
  valid :: EligibleFactor s p t n m a -> Statement
valid (EligibleFactorTo Cone s 'Projective t n m a
l a
x Cone s 'Projective t n m a
c) = String -> Label
Label String
"EligibleFactorTo" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Cone s 'Projective t n m a
l
        , forall a. Validable a => a -> Statement
valid a
x
        , forall a. Validable a => a -> Statement
valid Cone s 'Projective t n m a
c
        , String -> Label
Label String
"diagram" Label -> Statement -> Statement
:<=>:
            (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s 'Projective t n m a
l forall a. Eq a => a -> a -> Bool
== forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s 'Projective t n m a
c)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s 'Projective t n m a
l,String
"c"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s 'Projective t n m a
c]
        , String -> Label
Label String
"eligible" Label -> Statement -> Statement
:<=>:
            (forall a s (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
a -> Cone s p t n m a -> Cone s p t n m a -> Bool
cnEligibleFactor a
x Cone s 'Projective t n m a
c Cone s 'Projective t n m a
l)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show a
x,String
"l"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s 'Projective t n m a
l,String
"c"String -> String -> Parameter
:=forall a. Show a => a -> String
show Cone s 'Projective t n m a
c]
        ] 
  valid elf :: EligibleFactor s p t n m a
elf@(EligibleFactorFrom Cone s 'Injective t n m a
_ a
_ Cone s 'Injective t n m a
_) = forall a. Validable a => a -> Statement
valid (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
EligibleFactor s p t n m a -> Dual (EligibleFactor s p t n m a)
coEligibleFactor EligibleFactor s p t n m a
elf)

--------------------------------------------------------------------------------
-- xosEligibleFactorPrj -

-- | the induced random variable of eligible factors.
xosEligibleFactorPrj :: XOrtSite To a -> Cone s Projective t n m a
  -> X (EligibleFactor s Projective t n m a)
xosEligibleFactorPrj :: forall a s (t :: DiagramType) (n :: N') (m :: N').
XOrtSite 'To a
-> Cone s 'Projective t n m a
-> X (EligibleFactor s 'Projective t n m a)
xosEligibleFactorPrj (XEnd X (Point a)
_ Point a -> X a
xe) Cone s 'Projective t n m a
l
  = Point a -> X a
xe (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone s 'Projective t n m a
l) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a -> EligibleFactor s 'Projective t n m a
elf Cone s 'Projective t n m a
l where
    elf :: Cone s Projective t n m a -> a -> EligibleFactor s Projective t n m a
    elf :: forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a -> EligibleFactor s 'Projective t n m a
elf l :: Cone s 'Projective t n m a
l@(ConeProjective Diagram t n m a
d Point a
_ FinList n a
cs) a
x = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a
-> Cone s 'Projective t n m a
-> EligibleFactor s 'Projective t n m a
EligibleFactorTo Cone s 'Projective t n m a
l a
x (forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram t n m a
d (forall q. Oriented q => q -> Point q
start a
x) FinList n a
cs')
      where cs' :: FinList n a
cs' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall c. Multiplicative c => c -> c -> c
*a
x) FinList n a
cs
    elf l :: Cone s 'Projective t n m a
l@(ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d a
k) a
x = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> a
-> Cone s 'Projective t n m a
-> EligibleFactor s 'Projective t n m a
EligibleFactorTo Cone s 'Projective t n m a
l a
x (forall a (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel Diagram ('Parallel 'LeftToRight) ('S N1) m a
d (a
kforall c. Multiplicative c => c -> c -> c
*a
x))

--------------------------------------------------------------------------------
-- xosEligibleFactorInj -

-- | the induced random variable of eligible factors.
xosEligibleFactorInj :: ConeStruct s a -> Dual (Dual t) :~: t
  -> XOrtSite From a -> Cone s Injective t n m a
  -> X (EligibleFactor s Injective t n m a)
xosEligibleFactorInj :: forall s a (t :: DiagramType) (n :: N') (m :: N').
ConeStruct s a
-> (Dual (Dual t) :~: t)
-> XOrtSite 'From a
-> Cone s 'Injective t n m a
-> X (EligibleFactor s 'Injective t n m a)
xosEligibleFactorInj ConeStruct s a
cs Dual (Dual t) :~: t
rt XOrtSite 'From a
xos
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> Dual (EligibleFactor s p t n m a)
-> EligibleFactor s p t n m a
coEligibleFactorInv ConeStruct s a
cs forall {k} (a :: k). a :~: a
Refl Dual (Dual t) :~: t
rt) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall a s (t :: DiagramType) (n :: N') (m :: N').
XOrtSite 'To a
-> Cone s 'Projective t n m a
-> X (EligibleFactor s 'Projective t n m a)
xosEligibleFactorPrj (forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From a
xos) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Dual (Cone s p t n m a)
coCone

--------------------------------------------------------------------------------
-- XOrtPerspective -

-- | random variable given by a 'XOrtSite'.
data XOrtPerspective p a where
  XOrtProjective :: XOrtSite To a -> XOrtPerspective Projective a
  XOrtInjective :: XOrtSite From a -> XOrtPerspective Injective a

--------------------------------------------------------------------------------
-- xopEligibleFactor -

-- | the induced random variable of eligible factors.
xopEligibleFactor :: ConeStruct s a -> XOrtPerspective p a
  -> Cone s p t n m a -> X (EligibleFactor s p t n m a)
xopEligibleFactor :: forall s a (p :: Perspective) (t :: DiagramType) (n :: N')
       (m :: N').
ConeStruct s a
-> XOrtPerspective p a
-> Cone s p t n m a
-> X (EligibleFactor s p t n m a)
xopEligibleFactor ConeStruct s a
_ (XOrtProjective XOrtSite 'To a
xos) Cone s p t n m a
c = forall a s (t :: DiagramType) (n :: N') (m :: N').
XOrtSite 'To a
-> Cone s 'Projective t n m a
-> X (EligibleFactor s 'Projective t n m a)
xosEligibleFactorPrj XOrtSite 'To a
xos Cone s p t n m a
c
xopEligibleFactor ConeStruct s a
cs (XOrtInjective XOrtSite 'From a
xos) Cone s p t n m a
c
  = forall s a (t :: DiagramType) (n :: N') (m :: N').
ConeStruct s a
-> (Dual (Dual t) :~: t)
-> XOrtSite 'From a
-> Cone s 'Injective t n m a
-> X (EligibleFactor s 'Injective t n m a)
xosEligibleFactorInj ConeStruct s a
cs (forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Diagram t n m a
cnDiagram Cone s p t n m a
c) XOrtSite 'From a
xos Cone s p t n m a
c

--------------------------------------------------------------------------------
-- XStandardOrtPerspective -

-- | standard random variable for 'XOrtPerspective'.
class XStandardOrtPerspective p a where
  xStandardOrtPerspective :: XOrtPerspective p a

instance XStandardOrtSiteTo a => XStandardOrtPerspective Projective a where
  xStandardOrtPerspective :: XOrtPerspective 'Projective a
xStandardOrtPerspective = forall a. XOrtSite 'To a -> XOrtPerspective 'Projective a
XOrtProjective forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite

instance XStandardOrtSiteFrom a => XStandardOrtPerspective Injective a where
  xStandardOrtPerspective :: XOrtPerspective 'Injective a
xStandardOrtPerspective = forall a. XOrtSite 'From a -> XOrtPerspective 'Injective a
XOrtInjective forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite