{-# LANGUAGE NoImplicitPrelude #-}

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

-- |
-- Module      : OAlg.Entity.Matrix.Proposition
-- Description : propositions on matrices
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
--
-- propositions on matrices.
module OAlg.Entity.Matrix.Proposition
  (
    -- * Proposition
    prpMatrix, prpMatrixZ
  , prpHomCoMatrixOp
    
  ) where

import Control.Monad

import OAlg.Prelude

import OAlg.Category.Unify

import OAlg.Data.Variant
import OAlg.Data.HomCo

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Vectorial
import OAlg.Structure.Distributive
import OAlg.Structure.Algebraic

import OAlg.Limes.ProductsAndSums

import OAlg.Entity.Natural

import OAlg.Entity.Matrix.Definition
import OAlg.Entity.Matrix.ProductsAndSums

import OAlg.Hom.Oriented.Proposition
import OAlg.Hom.Fibred
import OAlg.Hom.FibredOriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Additive

--------------------------------------------------------------------------------
-- prpMatrix -

-- | validity of the algebraic structure of matrices.
prpMatrix :: Distributive x
  => XOrtOrientation (Matrix x)
  -> XOrtSite From (Matrix x)
  -> XOrtSite To (Matrix x)
  -> Statement
prpMatrix :: forall x.
Distributive x =>
XOrtOrientation (Matrix x)
-> XOrtSite 'From (Matrix x)
-> XOrtSite 'To (Matrix x)
-> Statement
prpMatrix XOrtOrientation (Matrix x)
xo XOrtSite 'From (Matrix x)
xf XOrtSite 'To (Matrix x)
xt = String -> Label
Prp String
"Matrix" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt (Matrix x) -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrtOrientation (Matrix x) -> XOrt (Matrix x)
forall q. XOrtOrientation q -> XOrt q
xoOrt XOrtOrientation (Matrix x)
xo)
      , XMlt (Matrix x) -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (X N -> XOrtOrientation (Matrix x) -> XMlt (Matrix x)
forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt (N -> N -> X N
xNB N
0 N
10) XOrtOrientation (Matrix x)
xo)
      , XOrt (Matrix x) -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrtOrientation (Matrix x) -> XOrt (Matrix x)
forall q. XOrtOrientation q -> XOrt q
xoFbr XOrtOrientation (Matrix x)
xo)
      , XOrt (Matrix x) -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrtOrientation (Matrix x) -> XOrt (Matrix x)
forall q. XOrtOrientation q -> XOrt q
xoFbrOrt XOrtOrientation (Matrix x)
xo)
      , XAdd (Matrix x) -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (X N -> XOrtOrientation (Matrix x) -> XAdd (Matrix x)
forall a. FibredOriented a => X N -> XOrtOrientation a -> XAdd a
xoAdd (N -> N -> X N
xNB N
0 N
5) XOrtOrientation (Matrix x)
xo)
      , XDst (Matrix x) -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XOrtOrientation (Matrix x)
-> XOrtSite 'From (Matrix x)
-> XOrtSite 'To (Matrix x)
-> XDst (Matrix x)
forall d.
Distributive d =>
XOrtOrientation d -> XOrtSite 'From d -> XOrtSite 'To d -> XDst d
xoDst XOrtOrientation (Matrix x)
xo XOrtSite 'From (Matrix x)
xf XOrtSite 'To (Matrix x)
xt)
      ]


dstMatrix :: Int -> X (Matrix x) -> IO ()
dstMatrix :: forall x. Int -> X (Matrix x) -> IO ()
dstMatrix = (Matrix x -> [String]) -> Int -> X (Matrix x) -> IO ()
forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr (\Matrix x
m -> [Matrix x -> String
forall {x}. Matrix x -> String
rws Matrix x
m,Matrix x -> String
forall {x}. Matrix x -> String
cls Matrix x
m]) where
  rws :: Matrix x -> String
rws (Matrix Dim x (Point x)
r Dim x (Point x)
_ Entries N N x
_) = N -> String
forall a. Show a => a -> String
show (N -> String) -> N -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
r
  cls :: Matrix x -> String
cls (Matrix Dim x (Point x)
_ Dim x (Point x)
c Entries N N x
_) = N -> String
forall a. Show a => a -> String
show (N -> String) -> N -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Dim x (Point x) -> N
forall x. LengthN x => x -> N
lengthN Dim x (Point x)
c


--------------------------------------------------------------------------------
-- prpMatrixZ -

-- | validity of the algebraic structure of block matrices of 'Z'.
prpMatrixZ :: Statement
prpMatrixZ :: Statement
prpMatrixZ = String -> Label
Prp String
"MatrixZ"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ XOrtOrientation (Matrix (Matrix Z))
-> XOrtSite 'From (Matrix (Matrix Z))
-> XOrtSite 'To (Matrix (Matrix Z))
-> Statement
forall x.
Distributive x =>
XOrtOrientation (Matrix x)
-> XOrtSite 'From (Matrix x)
-> XOrtSite 'To (Matrix x)
-> Statement
prpMatrix XOrtOrientation (Matrix (Matrix Z))
xo XOrtSite 'From (Matrix (Matrix Z))
xf XOrtSite 'To (Matrix (Matrix Z))
xt
            , XAbl (Matrix (Matrix Z)) -> Statement
