{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}

-- |
-- Module      : OAlg.Category.Proposition
-- Description : properties on categories
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on categories.
module OAlg.Category.Proposition
  (
    -- * Category
    prpCategory, XCat(..)
  , prpCategory1
  , prpCategory2, SomeCmpb3(..)

    -- * Application
  , XAppl

    -- * Functorial
  , prpFunctorial, XFnct(..)
  , prpFunctorial1
  , prpFunctorial2, SomeCmpbAppl(..)

    -- * Cayleyan2
  , prpCayleyan2

    -- * X
    -- ** Categroy
  , xCat, XMrphSite(..), xSomePathSiteMax, xSomePathMax
  , xSomePathSite, xSomePath

    -- ** Functorial
  , xFnct, xMrphSite, XFnctMrphSite(..)
  
  )
  where

import Control.Monad
import Control.Exception

import Data.Proxy

import OAlg.Control.Exception

import OAlg.Category.Definition
import OAlg.Structure.Definition

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

import OAlg.Data.X
import OAlg.Data.Number
import OAlg.Data.Dualisable
import OAlg.Data.Opposite
import OAlg.Data.Statement
import OAlg.Data.Show
import OAlg.Data.Equal
import OAlg.Data.Boolean

import OAlg.Entity.Definition

--------------------------------------------------------------------------------
-- XMorphismException -

-- | arithmetic exceptions which are sub exceptions from 'SomeOAlgException'.
data XMorphismException
  = NoSuchEntity
  deriving (XMorphismException -> XMorphismException -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: XMorphismException -> XMorphismException -> Bool
$c/= :: XMorphismException -> XMorphismException -> Bool
== :: XMorphismException -> XMorphismException -> Bool
$c== :: XMorphismException -> XMorphismException -> Bool
Eq,Int -> XMorphismException -> ShowS
[XMorphismException] -> ShowS
XMorphismException -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [XMorphismException] -> ShowS
$cshowList :: [XMorphismException] -> ShowS
show :: XMorphismException -> String
$cshow :: XMorphismException -> String
showsPrec :: Int -> XMorphismException -> ShowS
$cshowsPrec :: Int -> XMorphismException -> ShowS
Show)

instance Exception XMorphismException where
  toException :: XMorphismException -> SomeException
toException   = forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe XMorphismException
fromException = forall e. Exception e => SomeException -> Maybe e
oalgExceptionFromException

--------------------------------------------------------------------------------
-- XAppl -

-- | random variable for some application.
type XAppl h = X (SomeApplication h)

--------------------------------------------------------------------------------
-- prpCategory1 -

-- | validity according to "OAlg.Category.Category#Cat1".
prpCategory1 :: (Category c, Show2 c, Eq2 c) => X (SomeMorphism c) -> Statement
prpCategory1 :: forall (c :: * -> * -> *).
(Category c, Show2 c, Eq2 c) =>
X (SomeMorphism c) -> Statement
prpCategory1 X (SomeMorphism c)
xsm = String -> Label
Prp String
"Category1"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism c)
xsm (\(SomeMorphism c x y
f)
                    -> let == :: c x y -> c x y -> Bool
(==) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2
                           prm :: Message
prm  = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
f]
                        in [Statement] -> Statement
And [ ((forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f) forall {x} {y}. c x y -> c x y -> Bool
== c x y
f) Bool -> Message -> Statement
:?> Message
prm
                               , (c x y
f forall {x} {y}. c x y -> c x y -> Bool
== (c x y
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f))) Bool -> Message -> Statement
:?> Message
prm
                               ]
                   )

--------------------------------------------------------------------------------
-- SomeCmpb3 -

-- | some composable morphisms.
data SomeCmpb3 c where
  SomeCmpb3 :: c x w -> c y x ->  c z y -> SomeCmpb3 c

--------------------------------------------------------------------------------
-- prpCategory2

