{-# 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

    -- * Application

  , XAppl

    -- * Functorial

  , prpFunctorial, XFnct(..)
  , prpFunctorial1
  , prpFunctorial2, SomeCmpbAppl(..)
  , prpFunctorialG
  , prpFunctorialGType, SomeEntityG(..), SomeCmpb2G(..)

    -- * Cayleyan2

  , prpCayleyan2

    -- * X

    -- ** Categroy

  , xCat, XMrphSite(..), xSomePathSiteMax, xSomePathMax
  , xSomePathSite, xSomePath

    -- ** Functorial

  , xFnct, xMrphSite, XFnctMrphSite(..)

    -- * Inv2

  , relInvEq2
  
  )
  where

import Control.Monad
import Control.Exception
import Data.Kind


import OAlg.Control.Exception

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

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

import OAlg.Data.Identity
import OAlg.Data.Proxy
import OAlg.Data.EqualExtensional
import OAlg.Data.Logical
import OAlg.Data.X
import OAlg.Data.Number
import OAlg.Data.Dualisable
import OAlg.Data.Statement
import OAlg.Data.Show
import OAlg.Data.Equal

import OAlg.Entity.Definition

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

-- XMorphismException -


-- | arithmetic exceptions which are sub exceptions from 'SomeOAlgException'.

data XMorphismException
  = NoSuchEntity
  deriving (XMorphismException -> XMorphismException -> Bool
(XMorphismException -> XMorphismException -> Bool)
-> (XMorphismException -> XMorphismException -> Bool)
-> Eq XMorphismException
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: XMorphismException -> XMorphismException -> Bool
== :: XMorphismException -> XMorphismException -> Bool
$c/= :: XMorphismException -> XMorphismException -> Bool
/= :: XMorphismException -> XMorphismException -> Bool
Eq,Int -> XMorphismException -> ShowS
[XMorphismException] -> ShowS
XMorphismException -> String
(Int -> XMorphismException -> ShowS)
-> (XMorphismException -> String)
-> ([XMorphismException] -> ShowS)
-> Show XMorphismException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> XMorphismException -> ShowS
showsPrec :: Int -> XMorphismException -> ShowS
$cshow :: XMorphismException -> String
show :: XMorphismException -> String
$cshowList :: [XMorphismException] -> ShowS
showList :: [XMorphismException] -> ShowS
Show)

instance Exception XMorphismException where
  toException :: XMorphismException -> SomeException
toException   = XMorphismException -> SomeException
forall e. Exception e => e -> SomeException
oalgExceptionToException
  fromException :: SomeException -> Maybe XMorphismException
fromException = SomeException -> Maybe XMorphismException
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
:<=>: X (SomeMorphism c) -> (SomeMorphism c -> 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
(==) = c x y -> c x y -> Bool
forall x y. 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
:=c x y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
f]
                        in [Statement] -> Statement
And [ ((Struct (ObjectClass c) y -> c y y
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f) c y y -> c x y -> c x y
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f) c x y -> c x y -> Bool
forall x y. c x y -> c x y -> Bool
== c x y
f) Bool -> Message -> Statement
:?> Message
prm
                               , (c x y
f c x y -> c x y -> Bool
forall x y. c x y -> c x y -> Bool
== (c x y
f c x y -> c x x -> c x y
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) x
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f))) Bool -> Message -> Statement
:?> Message
prm
                               ]
                   )

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

-- 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 c x w -> c y x -> c y w
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
g) c y w -> c z y -> c z w
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
h) c z w -> c z w -> Bool
forall {x} {y}. c x y -> c x y -> Bool
== (c x w
f c x w -> c z x -> c z w
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. (c y x
g c y x -> c z y -> c z x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c z y
h))) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c x w -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x w
f,String
"g"String -> String -> Parameter
:=c y x -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y x
g,String
"h"String -> String -> Parameter
:=c z y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c z y
h]
  where == :: c x y -> c x y -> Bool
(==) = c x y -> c x y -> Bool
forall {x} {y}. 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 y1 y
f :. c y1 y1
g :. c y1 y1
h :. Path c x y1
pth)
  = c y1 y -> c y1 y1 -> c y1 y1 -> Statement