forall a. Abelian a => XAbl a -> Statement
prpAbl (X Z
-> XOrtOrientation (Matrix (Matrix Z)) -> XAbl (Matrix (Matrix Z))
forall a. FibredOriented a => X Z -> XOrtOrientation a -> XAbl a
xoAbl (Z -> Z -> X Z
xZB (-Z
10) Z
10) XOrtOrientation (Matrix (Matrix Z))
xo)            
            , XVec (Matrix (Matrix Z)) -> Statement
forall v. Vectorial v => XVec v -> Statement
prpVec (X (Scalar (Matrix (Matrix Z)))
-> XOrtOrientation (Matrix (Matrix Z)) -> XVec (Matrix (Matrix Z))
forall v.
FibredOriented v =>
X (Scalar v) -> XOrtOrientation v -> XVec v
xoVec X Z
X (Scalar (Matrix (Matrix Z)))
xZ XOrtOrientation (Matrix (Matrix Z))
xo)
            , XAlg (Matrix (Matrix Z)) -> Statement
forall a. Algebraic a => XAlg a -> Statement
prpAlg (X (Scalar (Matrix (Matrix Z)))
-> XOrtSite 'From (Matrix (Matrix Z)) -> XAlg (Matrix (Matrix Z))
forall a (d :: Site).
Algebraic a =>
X (Scalar a) -> XOrtSite d a -> XAlg a
xoAlg X Z
X (Scalar (Matrix (Matrix Z)))
xZ XOrtSite 'From (Matrix (Matrix Z))
xf)
            , String -> Label
Label String
"Sums N3 (Matrix Z)" 
                 Label -> Statement -> Statement
:<=>: Sums N3 (Matrix Z) -> Statement
forall a. Validable a => a -> Statement
valid (Sums N3 (Matrix Z)
forall x (n :: N'). Distributive x => Sums n (Matrix x)
mtxSums :: Sums N3 (Matrix Z))
            ]
  where xo :: XOrtOrientation (Matrix (Matrix Z))
xo = XOrtOrientation (Matrix (Matrix Z))
xodZZ
        xf :: XOrtSite 'From (Matrix (Matrix Z))
xf = XOrtOrientation (Matrix (Matrix Z))
-> XOrtSite 'From (Matrix (Matrix Z))
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom XOrtOrientation (Matrix (Matrix Z))
xo
        xt :: XOrtSite 'To (Matrix (Matrix Z))
xt = XOrtOrientation (Matrix (Matrix Z))
-> XOrtSite 'To (Matrix (Matrix Z))
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'To q
xoTo XOrtOrientation (Matrix (Matrix Z))
xo

--------------------------------------------------------------------------------
-- prpHomCoMatrixFunctorial -

prpHomCoMatrixOpFunctorial ::
  ( FunctorialG t (HomCo m s o) (->)
  , m ~ Matrix, o ~ Op, s ~ DstX
  )
  => X (SomeEntityG t (HomCo m s o)) -> X (SomeCmpb2G t (HomCo m s o)) -> Statement
prpHomCoMatrixOpFunctorial :: forall (t :: * -> *) (m :: * -> *) s (o :: * -> *).
(FunctorialG t (HomCo m s o) (->), m ~ Matrix, o ~ Op, s ~ DstX) =>
X (SomeEntityG t (HomCo m s o))
-> X (SomeCmpb2G t (HomCo m s o)) -> Statement
prpHomCoMatrixOpFunctorial = X (SomeEntityG t (HomCo m s o))
-> X (SomeCmpb2G t (HomCo m s o)) -> Statement
forall (t :: * -> *) (a :: * -> * -> *).
FunctorialG t a (->) =>
X (SomeEntityG t a) -> X (SomeCmpb2G t a) -> Statement
prpFunctorialGType