relCategory2 :: (Category c, Show2 c, Eq2 c) => c x w -> c y x ->  c z y -> Statement
relCategory2 :: forall (c :: * -> * -> *) x w y z.
(Category c, Show2 c, Eq2 c) =>
c x w -> c y x -> c z y -> Statement
relCategory2 c x w
f c y x
g c z y
h
  = (((c x w
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
g) forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
h) forall {x} {y}. c x y -> c x y -> Bool
== (c x w
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (c y x
g forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
h))) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x w
f,String
"g"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y x
g,String
"h"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c z y
h]
  where == :: c x y -> c x y -> Bool
(==) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2

relCategory2Path :: (Category c, Show2 c, Eq2 c) => Path c x y -> Statement
relCategory2Path :: forall (c :: * -> * -> *) x y.
(Category c, Show2 c, Eq2 c) =>
Path c x y -> Statement
relCategory2Path (c y y
f :. c y y
g :. c y y
h :. Path c x y
pth)
  = forall (c :: * -> * -> *) x w y z.
(Category c, Show2 c, Eq2 c) =>
c x w -> c y x -> c z y -> Statement
relCategory2 c y y
f c y y
g c y y
h forall b. Boolean b => b -> b -> b
&& forall (c :: * -> * -> *) x y.
(Category c, Show2 c, Eq2 c) =>
Path c x y -> Statement
relCategory2Path (c y y
g forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. c y y
h forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. Path c x y
pth) 
relCategory2Path Path c x y
_  = Statement
SValid

-- | validity according to "OAlg.Category.Category#Cat2".
prpCategory2 :: (Category c, Show2 c, Eq2 c) => X (SomeCmpb3 c) -> Statement
prpCategory2 :: forall (c :: * -> * -> *).
(Category c, Show2 c, Eq2 c) =>
X (SomeCmpb3 c) -> Statement
prpCategory2 X (SomeCmpb3 c)
xpth = String -> Label
Prp String
"Category2"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeCmpb3 c)
xpth (\(SomeCmpb3 c x w
f c y x
g c z y
h) -> forall (c :: * -> * -> *) x w y z.
(Category c, Show2 c, Eq2 c) =>
c x w -> c y x -> c z y -> Statement
relCategory2 c x w
f c y x
g c z y
h)

--------------------------------------------------------------------------------
-- XCat -

-- | random variable for validating 'Category'.
data XCat c
  = XCat
  { forall (c :: * -> * -> *). XCat c -> X (SomeMorphism c)
xcSomeMrph  :: X (SomeMorphism c)
  , forall (c :: * -> * -> *). XCat c -> X (SomeCmpb3 c)
xcSomeCmpb3 :: X (SomeCmpb3 c)
  }

--------------------------------------------------------------------------------
-- prpCategory -

-- | validity of a 'Category'.
prpCategory :: (Category c, Eq2 c, Show2 c) => XCat c -> Statement
prpCategory :: forall (c :: * -> * -> *).
(Category c, Eq2 c, Show2 c) =>
XCat c -> Statement
prpCategory (XCat X (SomeMorphism c)
xm X (SomeCmpb3 c)
xc3) = String -> Label
Prp String
"Category"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall (c :: * -> * -> *).
(Category c, Show2 c, Eq2 c) =>
X (SomeMorphism c) -> Statement
prpCategory1 X (SomeMorphism c)
xm
            , forall (c :: * -> * -> *).
(Category c, Show2 c, Eq2 c) =>
X (SomeCmpb3 c) -> Statement
prpCategory2 X (SomeCmpb3 c)
xc3
            ]

--------------------------------------------------------------------------------
-- prpFunctorial1 -

-- | validity according to "OAlg.Category.Category#Fnc1".
prpFunctorial1 :: (Functorial c, Show2 c) => X (SomeEntity c) -> Statement
prpFunctorial1 :: forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
X (SomeEntity c) -> Statement
prpFunctorial1 X (SomeEntity c)
xid = String -> Label
Prp String
"Functorial1"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeEntity c)
xid (\(SomeEntity Struct (ObjectClass c) x
d x
x)
                    -> let od :: c x x
od = forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' (forall (c :: * -> * -> *). X (SomeEntity c) -> Proxy c
p X (SomeEntity c)
xid) Struct (ObjectClass c) x
d
                        in (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap c x x
od x
x forall a. Eq a => a -> a -> Bool
== x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"od"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x x
od,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show x
x]
                   )
  where p :: X (SomeEntity c) -> Proxy c
        p :: forall (c :: * -> * -> *). X (SomeEntity c) -> Proxy c