forall (c :: * -> * -> *) x w y z.
(Category c, Show2 c, Eq2 c) =>
c x w -> c y x -> c z y -> Statement
relCategory2 c y1 y
f c y1 y1
g c y1 y1
h Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& Path c x y1 -> Statement
forall (c :: * -> * -> *) x y.
(Category c, Show2 c, Eq2 c) =>
Path c x y -> Statement
relCategory2Path (c y1 y1
g c y1 y1 -> Path c x y1 -> Path c x y1
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. c y1 y1
h c y1 y1 -> Path c x y1 -> Path c x y1
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. Path c x y1
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
:<=>: X (SomeCmpb3 c) -> (SomeCmpb3 c -> 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) -> c x w -> c y x -> c z y -> Statement
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 [ X (SomeMorphism c) -> Statement
forall (c :: * -> * -> *).
(Category c, Show2 c, Eq2 c) =>
X (SomeMorphism c) -> Statement
prpCategory1 X (SomeMorphism c)
xm
            , X (SomeCmpb3 c) -> Statement
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
:<=>: X (SomeEntity c) -> (SomeEntity c -> 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 = Proxy c -> Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' (X (SomeEntity c) -> Proxy c
forall (c :: * -> * -> *). X (SomeEntity c) -> Proxy c
p X (SomeEntity c)
xid) Struct (ObjectClass c) x
d
                        in (c x x -> x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap c x x
od x
x x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
x) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"od"String -> String -> Parameter
:=c x x -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x x
od,String
"x"String -> String -> Parameter
:=x -> String
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)
_ = Proxy 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
:<=>: X (SomeCmpbAppl c) -> (SomeCmpbAppl c -> 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)
                    -> (c x z -> x -> z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap (c y z
f c y z -> c x y -> c x z
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
g) x
x z -> z -> Bool
forall a. Eq a => a -> a -> Bool
== (c y z -> y -> z
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap c y z
f (y -> z) -> (x -> y) -> x -> z
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
. c x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap c x y
g) x
x)
                        Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c y z -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y z
f,String
"g"String -> String -> Parameter
:=c x y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
g,String
"x"String -> String -> Parameter
:=x -> String
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 [ X (SomeEntity c) -> Statement
forall (c :: * -> * -> *).
(Functorial c, Show2 c) =>
X (SomeEntity c) -> Statement
prpFunctorial1 X (SomeEntity c)
xd
            , X (SomeCmpbAppl c) -> Statement
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
:<=>: X (SomeMorphism c) -> (SomeMorphism c -> 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
:=c x y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
f]
                           == :: c x y -> c x y -> Bool
(==) = c x y -> c x y -> Bool
forall x y. 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'   = c x y -> c y x
forall x y. c x y -> c y x
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' c y x -> c x y -> c x x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f) c x x -> c x x -> Bool
forall x y. c x y -> c x y -> Bool
== Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) x
forall x y. c x y -> Struct (ObjectClass c) x
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 c x y -> c y x -> c y y
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
f') c y y -> c y y -> Bool
forall x y. c x y -> c x y -> Bool
== Struct (ObjectClass c) y -> c y y
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c x y
f)) Bool -> Message -> Statement
:?> Message
prm
                               ]
                   )

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

-- relInvEq2 -


-- | validity according to 'Inv2'.

relInvEq2 :: (Category c, Eq2 c, Show2 c) => Inv2 c x y -> Statement
relInvEq2 :: forall (c :: * -> * -> *) x y.
(Category c, Eq2 c, Show2 c) =>
Inv2 c x y -> Statement
relInvEq2 (Inv2 c x y
f c y x
g)
  = [Statement] -> Statement
And [ String -> Label
Label String
"g . f" Label -> Statement -> Statement
:<=>: ((c y x
g c y x -> c x y -> c x x
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c x y
f) c x x -> c x x -> Bool
forall {x} {y}. c x y -> c x y -> Bool
.=. Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c x y -> Struct (ObjectClass c) x
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c x y
f)) Bool -> Message -> Statement
:?> Message
prms
        , String -> Label
Label String
"f . g" Label -> Statement -> Statement
:<=>: ((c x y
f c x y -> c y x -> c y y
forall y z x. c y z -> c x y -> c x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. c y x
g) c y y -> c y y -> Bool
forall {x} {y}. c x y -> c x y -> Bool
.=. Struct (ObjectClass c) y -> c y y
forall x. Struct (ObjectClass c) x -> c x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne (c y x -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c y x
g)) Bool -> Message -> Statement
:?> Message
prms
        ]
    where .=. :: c x y -> c x y -> Bool