xsoId :: XOrtOrientation x -> X (Id x)
xsoId :: forall x. XOrtOrientation x -> X (Id x)
xsoId XOrtOrientation x
xo = (x -> Id x) -> X x -> X (Id x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Id x
forall x. x -> Id x
Id (XOrtOrientation x -> X (Orientation (Point x))
forall q. XOrtOrientation q -> X (Orientation (Point q))
xoOrientation XOrtOrientation x
xo X (Orientation (Point x)) -> (Orientation (Point x) -> X x) -> X x
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= XOrtOrientation x -> Orientation (Point x) -> X x
forall q. XOrtOrientation q -> Orientation (Point q) -> X q
xoArrow XOrtOrientation x
xo)

xsoPnt :: Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt :: forall x. Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt = (Point x -> Pnt x) -> X (Point x) -> X (Pnt x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Point x -> Pnt x
forall x. Point x -> Pnt x
Pnt (X (Point x) -> X (Pnt x))
-> (XOrtOrientation x -> X (Point x))
-> XOrtOrientation x
-> X (Pnt x)
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. XOrtOrientation x -> X (Point x)
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint

xsoRt :: Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt :: forall x. Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt (XOrtOrientation X (Orientation (Point x))
xo Orientation (Point x) -> X x
_) = (Orientation (Point x) -> Rt x)
-> X (Orientation (Point x)) -> X (Rt x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Orientation (Point x) -> Rt x
Root x -> Rt x
forall x. Root x -> Rt x
Rt X (Orientation (Point x))
xo

xse :: Entity (t x)
  => (XOrtOrientation x -> X (t x)) -> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse :: forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation x -> X (t x)
xot s :: Struct DstX x
s@Struct DstX x
Struct = XOrtOrientation x -> X (t x)
xot XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation X (t x)
-> (t x -> X (SomeEntityG t (HomCo Matrix DstX Op)))
-> X (SomeEntityG t (HomCo Matrix DstX Op))
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeEntityG t (HomCo Matrix DstX Op)
-> X (SomeEntityG t (HomCo Matrix DstX Op))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeEntityG t (HomCo Matrix DstX Op)
 -> X (SomeEntityG t (HomCo Matrix DstX Op)))
-> (t x -> SomeEntityG t (HomCo Matrix DstX Op))
-> t x
-> X (SomeEntityG t (HomCo Matrix DstX Op))
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 (HomCo Matrix DstX Op)) x
-> t x -> SomeEntityG t (HomCo Matrix DstX Op)
forall (t :: * -> *) x (c :: * -> * -> *).
Entity (t x) =>
Struct (ObjectClass c) x -> t x -> SomeEntityG t c
SomeEntityG Struct (ObjectClass (HomCo Matrix DstX Op)) x
Struct DstX x
s

xseId :: X (SomeEntityG Id (HomCo Matrix DstX Op))
xseId :: X (SomeEntityG Id (HomCo Matrix DstX Op))
xseId
  = [X (SomeEntityG Id (HomCo Matrix DstX Op))]
-> X (SomeEntityG Id (HomCo Matrix DstX Op))
forall a. [X a] -> X a
xOneOfX [ (XOrtOrientation (Matrix Z) -> X (Id (Matrix Z)))
-> Struct DstX (Matrix Z)
-> X (SomeEntityG Id (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix Z) -> X (Id (Matrix Z))
forall x. XOrtOrientation x -> X (Id x)
xsoId (Struct DstX (Matrix Z)
forall s x. Structure s x => Struct s x
Struct :: Struct DstX (Matrix Z))
            , (XOrtOrientation (Matrix (Matrix Z)) -> X (Id (Matrix (Matrix Z))))
-> Struct DstX (Matrix (Matrix Z))
-> X (SomeEntityG Id (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix (Matrix Z)) -> X (Id (Matrix (Matrix Z)))
forall x. XOrtOrientation x -> X (Id x)
xsoId (Struct DstX (Matrix (Matrix Z))
forall s x. Structure s x => Struct s x
Struct :: Struct DstX ((Matrix (Matrix Z))))
            , (XOrtOrientation Z -> X (Id Z))
-> Struct DstX Z -> X (SomeEntityG Id (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation Z -> X (Id Z)
forall x. XOrtOrientation x -> X (Id x)
xsoId (Struct DstX Z
forall s x. Structure s x => Struct s x
Struct :: Struct DstX Z)
            ]

xsePnt :: X (SomeEntityG Pnt (HomCo Matrix DstX Op))
xsePnt :: X (SomeEntityG Pnt (HomCo Matrix DstX Op))
xsePnt
  = [X (SomeEntityG Pnt (HomCo Matrix DstX Op))]
-> X (SomeEntityG Pnt (HomCo Matrix DstX Op))
forall a. [X a] -> X a
xOneOfX [ (XOrtOrientation (Matrix Z) -> X (Pnt (Matrix Z)))
-> Struct DstX (Matrix Z)
-> X (SomeEntityG Pnt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix Z) -> X (Pnt (Matrix Z))
forall x. Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt (Struct DstX (Matrix Z)
forall s x. Structure s x => Struct s x
Struct :: Struct DstX (Matrix Z))
            , (XOrtOrientation (Matrix (Matrix Z))
 -> X (Pnt (Matrix (Matrix Z))))
-> Struct DstX (Matrix (Matrix Z))
-> X (SomeEntityG Pnt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix (Matrix Z)) -> X (Pnt (Matrix (Matrix Z)))
forall x. Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt (Struct DstX (Matrix (Matrix Z))
forall s x. Structure s x => Struct s x
Struct :: Struct DstX (Matrix (Matrix Z)))
            , (XOrtOrientation Z -> X (Pnt Z))
-> Struct DstX Z -> X (SomeEntityG Pnt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation Z -> X (Pnt Z)
forall x. Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt (Struct DstX Z
forall s x. Structure s x => Struct s x
Struct :: Struct DstX Z)
            ]

xseRt :: X (SomeEntityG Rt (HomCo Matrix DstX Op))
xseRt :: X (SomeEntityG Rt (HomCo Matrix DstX Op))
xseRt
  = [X (SomeEntityG Rt (HomCo Matrix DstX Op))]
-> X (SomeEntityG Rt (HomCo Matrix DstX Op))
forall a. [X a] -> X a
xOneOfX [ (XOrtOrientation (Matrix Z) -> X (Rt (Matrix Z)))
-> Struct DstX (Matrix Z)
-> X (SomeEntityG Rt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix Z) -> X (Rt (Matrix Z))
forall x. Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt (Struct DstX (Matrix Z)
forall s x. Structure s x => Struct s x
Struct :: Struct DstX (Matrix Z))
            , (XOrtOrientation (Matrix (Matrix Z)) -> X (Rt (Matrix (Matrix Z))))
-> Struct DstX (Matrix (Matrix Z))
-> X (SomeEntityG Rt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation (Matrix (Matrix Z)) -> X (Rt (Matrix (Matrix Z)))
forall x. Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt (Struct DstX (Matrix (Matrix Z))
forall s x. Structure s x => Struct s x
Struct :: Struct DstX (Matrix (Matrix Z)))
            , (XOrtOrientation Z -> X (Rt Z))
-> Struct DstX Z -> X (SomeEntityG Rt (HomCo Matrix DstX Op))
forall (t :: * -> *) x.
Entity (t x) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> X (SomeEntityG t (HomCo Matrix DstX Op))
xse XOrtOrientation Z -> X (Rt Z)
forall x. Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt (Struct DstX Z
forall s x. Structure s x => Struct s x
Struct :: Struct DstX Z)
            ]

xsct ::
  ( Entity (t x)
  , Entity (t z)
  )
  => (XOrtOrientation x -> X (t x)) -> Struct DstX x
  -> a y z -> a x y -> X (SomeCmpb2G t a)
xsct :: forall (t :: * -> *) x z (a :: * -> * -> *) y.
(Entity (t x), Entity (t z)) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G t a)
xsct XOrtOrientation x -> X (t x)
xt Struct DstX x
Struct a y z
f a x y
g = XOrtOrientation x -> X (t x)
xt XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation X (t x) -> (t x -> X (SomeCmpb2G t a)) -> X (SomeCmpb2G t a)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SomeCmpb2G t a -> X (SomeCmpb2G t a)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeCmpb2G t a -> X (SomeCmpb2G t a))
-> (t x -> SomeCmpb2G t a) -> t x -> X (SomeCmpb2G t a)
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
. a y z -> a x y -> t x -> SomeCmpb2G t a
forall (t :: * -> *) x z (c :: * -> * -> *) y.
(Entity (t x), Entity (t z)) =>
c y z -> c x y -> t x -> SomeCmpb2G t c
SomeCmpb2G a y z
f a x y
g

xsctId :: Struct DstX x -> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Id a)
xsctId :: forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Id a)
xsctId sx :: Struct DstX x
sx@Struct DstX x
Struct Struct DstX z
Struct = (XOrtOrientation x -> X (Id x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G Id a)
forall (t :: * -> *) x z (a :: * -> * -> *) y.
(Entity (t x), Entity (t z)) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G t a)
xsct XOrtOrientation x -> X (Id x)
forall x. XOrtOrientation x -> X (Id x)
xsoId Struct DstX x
sx

xsctPnt :: Struct DstX x -> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Pnt a)
xsctPnt :: forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Pnt a)
xsctPnt sx :: Struct DstX x
sx@Struct DstX x
Struct Struct DstX z
Struct = (XOrtOrientation x -> X (Pnt x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G Pnt a)
forall (t :: * -> *) x z (a :: * -> * -> *) y.
(Entity (t x), Entity (t z)) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G t a)
xsct XOrtOrientation x -> X (Pnt x)
forall x. Oriented x => XOrtOrientation x -> X (Pnt x)
xsoPnt Struct DstX x
sx 

xsctRt :: Struct DstX x -> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Rt a)
xsctRt :: forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Rt a)
xsctRt sx :: Struct DstX x
sx@Struct DstX x
Struct Struct DstX z
Struct = (XOrtOrientation x -> X (Rt x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G Rt a)
forall (t :: * -> *) x z (a :: * -> * -> *) y.
(Entity (t x), Entity (t z)) =>
(XOrtOrientation x -> X (t x))
-> Struct DstX x -> a y z -> a x y -> X (SomeCmpb2G t a)
xsct XOrtOrientation x -> X (Rt x)
forall x. Distributive x => XOrtOrientation x -> X (Rt x)
xsoRt Struct DstX x
sx

xscId :: SomeCmpb2 (HomCo Matrix DstX Op) -> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscId :: SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscId (SomeCmpb2 HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g) = Struct DstX x
-> Struct DstX z
-> HomCo Matrix DstX Op y z
-> HomCo Matrix DstX Op x y
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Id a)
xsctId (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
g) (HomCo Matrix DstX Op y z
-> Struct (ObjectClass (HomCo Matrix DstX Op)) z
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range HomCo Matrix DstX Op y z
f) HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g