p X (SomeEntity c)
_ = forall {k} (t :: k). Proxy t
Proxy

--------------------------------------------------------------------------------
-- SomeCmpbAppl -

-- | some composable morphisms with an applicable value.
data SomeCmpbAppl c where
  SomeCmpbAppl :: (Entity x, Eq z) => c y z -> c x y -> x -> SomeCmpbAppl c

--------------------------------------------------------------------------------
-- prpFunctorial2 -

-- | validity according to "OAlg.Category.Category#Fnc2".
prpFunctorial2 :: (Functorial c, Show2 c)
  => X (SomeCmpbAppl c) -> Statement
prpFunctorial2 :: forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
X (SomeCmpbAppl c) -> Statement
prpFunctorial2 X (SomeCmpbAppl c)
xca = String -> Label
Prp String
"Functorial2"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeCmpbAppl c)
xca (\(SomeCmpbAppl c y z
f c x y
g x
x)
                    -> (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap (c y z
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
g) x
x forall a. Eq a => a -> a -> Bool
== (forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap c y z
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
amap c x y
g) x
x)
                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y z
f,String
"g"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
g,String
"x"String -> String -> Parameter
:=forall a. Show a => a -> String
show x
x]
                   )

--------------------------------------------------------------------------------
-- XFnct - 

-- | random variable for 'Functorial' categories.
data XFnct c where
  XFnct :: X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c

--------------------------------------------------------------------------------
-- prpFunctorial -

-- | validity of a 'Functorial' category.
prpFunctorial :: (Functorial c, Show2 c) => XFnct c -> Statement
prpFunctorial :: forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
XFnct c -> Statement
prpFunctorial (XFnct X (SomeEntity c)
xd X (SomeCmpbAppl c)
xca) = String -> Label
Prp String
"Functorial"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
X (SomeEntity c) -> Statement
prpFunctorial1 X (SomeEntity c)
xd
            , forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
X (SomeCmpbAppl c) -> Statement
prpFunctorial2 X (SomeCmpbAppl c)
xca
            ]

--------------------------------------------------------------------------------
-- prpCayleyan2 -

-- | validity of 'Cayleyan2'.
prpCayleyan2 :: (Cayleyan2 c, Show2 c) => X (SomeMorphism c) -> Statement
prpCayleyan2 :: forall (c :: * -> * -> *).
(Cayleyan2 c, Show2 c) =>
X (SomeMorphism c) -> Statement
prpCayleyan2 X (SomeMorphism c)
xmp = String -> Label
Prp String
"Cayleyan2"
  Label -> Statement -> Statement
:<=>: forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism c)
xmp (\(SomeMorphism c x y
f)
                    -> let prm :: Message
prm  = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
f]
                           == :: c x y -> c x y -> Bool
(==) = forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2
                           f' :: c y x
f'   = forall (c :: * -> * -> *) x y. Cayleyan2 c => c x y -> c y x
invert2 c x y
f
                        in [Statement] -> Statement
And [ ((c y x
f' forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f) forall {x} {y}. c x y -> c x y -> Bool
== forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f)) Bool -> Message -> Statement
:?> Message
prm
                               , ((c x y
f forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
f') forall {x} {y}. c x y -> c x y -> Bool
== forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f)) Bool -> Message -> Statement
:?> Message
prm
                               ]
                   )

--------------------------------------------------------------------------------
-- XMrphSite -