(.=.) = c x y -> c x y -> Bool
forall {x} {y}. c x y -> c x y -> Bool
forall (h :: * -> * -> *) x y. Eq2 h => h x y -> h x y -> Bool
eq2
          prms :: Message
prms  = [Parameter] -> Message
Params [String
"f"String -> String -> Parameter
:=c x y -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c x y
f, String
"g"String -> String -> Parameter
:=c y x -> String
forall a b. c a b -> String
forall (h :: * -> * -> *) a b. Show2 h => h a b -> String
show2 c y x
g]

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

-- 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)
_) = X (SomeObjectClass (Op2 m))
-> (forall x.
    Struct (ObjectClass (Op2 m)) x
    -> X (SomeMorphismSite 'From (Op2 m) x))
-> XMrphSite 'From (Op2 m)
forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall x.
    Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x))
-> XMrphSite 'From m
XDomain ((SomeObjectClass m -> SomeObjectClass (Op2 m))
-> X (SomeObjectClass m) -> X (SomeObjectClass (Op2 m))
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SomeObjectClass m -> Dual (SomeObjectClass m)
SomeObjectClass m -> SomeObjectClass (Op2 m)
forall x. Dualisable x => x -> Dual x
toDual X (SomeObjectClass m)
xo) (XMrphSite 'To m
-> Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
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' = (SomeMorphismSite 'To m x -> SomeMorphismSite 'From (Op2 m) x)
-> X (SomeMorphismSite 'To m x)
-> X (SomeMorphismSite 'From (Op2 m) x)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SomeMorphismSite 'To m x -> Dual (SomeMorphismSite 'To m x)
SomeMorphismSite 'To m x -> SomeMorphismSite 'From (Op2 m) x
forall x. Dualisable x => x -> Dual x
toDual (X (SomeMorphismSite 'To m x)
 -> X (SomeMorphismSite 'From (Op2 m) x))
-> X (SomeMorphismSite 'To m x)
-> X (SomeMorphismSite 'From (Op2 m) x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct (ObjectClass m) x -> X (SomeMorphismSite 'To m x)
forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm Struct (ObjectClass m) x
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)
_) = X (SomeObjectClass m)
-> (forall y.
    Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y))
-> XMrphSite 'To m
forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall y.
    Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y))
-> XMrphSite 'To m
XRange ((SomeObjectClass (Op2 m) -> SomeObjectClass m)
-> X (SomeObjectClass (Op2 m)) -> X (SomeObjectClass m)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (SomeObjectClass m) -> SomeObjectClass m
SomeObjectClass (Op2 m) -> SomeObjectClass m
forall x. Dualisable x => Dual x -> x
fromDual X (SomeObjectClass (Op2 m))
xo') (XMrphSite 'From (Op2 m)
-> Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
forall (m :: * -> * -> *) y.
XMrphSite 'From (Op2 m)
-> Struct (ObjectClass m) y -> X (SomeMorphismSite 'To m y)
xsm Dual (XMrphSite 'To m)
XMrphSite 'From (Op2 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 = (SomeMorphismSite 'From (Op2 m) y -> SomeMorphismSite 'To m y)
-> X (SomeMorphismSite 'From (Op2 m) y)
-> X (SomeMorphismSite 'To m y)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (SomeMorphismSite 'To m y) -> SomeMorphismSite 'To m y
SomeMorphismSite 'From (Op2 m) y -> SomeMorphismSite 'To m y
forall x. Dualisable x => Dual x -> x
fromDual (X (SomeMorphismSite 'From (Op2 m) y)
 -> X (SomeMorphismSite 'To m y))
-> X (SomeMorphismSite 'From (Op2 m) y)
-> X (SomeMorphismSite 'To m y)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct (ObjectClass (Op2 m)) y
-> X (SomeMorphismSite 'From (Op2 m) y)
forall x.
Struct (ObjectClass (Op2 m)) x
-> X (SomeMorphismSite 'From (Op2 m) x)
xsm' Struct (ObjectClass m) y
Struct (ObjectClass (Op2 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 = XMrphSite 'From m
-> N
-> Struct (ObjectClass m) x
-> Struct (ObjectClass m) x
-> Path m x x
-> X (SomePathSite 'From m x)
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
XMrphSite 'From m
xmf N
n Struct (ObjectClass m) x
d Struct (ObjectClass m) x
d (Struct (ObjectClass (Path m)) x -> Path m x x
forall x. Struct (ObjectClass (Path m)) x -> Path m x x
forall (c :: * -> * -> *) x.
Category c =>
Struct (ObjectClass c) x -> c x x
cOne Struct (ObjectClass m) x
Struct (ObjectClass (Path 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                      = SomePathSite 'From m x -> X (SomePathSite 'From m x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomePathSite 'From m x -> X (SomePathSite 'From m x))
-> SomePathSite 'From m x -> X (SomePathSite 'From m x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Path m x y -> SomePathSite 'From m x
forall (m :: * -> * -> *) x y. Path m x y -> 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 Struct (ObjectClass m) y -> X (SomeMorphismSite 'From m y)
forall x.
Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)
xmf Struct (ObjectClass m) y
r of
    X (SomeMorphismSite 'From m y)
XEmpty -> SomePathSite 'From m x -> X (SomePathSite 'From m x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomePathSite 'From m x -> X (SomePathSite 'From m x))
-> SomePathSite 'From m x -> X (SomePathSite 'From m x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Path m x y -> SomePathSite 'From m x
forall (m :: * -> * -> *) x y. Path m x y -> SomePathSite 'From m x
SomePathDomain Path m x y
fs
    X (SomeMorphismSite 'From m y)
xf     -> X (SomeMorphismSite 'From m y)
xf X (SomeMorphismSite 'From m y)
-> (SomeMorphismSite 'From m y -> X (SomePathSite 'From m x))
-> X (SomePathSite 'From m x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(SomeMorphismDomain m y y
f) -> XMrphSite 'From m
-> N
-> Struct (ObjectClass m) x
-> Struct (ObjectClass m) y
-> Path m x y
-> X (SomePathSite 'From m x)
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 (N -> N
forall a. Enum a => a -> a
pred N
n) Struct (ObjectClass m) x
d (m y y -> Struct (ObjectClass m) y
forall x y. m x y -> Struct (ObjectClass m) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range m y y
f) (m y y
f m y y -> Path m x y -> Path m x y
forall (m :: * -> * -> *) y1 y x.
m y1 y -> Path m x y1 -> Path m x y
:. 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
  = (SomePathSite 'From (Op2 m) x -> SomePathSite 'To m x)
-> X (SomePathSite 'From (Op2 m) x) -> X (SomePathSite 'To m x)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (SomePathSite 'To m x) -> SomePathSite 'To m x
SomePathSite 'From (Op2 m) x -> SomePathSite 'To m x
forall x. Dualisable x => Dual x -> x
fromDual (X (SomePathSite 'From (Op2 m) x) -> X (SomePathSite s m x))
-> X (SomePathSite 'From (Op2 m) x) -> X (SomePathSite s m x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XMrphSite 'From (Op2 m)
-> N
-> Struct (ObjectClass (Op2 m)) x
-> X (SomePathSite 'From (Op2 m) x)
forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax (XMrphSite s m -> Dual (XMrphSite s m)
forall x. Dualisable x => x -> Dual x
toDual XMrphSite s m
xmt) N
n Struct (ObjectClass m) x
Struct (ObjectClass (Op2 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 <- XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
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
  SomePath m -> X (SomePath m)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomePath m -> X (SomePath m)) -> SomePath m -> X (SomePath m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SomePathSite s m x -> SomePath m
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 = (SomePath (Op2 m) -> SomePath m)
-> X (SomePath (Op2 m)) -> X (SomePath m)
forall a b. (a -> b) -> X a -> X b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dual (SomePath m) -> SomePath m
SomePath (Op2 m) -> SomePath m
forall x. Dualisable x => Dual x -> x
fromDual (X (SomePath (Op2 m)) -> X (SomePath m))
-> X (SomePath (Op2 m)) -> X (SomePath m)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XMrphSite 'From (Op2 m) -> N -> X (SomePath (Op2 m))
forall (m :: * -> * -> *) (s :: Site).
Morphism m =>
XMrphSite s m -> N -> X (SomePath m)
xSomePathMax (XMrphSite s m -> Dual (XMrphSite s m)
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)
_) = X (SomeObjectClass c)
-> (forall x.
    Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x))
-> XMrphSite 'From c
forall (m :: * -> * -> *).
X (SomeObjectClass m)
-> (forall x.
    Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x))
-> XMrphSite 'From m
XDomain X (SomeObjectClass c)
xo (XMrphSite 'From c
-> Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
forall (c :: * -> * -> *) x.
Category c =>
XMrphSite 'From c
-> Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm' XMrphSite s c
XMrphSite 'From 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 Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
forall x.
Struct (ObjectClass c) x -> X (SomeMorphismSite 'From c x)
xsm Struct (ObjectClass c) x
o of
    X (SomeMorphismSite 'From c x)
XEmpty -> SomeMorphismSite 'From c x -> X (SomeMorphismSite 'From c x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeMorphismSite 'From c x -> X (SomeMorphismSite 'From c x))
-> SomeMorphismSite 'From c x -> X (SomeMorphismSite 'From c x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c x x -> SomeMorphismSite 'From c x
forall (m :: * -> * -> *) x y. m x y -> SomeMorphismSite 'From m x
SomeMorphismDomain (c x x -> SomeMorphismSite 'From c x)
-> c x x -> SomeMorphismSite 'From c x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct (ObjectClass c) x -> c x x
forall x. Struct (ObjectClass c) x -> c x x
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)
_) = Dual (XMrphSite 'To c) -> XMrphSite 'To c
XMrphSite 'From (Op2 c) -> XMrphSite s c
forall x. Dualisable x => Dual x -> x
fromDual (XMrphSite 'From (Op2 c) -> XMrphSite s c)
-> XMrphSite 'From (Op2 c) -> XMrphSite s c
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XMrphSite 'From (Op2 c) -> XMrphSite 'From (Op2 c)
forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> XMrphSite s c
adjOne (XMrphSite 'From (Op2 c) -> XMrphSite 'From (Op2 c))
-> XMrphSite 'From (Op2 c) -> XMrphSite 'From (Op2 c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ XMrphSite s c -> Dual (XMrphSite s c)
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 = XMrphSite s c
-> N -> Struct (ObjectClass c) x -> X (SomePathSite s c x)
forall (m :: * -> * -> *) (s :: Site) x.
Morphism m =>
XMrphSite s m
-> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathSiteMax (XMrphSite s c -> XMrphSite s c
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 = XMrphSite s c -> N -> X (SomePath c)
forall (m :: * -> * -> *) (s :: Site).
Morphism m =>
XMrphSite s m -> N -> X (SomePath m)
xSomePathMax (XMrphSite s c -> XMrphSite s c
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 = X (SomeMorphism c) -> X (SomeCmpb3 c) -> XCat c
forall (c :: * -> * -> *).
X (SomeMorphism c) -> X (SomeCmpb3 c) -> XCat c
XCat (XMrphSite s c -> X (SomeMorphism c)
forall {c :: * -> * -> *} {s :: Site}.
Category c =>
XMrphSite s c -> X (SomeMorphism c)
xsm XMrphSite s c
xm) (XMrphSite s c -> X (SomeCmpb3 c)
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 y1 y
f :. Path c x y1
_) <- XMrphSite s c -> N -> X (SomePath c)
forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xm N
1
    SomeMorphism c -> X (SomeMorphism c)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeMorphism c -> X (SomeMorphism c))
-> SomeMorphism c -> X (SomeMorphism c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c y1 y -> SomeMorphism c
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism c y1 y
f
    
  xsm3 :: XMrphSite s c -> X (SomeCmpb3 c)
xsm3 XMrphSite s c
xm = do
    SomePath (c y1 y
f :. c y1 y1
g :. c y1 y1
h :. Path c x y1
_) <- XMrphSite s c -> N -> X (SomePath c)
forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xm N
3
    SomeCmpb3 c -> X (SomeCmpb3 c)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeCmpb3 c -> X (SomeCmpb3 c)) -> SomeCmpb3 c -> X (SomeCmpb3 c)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ c y1 y -> c y1 y1 -> c y1 y1 -> SomeCmpb3 c
forall (c :: * -> * -> *) x w y z.
c x w -> c y x -> c z y -> SomeCmpb3 c
SomeCmpb3 c y1 y
f c y1 y1
g c y1 y1
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) = X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c
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 <- XMrphSite s c -> X (SomeObjectClass c)
forall (s :: Site) (m :: * -> * -> *).
XMrphSite s m -> X (SomeObjectClass m)
xSomeObjectClass XMrphSite s c
xmd
    XFnctMrphSite s c
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent x
-> Struct (ObjectClass c) x
-> X (SomeEntity c)
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 Struct (ObjectClass c) x -> X x
forall x. Struct (ObjectClass c) x -> X x
xox (Struct (ObjectClass c) x -> Struct Ent x
forall x. Struct (ObjectClass c) x -> Struct Ent x
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 y1 y
f:.c y1 y1
g:.Path c x y1
_) <- XMrphSite s c -> N -> X (SomePath c)
forall (c :: * -> * -> *) (s :: Site).
Category c =>
XMrphSite s c -> N -> X (SomePath c)
xSomePath XMrphSite s c
xmd N
2
    c y1 y
-> c y1 y1
-> (forall x. Struct (ObjectClass c) x -> X x)
-> Struct Ent y
-> Struct Ent y1
-> Struct (ObjectClass c) y1
-> X (SomeCmpbAppl c)
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 y1 y
f c y1 y1
g Struct (ObjectClass c) x -> X x
forall x. Struct (ObjectClass c) x -> X x
xox (Struct (ObjectClass c) y -> Struct Ent y
forall x. Struct (ObjectClass c) x -> Struct Ent x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (c y1 y -> Struct (ObjectClass c) y
forall x y. c x y -> Struct (ObjectClass c) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range c y1 y
f)) (Struct (ObjectClass c) y1 -> Struct Ent y1
forall x. Struct (ObjectClass c) x -> Struct Ent x
forall s t x. Transformable s t => Struct s x -> Struct t x
tau (c y1 y1 -> Struct (ObjectClass c) y1
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c y1 y1
g)) (c y1 y1 -> Struct (ObjectClass c) y1
forall x y. c x y -> Struct (ObjectClass c) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain c y1 y1
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 = Struct (ObjectClass c) x -> X x
forall x. Struct (ObjectClass c) x -> X x
xox Struct (ObjectClass c) x
so X x -> (x -> X (SomeEntity c)) -> X (SomeEntity c)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeEntity c -> X (SomeEntity c)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeEntity c -> X (SomeEntity c))
-> (x -> SomeEntity c) -> x -> X (SomeEntity c)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. Struct (ObjectClass c) x -> x -> SomeEntity c
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 = Struct (ObjectClass c) x -> X x
forall x. Struct (ObjectClass c) x -> X x
xox Struct (ObjectClass c) x
so X x -> (x -> X (SomeCmpbAppl c)) -> X (SomeCmpbAppl c)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeCmpbAppl c -> X (SomeCmpbAppl c)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeCmpbAppl c -> X (SomeCmpbAppl c))
-> (x -> SomeCmpbAppl c) -> x -> X (SomeCmpbAppl c)
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
. c y z -> c x y -> x -> SomeCmpbAppl c
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 

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

-- relFunctorialGOne -


relFunctorialGOne :: (FunctorialG t a b, EqExt b) => q t a b -> Struct (ObjectClass a) x -> Statement
relFunctorialGOne :: forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) x.
(FunctorialG t a b, EqExt b) =>
q t a b -> Struct (ObjectClass a) x -> Statement
relFunctorialGOne q t a b
q Struct (ObjectClass a) x
s = a x x -> b (t x) (t x)
forall x y. a x y -> b (t x) (t y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (Proxy a -> Struct (ObjectClass a) x -> a x x
forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' (q t a b -> Proxy a
forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy a
qa q t a b
q) Struct (ObjectClass a) x
s) b (t x) (t x) -> b (t x) (t x) -> Statement
forall x y. b x y -> b x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. Proxy b -> Struct (ObjectClass b) (t x) -> b (t x) (t x)
forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' (q t a b -> Proxy b
forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy b
qb q t a b
q) (Proxy t -> Struct (ObjectClass a) x -> Struct (ObjectClass b) (t x)
forall (t :: * -> *) u v (q :: (* -> *) -> *) x.
TransformableG t u v =>
q t -> Struct u x -> Struct v (t x)
tauG' (q t a b -> Proxy t
forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy t
qt q t a b
q) Struct (ObjectClass a) x
s) where

  qa :: forall q (t :: Type -> Type) (a :: Type -> Type -> Type) (b :: Type -> Type -> Type)
      . q t a b -> Proxy a
  qa :: forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy a
qa q t a b
_ = Proxy a
forall {k} (t :: k). Proxy t
Proxy

  qb :: forall q (t :: Type -> Type) (a :: Type -> Type -> Type) (b :: Type -> Type -> Type)
      . q t a b -> Proxy b
  qb :: forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy b
qb q t a b
_ = Proxy b
forall {k} (t :: k). Proxy t
Proxy

  qt :: forall q (t :: Type -> Type) (a :: Type -> Type -> Type) (b :: Type -> Type -> Type)
      . q t a b -> Proxy t
  qt :: forall (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
       (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *).
q t a b -> Proxy t
qt q t a b
_ = Proxy t
forall {k} (t :: k). Proxy t
Proxy

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

-- relFunctorialGCmp -


relFunctorialGCmp :: (FunctorialG t a b, EqExt b) => q t a b -> a y z -> a x y -> Statement
relFunctorialGCmp :: forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) y z x.
(FunctorialG t a b, EqExt b) =>
q t a b -> a y z -> a x y -> Statement
relFunctorialGCmp q t a b
q a y z
f a x y
g = q t a b -> a x z -> b (t x) (t z)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) x y.
ApplicativeG t a b =>
q t a b -> a x y -> b (t x) (t y)
amapG' q t a b
q (a y z
f a y z -> a x y -> a x z
forall y z x. a y z -> a x y -> a x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. a x y
g) b (t x) (t z) -> b (t x) (t z) -> Statement
forall x y. b x y -> b x y -> Statement
forall (c :: * -> * -> *) x y.
EqExt c =>
c x y -> c x y -> Statement
.=. (q t a b -> a y z -> b (t y) (t z)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) x y.
ApplicativeG t a b =>
q t a b -> a x y -> b (t x) (t y)
amapG' q t a b
q a y z
f b (t y) (t z) -> b (t x) (t y) -> b (t x) (t z)
forall y z x. b y z -> b x y -> b x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. q t a b -> a x y -> b (t x) (t y)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) x y.
ApplicativeG t a b =>
q t a b -> a x y -> b (t x) (t y)
amapG' q t a b
q a x y
g)

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

-- prpFunctorialG -


-- | validity according to 'FunctorialG'.

prpFunctorialG :: (FunctorialG t a b, EqExt b)
  => q t a b -> X (SomeObjectClass a) -> X (SomeCmpb2 a) -> Statement
prpFunctorialG :: forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *).
(FunctorialG t a b, EqExt b) =>
q t a b -> X (SomeObjectClass a) -> X (SomeCmpb2 a) -> Statement
prpFunctorialG q t a b
q X (SomeObjectClass a)
xo X (SomeCmpb2 a)
xfg = String -> Label
Prp String
"FunctorialG" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"cOne" Label -> Statement -> Statement
:<=>: X (SomeObjectClass a)
-> (SomeObjectClass a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeObjectClass a)
xo (\(SomeObjectClass Struct (ObjectClass a) x
s) -> q t a b -> Struct (ObjectClass a) x -> Statement
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) x.
(FunctorialG t a b, EqExt b) =>
q t a b -> Struct (ObjectClass a) x -> Statement
relFunctorialGOne q t a b
q Struct (ObjectClass a) x
s)
      , String -> Label
Label String
"." Label -> Statement -> Statement
:<=>: X (SomeCmpb2 a) -> (SomeCmpb2 a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeCmpb2 a)
xfg (\(SomeCmpb2 a y z
f a x y
g) -> q t a b -> a y z -> a x y -> Statement
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *)
       (q :: (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) y z x.
(FunctorialG t a b, EqExt b) =>
q t a b -> a y z -> a x y -> Statement
relFunctorialGCmp q t a b
q a y z
f a x y
g)
      ] 

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

-- relFunctorialGOneType -


relFunctorialGOneType ::
  ( FunctorialG t a (->)
  , Entity (t x)
  )
  => q a -> Struct (ObjectClass a) x -> t x -> Statement
relFunctorialGOneType :: forall (t :: * -> *) (a :: * -> * -> *) x
       (q :: (* -> * -> *) -> *).
(FunctorialG t a (->), Entity (t x)) =>
q a -> Struct (ObjectClass a) x -> t x -> Statement
relFunctorialGOneType q a
q Struct (ObjectClass a) x
s t x
tx = (a x x -> t x -> t x
forall x y. a x y -> t x -> t y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (q a -> Struct (ObjectClass a) x -> a x x
forall (c :: * -> * -> *) (p :: (* -> * -> *) -> *) x.
Category c =>
p c -> Struct (ObjectClass c) x -> c x x
cOne' q a
q Struct (ObjectClass a) x
s) t x
tx t x -> t x -> Bool
forall a. Eq a => a -> a -> Bool
== t x
tx) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"tx"String -> String -> Parameter
:=t x -> String
forall a. Show a => a -> String
show t x
tx]

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

-- relFunctorialGCmpType -


relFunctorialGCmpType ::
  ( FunctorialG t a (->)
  , Entity (t x)
  , Entity (t z)
  )
  => a y z -> a x y -> t x -> Statement
relFunctorialGCmpType :: forall (t :: * -> *) (a :: * -> * -> *) x z y.
(FunctorialG t a (->), Entity (t x), Entity (t z)) =>
a y z -> a x y -> t x -> Statement
relFunctorialGCmpType a y z
f a x y
g t x
tx = (a x z -> t x -> t z
forall x y. a x y -> t x -> t y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG (a y z
f a y z -> a x y -> a x z
forall y z x. a y z -> a x y -> a x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. a x y
g) t x
tx t z -> t z -> Bool
forall a. Eq a => a -> a -> Bool
== a y z -> t y -> t z
forall x y. a x y -> t x -> t y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG a y z
f (a x y -> t x -> t y
forall x y. a x y -> t x -> t y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG a x y
g t x
tx)) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"tx"String -> String -> Parameter
:=t x -> String
forall a. Show a => a -> String
show t x
tx]

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

-- SomeEntityG -


-- | some object class for @__c__@ with a applicable @__t__@-entity.

data SomeEntityG t c where
  SomeEntityG :: Entity (t x) => Struct (ObjectClass c) x -> t x -> SomeEntityG t c

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

-- SomeCmpb2G -


-- | some combosables for @__c__@ with a applicable @__t__@-entity.

data SomeCmpb2G t c where
  SomeCmpb2G :: (Entity (t x), Entity (t z)) => c y z -> c x y -> t x -> SomeCmpb2G t c
  
--------------------------------------------------------------------------------

-- prpFunctorialGType -


-- | validity acording to represatnable 'FunctorialG's.

prpFunctorialGType :: FunctorialG t a (->)
  => X (SomeEntityG t a) -> X (SomeCmpb2G t a) -> Statement
prpFunctorialGType :: forall (t :: * -> *) (a :: * -> * -> *).
FunctorialG t a (->) =>
X (SomeEntityG t a) -> X (SomeCmpb2G t a) -> Statement
prpFunctorialGType X (SomeEntityG t a)
xse X (SomeCmpb2G t a)
xcpb2 = String -> Label
Prp String
"FunctorialGType" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ String -> Label
Label String
"cOne" Label -> Statement -> Statement
:<=>: X (SomeEntityG t a) -> (SomeEntityG t a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeEntityG t a)
xse (\(SomeEntityG Struct (ObjectClass a) x
s t x
tx) -> Proxy a -> Struct (ObjectClass a) x -> t x -> Statement
forall (t :: * -> *) (a :: * -> * -> *) x
       (q :: (* -> * -> *) -> *).
(FunctorialG t a (->), Entity (t x)) =>
q a -> Struct (ObjectClass a) x -> t x -> Statement
relFunctorialGOneType (X (SomeEntityG t a) -> Proxy a
forall (t :: * -> *) (a :: * -> * -> *).
X (SomeEntityG t a) -> Proxy a
qa X (SomeEntityG t a)
xse) Struct (ObjectClass a) x
s t x
tx)
      , String -> Label
Label String
"." Label -> Statement -> Statement
:<=>: X (SomeCmpb2G t a) -> (SomeCmpb2G t a -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeCmpb2G t a)
xcpb2 (\(SomeCmpb2G a y z
f a x y
g t x
tx) -> a y z -> a x y -> t x -> Statement
forall (t :: * -> *) (a :: * -> * -> *) x z y.
(FunctorialG t a (->), Entity (t x), Entity (t z)) =>
a y z -> a x y -> t x -> Statement
relFunctorialGCmpType a y z
f a x y
g t x
tx)
      ]
  where
    qa :: X (SomeEntityG t a) -> Proxy a
    qa :: forall (t :: * -> *) (a :: * -> * -> *).
X (SomeEntityG t a) -> Proxy a
qa X (SomeEntityG t a)
_ = Proxy a
forall {k} (t :: k). Proxy t
Proxy