xscPnt :: SomeCmpb2 (HomCo Matrix DstX Op) -> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
xscPnt :: SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
xscPnt (SomeCmpb2 HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g) = Struct DstX x
-> Struct DstX z
-> HomCo Matrix DstX Op y z
-> HomCo Matrix DstX Op x y
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Pnt a)
xsctPnt (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
g) (HomCo Matrix DstX Op y z
-> Struct (ObjectClass (HomCo Matrix DstX Op)) z
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range HomCo Matrix DstX Op y z
f) HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g

xscRt :: SomeCmpb2 (HomCo Matrix DstX Op) -> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
xscRt :: SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
xscRt (SomeCmpb2 HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g) = Struct DstX x
-> Struct DstX z
-> HomCo Matrix DstX Op y z
-> HomCo Matrix DstX Op x y
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
forall x z (a :: * -> * -> *) y.
Struct DstX x
-> Struct DstX z -> a y z -> a x y -> X (SomeCmpb2G Rt a)
xsctRt (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
g) (HomCo Matrix DstX Op y z
-> Struct (ObjectClass (HomCo Matrix DstX Op)) z
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range HomCo Matrix DstX Op y z
f) HomCo Matrix DstX Op y z
f HomCo Matrix DstX Op x y
g

xsc :: X (SomeCmpb2 (HomCo Matrix DstX Op))
xsc :: X (SomeCmpb2 (HomCo Matrix DstX Op))
xsc = N
-> X (SomeObjectClass (HomCo Matrix DstX Op))
-> X (SomeMorphism (MorCo Matrix DstX Op))
-> X (SomeCmpb2 (HomCo Matrix DstX Op))
forall (o :: * -> *) s (m :: * -> *).
TransformableG o s s =>
N
-> X (SomeObjectClass (HomCo m s o))
-> X (SomeMorphism (MorCo m s o))
-> X (SomeCmpb2 (HomCo m s o))
xscHomCo N
10 ((SomeEntityG Id (HomCo Matrix DstX Op)
 -> SomeObjectClass (HomCo Matrix DstX Op))
-> X (SomeEntityG Id (HomCo Matrix DstX Op))
-> X (SomeObjectClass (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeEntityG Id (HomCo Matrix DstX Op)
-> SomeObjectClass (HomCo Matrix DstX Op)
forall s (t :: * -> *) (m :: * -> *) (o :: * -> *).
Transformable s Typ =>
SomeEntityG t (HomCo m s o) -> SomeObjectClass (HomCo m s o)
seoc X (SomeEntityG Id (HomCo Matrix DstX Op))
xseId) X (SomeMorphism (MorCo Matrix DstX Op))
xMorCo

seoc :: Transformable s Typ => SomeEntityG t (HomCo m s o) -> SomeObjectClass (HomCo m s o)
seoc :: forall s (t :: * -> *) (m :: * -> *) (o :: * -> *).
Transformable s Typ =>
SomeEntityG t (HomCo m s o) -> SomeObjectClass (HomCo m s o)
seoc (SomeEntityG Struct (ObjectClass (HomCo m s o)) x
s t x
_) = Struct (ObjectClass (HomCo m s o)) x
-> SomeObjectClass (HomCo m s o)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass Struct (ObjectClass (HomCo m s o)) x
s

xMorCo :: X (SomeMorphism (MorCo Matrix DstX Op))
xMorCo :: X (SomeMorphism (MorCo Matrix DstX Op))
xMorCo = [SomeMorphism (MorCo Matrix DstX Op)]
-> X (SomeMorphism (MorCo Matrix DstX Op))
forall a. [a] -> X a
xOneOf [ MorCo Matrix DstX Op (Op (Matrix Z)) (Matrix (Op Z))
-> SomeMorphism (MorCo Matrix DstX Op)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (MorCo Matrix DstX Op (Op (Matrix Z)) (Matrix (Op Z))
forall s x1 (m :: * -> *) (o :: * -> *).
(Structure s x1, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (o (m x1)) (m (o x1))
ToCo   :: MorCo Matrix DstX Op (Op (Matrix Z)) (Matrix (Op Z)))
                , MorCo
  Matrix DstX Op (Op (Matrix (Matrix Z))) (Matrix (Op (Matrix Z)))
-> SomeMorphism (MorCo Matrix DstX Op)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (MorCo
  Matrix DstX Op (Op (Matrix (Matrix Z))) (Matrix (Op (Matrix Z)))
forall s x1 (m :: * -> *) (o :: * -> *).
(Structure s x1, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (o (m x1)) (m (o x1))
ToCo   :: MorCo Matrix DstX Op
                                            (Op (Matrix (Matrix Z))) (Matrix (Op (Matrix Z)))
                               )
                , MorCo Matrix DstX Op (Matrix (Op Z)) (Op (Matrix Z))
-> SomeMorphism (MorCo Matrix DstX Op)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (MorCo Matrix DstX Op (Matrix (Op Z)) (Op (Matrix Z))
forall s x1 (m :: * -> *) (o :: * -> *).
(Structure s x1, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (m (o x1)) (o (m x1))
FromCo :: MorCo Matrix DstX Op (Matrix (Op Z)) (Op (Matrix Z)))
                , MorCo
  Matrix DstX Op (Matrix (Op (Matrix Z))) (Op (Matrix (Matrix Z)))
-> SomeMorphism (MorCo Matrix DstX Op)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (MorCo
  Matrix DstX Op (Matrix (Op (Matrix Z))) (Op (Matrix (Matrix Z)))
forall s x1 (m :: * -> *) (o :: * -> *).
(Structure s x1, TransformableG m s s, TransformableG o s s) =>
MorCo m s o (m (o x1)) (o (m x1))
FromCo :: MorCo Matrix DstX Op
                                            (Matrix (Op (Matrix Z))) (Op (Matrix (Matrix Z)))
                               )
                ]

sap :: Category c => SomeCmpb2G Id c -> SomeApplication c
sap :: forall (c :: * -> * -> *).
Category c =>
SomeCmpb2G Id c -> SomeApplication c
sap (SomeCmpb2G c y z
f c x y
g (Id x
x)) = c x z -> x -> SomeApplication c
forall (h :: * -> * -> *) x y. h x y -> x -> SomeApplication h
SomeApplication (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

smp :: Category c => SomeCmpb2G t c -> SomeMorphism c
smp :: forall (c :: * -> * -> *) (t :: * -> *).
Category c =>
SomeCmpb2G t c -> SomeMorphism c
smp (SomeCmpb2G c y z
f c x y
g t x
_) = c x z -> SomeMorphism c
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (c y z
fc 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)

xscG :: X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG :: X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG = X (X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
 -> X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
-> X (X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SomeCmpb2 (HomCo Matrix DstX Op)
 -> X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
-> X (SomeCmpb2 (HomCo Matrix DstX Op))
-> X (X (SomeCmpb2G Id (HomCo Matrix DstX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscId X (SomeCmpb2 (HomCo Matrix DstX Op))
xsc

relHomMltStruct :: HomMultiplicativeDisjunctive h => Struct DstX x -> h x y -> Statement
relHomMltStruct :: forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
Struct DstX x -> h x y -> Statement
relHomMltStruct Struct DstX x
Struct h x y
h
  = h x y -> XHomMlt x -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
h x y -> XHomMlt x -> Statement
prpHomMultiplicativeDisjunctive h x y
h (XMlt x -> XHomMlt x
forall x. XMlt x -> XHomMlt x
xMltHomMlt (XMlt x -> XHomMlt x) -> XMlt x -> XHomMlt x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X N -> XOrtOrientation x -> XMlt x
forall c. Multiplicative c => X N -> XOrtOrientation c -> XMlt c
xoMlt (N -> N -> X N
xNB N
0 N
5) XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation)

relHomMlt :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomMlt :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomMlt X (SomeMorphism (HomCo Matrix DstX Op))
xsm = X (SomeMorphism (HomCo Matrix DstX Op))
-> (SomeMorphism (HomCo Matrix DstX Op) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomCo Matrix DstX Op))
xsm (\(SomeMorphism HomCo Matrix DstX Op x y
h) -> Struct DstX x -> HomCo Matrix DstX Op x y -> Statement
forall (h :: * -> * -> *) x y.
HomMultiplicativeDisjunctive h =>
Struct DstX x -> h x y -> Statement
relHomMltStruct (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
h) HomCo Matrix DstX Op x y
h) 

xo :: Struct DstX x -> XOrtOrientation x
xo :: forall x. Struct DstX x -> XOrtOrientation x
xo Struct DstX x
Struct = XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation

relHomFbrOrtStruct :: (HomFibredOrientedDisjunctive h, Show2 h)
  => Struct DstX x -> h x y ->  Statement
relHomFbrOrtStruct :: forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Struct DstX x -> h x y -> Statement
relHomFbrOrtStruct s :: Struct DstX x
s@Struct DstX x
Struct h x y
h = X (Orientation (Point x))
-> (Orientation (Point x) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall (XOrtOrientation x -> X (Orientation (Point x))
XOrtOrientation x -> X (Root x)
forall a. FibredOriented a => XOrtOrientation a -> X (Root a)
xoRoot (XOrtOrientation x -> X (Orientation (Point x)))
-> XOrtOrientation x -> X (Orientation (Point x))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Struct DstX x -> XOrtOrientation x
forall x. Struct DstX x -> XOrtOrientation x
xo Struct DstX x
s) (h x y -> Root x -> Statement
forall (h :: * -> * -> *) a b.
(HomFibredOrientedDisjunctive h, Show2 h) =>
h a b -> Root a -> Statement
prpHomFbrOrtDisj h x y
h)

relHomFbrOrt :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomFbrOrt :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomFbrOrt X (SomeMorphism (HomCo Matrix DstX Op))
xsm = X (SomeMorphism (HomCo Matrix DstX Op))
-> (SomeMorphism (HomCo Matrix DstX Op) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomCo Matrix DstX Op))
xsm (\(SomeMorphism HomCo Matrix DstX Op x y
h) -> Struct DstX x -> HomCo Matrix DstX Op x y -> Statement
forall (h :: * -> * -> *) x y.
(HomFibredOrientedDisjunctive h, Show2 h) =>
Struct DstX x -> h x y -> Statement
relHomFbrOrtStruct (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
h) HomCo Matrix DstX Op x y
h)

relHomAddStruct :: (HomAdditive h, Show2 h) => Struct DstX x -> h x y -> Statement
relHomAddStruct :: forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
Struct DstX x -> h x y -> Statement
relHomAddStruct Struct DstX x
Struct h x y
h = h x y -> XAdd x -> Statement
forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
h x y -> XAdd x -> Statement
prpHomAdditive h x y
h (X N -> XOrtOrientation x -> XAdd x
forall a. FibredOriented a => X N -> XOrtOrientation a -> XAdd a
xoAdd (N -> N -> X N
xNB N
0 N
5) XOrtOrientation x
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation)

relHomAdd :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomAdd :: X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomAdd X (SomeMorphism (HomCo Matrix DstX Op))
xsm = X (SomeMorphism (HomCo Matrix DstX Op))
-> (SomeMorphism (HomCo Matrix DstX Op) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeMorphism (HomCo Matrix DstX Op))
xsm (\(SomeMorphism HomCo Matrix DstX Op x y
h) -> Struct DstX x -> HomCo Matrix DstX Op x y -> Statement
forall (h :: * -> * -> *) x y.
(HomAdditive h, Show2 h) =>
Struct DstX x -> h x y -> Statement
relHomAddStruct (HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall x y.
HomCo Matrix DstX Op x y
-> Struct (ObjectClass (HomCo Matrix DstX Op)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomCo Matrix DstX Op x y
h) HomCo Matrix DstX Op x y
h)

--------------------------------------------------------------------------------
-- prpHomCoMatrixOp -

-- | validity of 'HomCo'.
prpHomCoMatrixOp :: Statement
prpHomCoMatrixOp :: Statement
prpHomCoMatrixOp = String -> Label
Prp String
"HomCoMatrixOp" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ X (SomeEntityG Id (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op)) -> Statement
forall (t :: * -> *) (m :: * -> *) s (o :: * -> *).
(FunctorialG t (HomCo m s o) (->), m ~ Matrix, o ~ Op, s ~ DstX) =>
X (SomeEntityG t (HomCo m s o))
-> X (SomeCmpb2G t (HomCo m s o)) -> Statement
prpHomCoMatrixOpFunctorial X (SomeEntityG Id (HomCo Matrix DstX Op))
xseId X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG
      , X (SomeEntityG Pnt (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)) -> Statement
forall (t :: * -> *) (m :: * -> *) s (o :: * -> *).
(FunctorialG t (HomCo m s o) (->), m ~ Matrix, o ~ Op, s ~ DstX) =>
X (SomeEntityG t (HomCo m s o))
-> X (SomeCmpb2G t (HomCo m s o)) -> Statement
prpHomCoMatrixOpFunctorial X (SomeEntityG Pnt (HomCo Matrix DstX Op))
xsePnt (X (X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
 -> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
-> X (X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SomeCmpb2 (HomCo Matrix DstX Op)
 -> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2 (HomCo Matrix DstX Op))
-> X (X (SomeCmpb2G Pnt (HomCo Matrix DstX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Pnt (HomCo Matrix DstX Op))
xscPnt X (SomeCmpb2 (HomCo Matrix DstX Op))
xsc)
      , X (SomeEntityG Rt (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op)) -> Statement
forall (t :: * -> *) (m :: * -> *) s (o :: * -> *).
(FunctorialG t (HomCo m s o) (->), m ~ Matrix, o ~ Op, s ~ DstX) =>
X (SomeEntityG t (HomCo m s o))
-> X (SomeCmpb2G t (HomCo m s o)) -> Statement
prpHomCoMatrixOpFunctorial X (SomeEntityG Rt (HomCo Matrix DstX Op))
xseRt (X (X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (X (X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
 -> X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
-> X (X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ (SomeCmpb2 (HomCo Matrix DstX Op)
 -> X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
-> X (SomeCmpb2 (HomCo Matrix DstX Op))
-> X (X (SomeCmpb2G Rt (HomCo Matrix DstX Op)))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomCo Matrix DstX Op)
-> X (SomeCmpb2G Rt (HomCo Matrix DstX Op))
xscRt X (SomeCmpb2 (HomCo Matrix DstX Op))
xsc)
      , X (SomeApplication (HomCo Matrix DstX Op)) -> Statement
forall (h :: * -> * -> *).
(HomOrientedDisjunctive h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomOrientedDisjunctive ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeApplication (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeApplication (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeApplication (HomCo Matrix DstX Op)
forall (c :: * -> * -> *).
Category c =>
SomeCmpb2G Id c -> SomeApplication c
sap X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG)
      , X (SomeApplication (HomCo Matrix DstX Op)) -> Statement
forall (h :: * -> * -> *).
(HomFibred h, Show2 h) =>
X (SomeApplication h) -> Statement
prpHomFibred ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeApplication (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeApplication (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeApplication (HomCo Matrix DstX Op)
forall (c :: * -> * -> *).
Category c =>
SomeCmpb2G Id c -> SomeApplication c
sap X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG)
      , X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomFbrOrt ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeMorphism (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeMorphism (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeMorphism (HomCo Matrix DstX Op)
forall (c :: * -> * -> *) (t :: * -> *).
Category c =>
SomeCmpb2G t c -> SomeMorphism c
smp X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG)
      , X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomAdd ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeMorphism (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeMorphism (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeMorphism (HomCo Matrix DstX Op)
forall (c :: * -> * -> *) (t :: * -> *).
Category c =>
SomeCmpb2G t c -> SomeMorphism c
smp X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG)
      , X (SomeMorphism (HomCo Matrix DstX Op)) -> Statement
relHomMlt ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeMorphism (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeMorphism (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeMorphism (HomCo Matrix DstX Op)
forall (c :: * -> * -> *) (t :: * -> *).
Category c =>
SomeCmpb2G t c -> SomeMorphism c
smp X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG)
      ]

--------------------------------------------------------------------------------
-- distributions -

dstrHomCoMatrix :: Int -> IO ()
dstrHomCoMatrix :: Int -> IO ()
dstrHomCoMatrix Int
n = (SomeMorphism (HomCo Matrix DstX Op) -> [String])
-> Int -> X (SomeMorphism (HomCo Matrix DstX Op)) -> IO ()
forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr SomeMorphism (HomCo Matrix DstX Op) -> [String]
asp Int
n ((SomeCmpb2G Id (HomCo Matrix DstX Op)
 -> SomeMorphism (HomCo Matrix DstX Op))
-> X (SomeCmpb2G Id (HomCo Matrix DstX Op))
-> X (SomeMorphism (HomCo Matrix DstX Op))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2G Id (HomCo Matrix DstX Op)
-> SomeMorphism (HomCo Matrix DstX Op)
forall (c :: * -> * -> *) (t :: * -> *).
Category c =>
SomeCmpb2G t c -> SomeMorphism c
smp X (SomeCmpb2G Id (HomCo Matrix DstX Op))
xscG) where
  asp :: SomeMorphism (HomCo Matrix DstX Op) -> [String]
  asp :: SomeMorphism (HomCo Matrix DstX Op) -> [String]
asp (SomeMorphism HomCo Matrix DstX Op x y
h) = [Variant -> String
forall a. Show a => a -> String
show (Variant -> String) -> Variant -> String
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ HomCo Matrix DstX Op x y -> Variant
forall x. Disjunctive x => x -> Variant
variant HomCo Matrix DstX Op x y
h]
  
--------------------------------------------------------------------------------
-- dstDimMatixMatrix -

dstDimMatrixMatrix :: Int -> IO ()
dstDimMatrixMatrix :: Int -> IO ()
dstDimMatrixMatrix Int
n = (Dim (Matrix Z) (Dim Z ()) -> [String])
-> Int -> X (Dim (Matrix Z) (Dim Z ())) -> IO ()
forall x. (x -> [String]) -> Int -> X x -> IO ()
putDstr Dim (Matrix Z) (Dim Z ()) -> [String]
forall {a}. Show a => a -> [String]
asp Int
n X (Dim (Matrix Z) (Dim Z ()))
xMM where
  xMM :: X (Point (Matrix (Matrix Z)))
xMM = XOrtOrientation (Matrix (Matrix Z))
-> X (Point (Matrix (Matrix Z)))
forall q. Oriented q => XOrtOrientation q -> X (Point q)
xoPoint (XOrtOrientation (Matrix (Matrix Z))
forall q. XStandardOrtOrientation q => XOrtOrientation q
xStandardOrtOrientation :: XOrtOrientation (Matrix (Matrix Z)))
  asp :: a -> [String]
asp a
dMM = [a -> String
forall a. Show a => a -> String
show a
dMM]