-- | random variable of 'SomeObjectClass' and 'SomeMorphismSite' with:
--
--   __Note__
--
--   (1) The random variable @'X' ('SomeObjectClass' m)@ should have a bias towards non
--   terminal respectively initial object classes. For an implementation see
--   'OAlg.Proposition.Homomorphism.Oriented.xIsoOpOrtFrom'.
--
--   (1) It is the analogue to 'OAlg.Proposition.Structure.Oriented.XStart' at the level
--   of 'Category's.
data XMrphSite (s :: Site) m where
  XDomain ::
       X (SomeObjectClass m)
    -> (forall x . Struct (ObjectClass m) x -> X (SomeMorphismSite From m x))
    -> XMrphSite From m
  XRange ::
       X (SomeObjectClass m)
    -> (forall y . Struct (ObjectClass m) y -> X (SomeMorphismSite To m y))
    -> XMrphSite To m

type instance Dual (XMrphSite s m) = XMrphSite (Dual s) (Op2 m)

instance Dualisable (XMrphSite To m) where
  toDual :: XMrphSite 'To m -> Dual (XMrphSite 'To m)
toDual xmt :: XMrphSite 'To m
xmt@(XRange X (SomeObjectClass m)
xo forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
_) = forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall x.
    Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x))
-> XMrphSite 'From m
XDomain (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => x -> Dual x
toDual X (SomeObjectClass m)
xo) (forall (m :: * -> * -> *) x.
XMrphSite 'To m
-> Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
xsm' XMrphSite 'To m
xmt) where
    xsm' :: XMrphSite To m
        -> Struct (ObjectClass (Op2 m)) x -> X (SomeMorphismSite From (Op2 m) x)
    xsm' :: forall (m :: * -> * -> *) x.
XMrphSite 'To m
-> Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
xsm' (XRange X (SomeObjectClass m)
_ forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm) Struct (ObjectClass (Op2 m)) x
xo' = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => x -> Dual x
toDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm Struct (ObjectClass (Op2 m)) x
xo'

  fromDual :: Dual (XMrphSite 'To m) -> XMrphSite 'To m
fromDual xmf :: Dual (XMrphSite 'To m)
xmf@(XDomain X (SomeObjectClass (Op2 m))
xo' forall x.
Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
_) = forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall y.
    Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y))
-> XMrphSite 'To m
XRange (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual X (SomeObjectClass (Op2 m))
xo') (forall (m :: * -> * -> *) y.
XMrphSite 'From (Op2 m)
-> Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm Dual (XMrphSite 'To m)
xmf) where
    xsm :: XMrphSite From (Op2 m)
        -> Struct (ObjectClass m) y -> X (SomeMorphismSite To m y)
    xsm :: forall (m :: * -> * -> *) y.
XMrphSite 'From (Op2 m)
-> Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm (XDomain X (SomeObjectClass (Op2 m))
_ forall x.
Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
xsm') Struct (ObjectClass m) y
xo = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x.
Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
xsm' Struct (ObjectClass m) y
xo

--------------------------------------------------------------------------------
-- xSomeObjectClass -

-- | the underlying random variable for some object class.
xSomeObjectClass :: XMrphSite s m -> X (SomeObjectClass m)
xSomeObjectClass :: forall (s :: Site) (m :: * -> * -> *).
XMrphSite s m -> X (SomeObjectClass m)
xSomeObjectClass (XDomain X (SomeObjectClass m)
xso forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
_) = X (SomeObjectClass m)
xso
xSomeObjectClass (XRange X (SomeObjectClass m)
xso forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
_) = X (SomeObjectClass m)
xso

--------------------------------------------------------------------------------
-- xSomePathSiteMax -

-- | random variable of paths of 'Morphism's having maximal the given length. If during
--   the randomly build path no terminal respectively initial object class has reached
--   then the resulting path will have the given length.
--
--   It is the analogue to 'OAlg.Proposition.Structure.Oriented.xStartPathOrt' at the
--   level of 'Category's.
xSomePathSiteMax :: Morphism m
  => XMrphSite s m -> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax :: forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax xmf :: XMrphSite s m
xmf@(XDomain X (SomeObjectClass m)
_ forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
_) N
n Struct (ObjectClass m) x
d = forall (m :: * -> * -> *) x y.
Morphism m =>
XMrphSite 'From m
-> N
-> Struct (ObjectClass m) x
-> Struct (ObjectClass m) y
-> Path m x y
-> X (SomePathSite 'From m x)
pth XMrphSite s m
xmf N
n Struct (ObjectClass m) x
d Struct (ObjectClass m) x
d (forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass m) x
d) where
  pth :: Morphism m
      => XMrphSite From m
      -> N -> Struct (ObjectClass m) x -> Struct (ObjectClass m) y
      -> Path m x y -> X (SomePathSite From m x)
  pth :: forall (m :: * -> * -> *) x y.
Morphism m =>
XMrphSite 'From m
-> N
-> Struct (ObjectClass m) x
-> Struct (ObjectClass m) y
-> Path m x y
-> X (SomePathSite 'From m x)
pth XMrphSite 'From m
_ N
0 Struct (ObjectClass m) x
_ Struct (ObjectClass m) y
_ Path m x y
fs                      = forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x x. Path m x x -> SomePathSite 'From m x
SomePathDomain Path m x y
fs
  pth xd :: XMrphSite 'From m
xd@(XDomain X (SomeObjectClass m)
_ forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
xmf) N
n Struct (ObjectClass m) x
d Struct (ObjectClass m) y
r Path m x y
fs = case forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
xmf Struct (ObjectClass m) y
r of
    X (SomeMorphismSite 'From m y)
XEmpty -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x x. Path m x x -> SomePathSite 'From m x
SomePathDomain Path m x y
fs
    X (SomeMorphismSite 'From m y)
xf     -> X (SomeMorphismSite 'From m y)
xf forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(SomeMorphismDomain m y y
f) -> forall (m :: * -> * -> *) x y.
Morphism m =>
XMrphSite 'From m
-> N
-> Struct (ObjectClass m) x
-> Struct (ObjectClass m) y
-> Path m x y
-> X (SomePathSite 'From m x)
pth XMrphSite 'From m
xd (forall a. Enum a => a -> a
pred N
n) Struct (ObjectClass m) x
d (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m y y
f) (m y y
f forall (m :: * -> * -> *) x z x. m x z -> Path m x x -> Path m x z
:. Path m x y
fs)

xSomePathSiteMax xmt :: XMrphSite s m
xmt@(XRange X (SomeObjectClass m)
_ forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
_) N
n Struct (ObjectClass m) x
d
  = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax (forall x. Dualisable x => x -> Dual x
toDual XMrphSite s m
xmt) N
n Struct (ObjectClass m) x
d

--------------------------------------------------------------------------------
-- xSomePathMax -

-- | derived random variable for some paths.
xSomePathMax :: Morphism m => XMrphSite s m -> N -> X (SomePath m)
xSomePathMax :: forall (m :: * -> * -> *) (s :: Site).
Morphism m =>
XMrphSite s m -> N -> X (SomePath m)
xSomePathMax xmf :: XMrphSite s m
xmf@(XDomain X (SomeObjectClass m)
xo forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
_) N
n = do
  SomeObjectClass Struct (ObjectClass m) x
o <- X (SomeObjectClass m)
xo
  SomePathSite s m x
pth <- forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax XMrphSite s m
xmf N
n Struct (ObjectClass m) x
o
  forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (s :: Site) (m :: * -> * -> *) x.
SomePathSite s m x -> SomePath m
somePath SomePathSite s m x
pth
xSomePathMax xmt :: XMrphSite s m
xmt@(XRange X (SomeObjectClass m)
_ forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
_) N
n = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) (s :: Site).
Morphism m =>
XMrphSite s m -> N -> X (SomePath m)
xSomePathMax (forall x. Dualisable x => x -> Dual x
toDual XMrphSite s m
xmt) N
n

--------------------------------------------------------------------------------
-- adjOne -

-- | adjoining 'cOne' for empty random variables.
adjOne :: Category c => XMrphSite s c -> XMrphSite s c
adjOne :: forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XMrphSite s c
adjOne xmf :: XMrphSite s c
xmf@(XDomain X (SomeObjectClass c)
xo forall x.
Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
_) = forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall x.
    Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x))
-> XMrphSite 'From m
XDomain X (SomeObjectClass c)
xo (forall (c :: * -> * -> *) x.
Category c =>
XMrphSite 'From c
-> Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm' XMrphSite s c
xmf) where
  xsm' :: Category c
       => XMrphSite From c
       -> Struct (ObjectClass c) x -> X (SomeMorphismSite From c x)
  xsm' :: forall (c :: * -> * -> *) x.
Category c =>
XMrphSite 'From c
-> Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm' (XDomain X (SomeObjectClass c)
_ forall x.
Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm) Struct (ObjectClass c) x
o = case forall x.
Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm Struct (ObjectClass c) x
o of
    X (SomeMorphismSite 'From c x)
XEmpty -> forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x x. m x x -> SomeMorphismSite 'From m x
SomeMorphismDomain forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass c) x
o
    X (SomeMorphismSite 'From c x)
xm     -> X (SomeMorphismSite 'From c x)
xm
adjOne xmt :: XMrphSite s c
xmt@(XRange X (SomeObjectClass c)
_ forall y. Struct (ObjectClass c) y -> X (SomeMorphismSite 'To c y)
_) = forall x. Dualisable x => Dual x -> x
fromDual forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XMrphSite s c
adjOne forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall x. Dualisable x => x -> Dual x
toDual XMrphSite s c
xmt

--------------------------------------------------------------------------------
-- xSomePathSite -

-- | constructing random variable for some path site.
xSomePathSite :: Category c
  => XMrphSite s c -> N -> Struct (ObjectClass c) x -> X (SomePathSite s c x)
xSomePathSite :: forall (c :: * -> * -> *) (s :: Site) x.
Category c =>
XMrphSite s c
-> N -> Struct (ObjectClass c) x -> X (SomePathSite s c x)
xSomePathSite XMrphSite s c
xm = forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax (forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XMrphSite s c
adjOne XMrphSite s c
xm)

--------------------------------------------------------------------------------
-- xSomePath -

-- | constructing random variable for some path.
xSomePath :: Category c => XMrphSite s c -> N -> X (SomePath c)
xSomePath :: forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xm = forall (m :: * -> * -> *) (s :: Site).
Morphism m =>
XMrphSite s m -> N -> X (SomePath m)
xSomePathMax (forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XMrphSite s c
adjOne XMrphSite s c
xm)

--------------------------------------------------------------------------------
-- xCat -

-- | random variable for validating 'Category'.
xCat :: Category c => XMrphSite s c -> XCat c
xCat :: forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XCat c
xCat XMrphSite s c
xm = forall (c :: * -> * -> *).
X (SomeMorphism c) -> X (SomeCmpb3 c) -> XCat c
XCat (forall {c :: * -> * -> *} {s :: Site}.
Category c =>
XMrphSite s c -> X (SomeMorphism c)
xsm XMrphSite s c
xm) (forall {c :: * -> * -> *} {s :: Site}.
Category c =>
XMrphSite s c -> X (SomeCmpb3 c)
xsm3 XMrphSite s c
xm) where
  xsm :: XMrphSite s c -> X (SomeMorphism c)
xsm XMrphSite s c
xm = do
    SomePath (c y y
f :. Path c x y
_) <- forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xm N
1
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (m :: * -> * -> *) x z. m x z -> SomeMorphism m
SomeMorphism c y y
f
    
  xsm3 :: XMrphSite s c -> X (SomeCmpb3 c)
xsm3 XMrphSite s c
xm = do
    SomePath (c y y
f :. c y y
g :. c y y
h :. Path c x y
_) <- forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xm N
3
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (c :: * -> * -> *) x z y z.
c x z -> c y x -> c z y -> SomeCmpb3 c
SomeCmpb3 c y y
f c y y
g c y y
h

--------------------------------------------------------------------------------
-- XFnctMrphSite -

-- | random variable for 'Functorial' 'Category's.
data XFnctMrphSite s m where
  XFnctMrphSite ::
        XMrphSite s m
    -> (forall x . Struct (ObjectClass m) x -> X x)
    -> XFnctMrphSite s m

--------------------------------------------------------------------------------
-- xMrphSite -

-- | random variable for 'Morphism's for a given 'Site'.
xMrphSite :: XFnctMrphSite s m -> XMrphSite s m
xMrphSite :: forall (s :: Site) (m :: * -> * -> *).
XFnctMrphSite s m -> XMrphSite s m
xMrphSite (XFnctMrphSite XMrphSite s m
xmd forall x. Struct (ObjectClass m) x -> X x
_) = XMrphSite s m
xmd

--------------------------------------------------------------------------------
-- xFnct -

-- | random variable for 'Functorial' 'Category's.
xFnct :: (Category c, Transformable (ObjectClass c) Ent)
  => XFnctMrphSite s c -> XFnct c
xFnct :: forall (c :: * -> * -> *) (s :: Site).
(Category c, Transformable (ObjectClass c) Ent) =>
XFnctMrphSite s c -> XFnct c
xFnct xfd :: XFnctMrphSite s c
xfd@(XFnctMrphSite XMrphSite s c
xmd forall x. Struct (ObjectClass c) x -> X x
xox) = forall (c :: * -> * -> *).
X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c
XFnct X (SomeEntity c)
xse X (SomeCmpbAppl c)
xsca where
  
  xse :: X (SomeEntity c)
xse = do
    SomeObjectClass Struct (ObjectClass c) x
so <- forall (s :: Site) (m :: * -> * -> *).
XMrphSite s m -> X (SomeObjectClass m)
xSomeObjectClass XMrphSite s c
xmd
    forall (p :: (* -> * -> *) -> *) (c :: * -> * -> *) x.
p c
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent x
-> Struct (ObjectClass c) x
-> X (SomeEntity c)
xse' XFnctMrphSite s c
xfd forall x. Struct (ObjectClass c) x -> X x
xox (forall s t x. Transformable s t => Struct s x -> Struct t x
tau Struct (ObjectClass c) x
so) Struct (ObjectClass c) x
so
  xsca :: X (SomeCmpbAppl c)
xsca = do
    SomePath (c y y
f:.c y y
g:.Path c x y
_) <- forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xmd N
2
    forall (c :: * -> * -> *) y z x.
c y z
-> c x y
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent z
-> Struct Ent x
-> Struct (ObjectClass c) x
-> X (SomeCmpbAppl c)
xsca' c y y
f c y y
g forall x. Struct (ObjectClass c) x -> X x
xox (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c y y
f)) (forall s t x. Transformable s t => Struct s x -> Struct t x
tau (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c y y
g)) (forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c y y
g)

  xse' :: p c
       -> (forall x . Struct (ObjectClass c) x -> X x)
       -> Struct Ent x
       -> Struct (ObjectClass c) x -> X (SomeEntity c)
  xse' :: forall (p :: (* -> * -> *) -> *) (c :: * -> * -> *) x.
p c
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent x
-> Struct (ObjectClass c) x
-> X (SomeEntity c)
xse' p c
_ forall x. Struct (ObjectClass c) x -> X x
xox Struct Ent x
Struct Struct (ObjectClass c) x
so = forall x. Struct (ObjectClass c) x -> X x
xox Struct (ObjectClass c) x
so 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 x (m :: * -> * -> *).
Entity x =>
Struct (ObjectClass m) x -> x -> SomeEntity m
SomeEntity Struct (ObjectClass c) x
so

  xsca' :: c y z -> c x y
        -> (forall x . Struct (ObjectClass c) x -> X x)
        -> Struct Ent z -> Struct Ent x
        -> Struct (ObjectClass c) x -> X (SomeCmpbAppl c)
  xsca' :: forall (c :: * -> * -> *) y z x.
c y z
-> c x y
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent z
-> Struct Ent x
-> Struct (ObjectClass c) x
-> X (SomeCmpbAppl c)
xsca' c y z
f c x y
g forall x. Struct (ObjectClass c) x -> X x
xox Struct Ent z
Struct Struct Ent x
Struct Struct (ObjectClass c) x
so = forall x. Struct (ObjectClass c) x -> X x
xox Struct (ObjectClass c) x
so 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 x z (c :: * -> * -> *) y.
(Entity x, Eq z) =>
c y z -> c x y -> x -> SomeCmpbAppl c
SomeCmpbAppl c y z
f c x y
g