{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Entity.Diagram.Diagrammatic

-- Description : objects with a naturally underlying diagram.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- objects with a naturally underlying 'Diagram'. They serve to generalize the concept of

-- limits according to a diagram (see "OAlg.Limes.Limits").

module OAlg.Entity.Diagram.Diagrammatic
  (
    -- * Diagrammatic

    Diagrammatic(..)
  , DiagramG(..), dmap
  , sdbToDgmObj, sdbFromDgmObj

    -- * Natural

    
  , NaturalDiagrammatic
  , drohS
  , NaturalDiagrammaticW

    -- * Duality

  , NaturalDiagrammaticBi

  , prpNaturalDiagrammatic
{-  
    -- * Proposition
  , prpDiagrammatic
-}
  ) where

import Control.Monad

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.NaturalTransformable
import OAlg.Category.SDuality
import OAlg.Category.Unify

import OAlg.Data.Either

import OAlg.Hom.Definition
import OAlg.Hom.Oriented

import OAlg.Structure.Oriented

import OAlg.Entity.Natural
import OAlg.Entity.Diagram.Definition

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

-- Diagrammatic -


-- | object @__d__@ having an underlying 'Diagram'.

class Diagrammatic d where
  diagram :: d t n m x -> Diagram t n m x

instance Diagrammatic Diagram where diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x.
Diagram t n m x -> Diagram t n m x
diagram = Diagram t n m x -> Diagram t n m x
forall x. x -> x
id

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

-- DiagramG -


-- | wrapper for 'Diagrammatic'-objects.

newtype DiagramG d (t :: DiagramType) (n :: N') (m :: N') x = DiagramG (d t n m x)
  deriving (Int -> DiagramG d t n m x -> ShowS
[DiagramG d t n m x] -> ShowS
DiagramG d t n m x -> String
(Int -> DiagramG d t n m x -> ShowS)
-> (DiagramG d t n m x -> String)
-> ([DiagramG d t n m x] -> ShowS)
-> Show (DiagramG d t n m x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
Int -> DiagramG d t n m x -> ShowS
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
[DiagramG d t n m x] -> ShowS
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
DiagramG d t n m x -> String
$cshowsPrec :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
Int -> DiagramG d t n m x -> ShowS
showsPrec :: Int -> DiagramG d t n m x -> ShowS
$cshow :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
DiagramG d t n m x -> String
show :: DiagramG d t n m x -> String
$cshowList :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Show (d t n m x) =>
[DiagramG d t n m x] -> ShowS
showList :: [DiagramG d t n m x] -> ShowS
Show,DiagramG d t n m x -> DiagramG d t n m x -> Bool
(DiagramG d t n m x -> DiagramG d t n m x -> Bool)
-> (DiagramG d t n m x -> DiagramG d t n m x -> Bool)
-> Eq (DiagramG d t n m x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Eq (d t n m x) =>
DiagramG d t n m x -> DiagramG d t n m x -> Bool
$c== :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Eq (d t n m x) =>
DiagramG d t n m x -> DiagramG d t n m x -> Bool
== :: DiagramG d t n m x -> DiagramG d t n m x -> Bool
$c/= :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Eq (d t n m x) =>
DiagramG d t n m x -> DiagramG d t n m x -> Bool
/= :: DiagramG d t n m x -> DiagramG d t n m x -> Bool
Eq)

type instance Dual1 (DiagramG d t n m) = DiagramG d (Dual t) n m

instance Oriented x => ShowDual1 (DiagramG Diagram t n m) x
instance Oriented x => EqDual1 (DiagramG Diagram t n m) x

instance Validable (d t n m x) => Validable (DiagramG d t n m x) where
  valid :: DiagramG d t n m x -> Statement
valid (DiagramG d t n m x
d) = d t n m x -> Statement
forall a. Validable a => a -> Statement
valid d t n m x
d

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

-- dmap -


-- | the induced mapping between the 'Diagrammatic' objects.

--

-- __Property__ Let @'ApplicativeG' ('DiagramG __d t n m) __h__ (->)@ and @h@ in @__h__@, then holds:

--

-- (1) @'DiagramG' '.' 'dmap' h '.=.' 'amapG' h '.' 'DiagramG'@.

dmap :: ApplicativeG (DiagramG d t n m) h (->)
  => h x y -> d t n m x -> d t n m y
dmap :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (h :: * -> * -> *) x y.
ApplicativeG (DiagramG d t n m) h (->) =>
h x y -> d t n m x -> d t n m y
dmap h x y
h d t n m x
d = d t n m y
d' where DiagramG d t n m y
d' = h x y -> DiagramG d t n m x -> DiagramG d t n m y
forall x y. h x y -> DiagramG d t n m x -> DiagramG d t n m y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d)


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

-- droh -


-- | the underlying diagram.

droh :: Diagrammatic d => DiagramG d t n m x -> DiagramG Diagram t n m x
droh :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
DiagramG d t n m x -> DiagramG Diagram t n m x
droh (DiagramG d t n m x
d) = Diagram t n m x -> DiagramG Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG (d t n m x -> Diagram t n m x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d t n m x
d)

instance Diagrammatic d => Natural s (->) (DiagramG d t n m) (DiagramG Diagram t n m) where
  roh :: forall x.
Struct s x -> DiagramG d t n m x -> DiagramG Diagram t n m x
roh Struct s x
_ = DiagramG d t n m x -> DiagramG Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
DiagramG d t n m x -> DiagramG Diagram t n m x
droh

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

-- sdbToDgmObj -


-- | canonical mapping to its underlying diagrammatic object.

sdbToDgmObj :: Dual1 (d t n m) ~ d (Dual t) n m
  => SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbToDgmObj :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbToDgmObj (SDualBi (Right1 (DiagramG d t n m x
d))) = Either1 (Dual1 (d t n m)) (d t n m) x -> SDualBi (d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (d t n m x -> Either1 (d (Dual t) n m) (d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 d t n m x
d)
sdbToDgmObj (SDualBi (Left1 (DiagramG d (Dual t) n m x
d'))) = Either1 (Dual1 (d t n m)) (d t n m) x -> SDualBi (d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (d (Dual t) n m x -> Either1 (d (Dual t) n m) (d t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 d (Dual t) n m x
d')

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

-- sdbFromDgmObj -


-- | canonical mapping from its underlying diagrammatic object.

sdbFromDgmObj :: Dual1 (d t n m) ~ d (Dual t) n m
  => SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
sdbFromDgmObj :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
sdbFromDgmObj (SDualBi (Right1 d t n m x
d)) = Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d t n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (d t n m x -> DiagramG d t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d t n m x
d))
sdbFromDgmObj (SDualBi (Left1 Dual1 (d t n m) x
d')) = Either1 (Dual1 (DiagramG d t n m)) (DiagramG d t n m) x
-> SDualBi (DiagramG d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG d (Dual t) n m x
-> Either1 (DiagramG d (Dual t) n m) (DiagramG d t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (d (Dual t) n m x -> DiagramG d (Dual t) n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG d (Dual t) n m x
Dual1 (d t n m) x
d'))

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

-- drohS -


-- | natural assocition induced by 'droh' betewwn @'SDualBi' ('DiagramG' __d t n m__)@ and

-- @'SDualBi' ('Diagram' __t n m__)@.

drohS :: Diagrammatic d => SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x
drohS :: forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x
drohS (SDualBi (Right1 DiagramG d t n m x
d)) = Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram t n m x
-> Either1
     (DiagramG Diagram (Dual t) n m) (DiagramG Diagram t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (DiagramG d t n m x -> DiagramG Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
DiagramG d t n m x -> DiagramG Diagram t n m x
droh DiagramG d t n m x
d))
drohS (SDualBi (Left1 Dual1 (DiagramG d t n m) x
d')) = Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram (Dual t) n m x
-> Either1
     (DiagramG Diagram (Dual t) n m) (DiagramG Diagram t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (DiagramG d (Dual t) n m x -> DiagramG Diagram (Dual t) n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
DiagramG d t n m x -> DiagramG Diagram t n m x
droh Dual1 (DiagramG d t n m) x
DiagramG d (Dual t) n m x
d'))

instance Diagrammatic d
  => Natural s (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)) where
  roh :: forall x.
Struct s x
-> SDualBi (DiagramG d t n m) x
   -> SDualBi (DiagramG Diagram t n m) x
roh Struct s x
_ = SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x
drohS

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

-- NaturalDiagrammatic -


-- | natural transformation on 'Diagrammatic' objects from @'SDualBi' ('DiagramG' __d t n m__)@ to

-- @'SDualBi' ('Diagram' __t n m__)@, respecting the canonical application of @__h__@ on

-- @'SDualBi' ('Diagram' __t n m__)@.

--

-- __Property__ Let @'NaturalDiagrammatic' __s h d t n m__@, then for all @__x__@,

-- @__y__@ and @h@ in @__h x y__@ holds:

--

-- (1) @'amapG' h '.=.' dgMapS h@.

--

-- __Note__ This property is required if incoherent instances are permitted.

class
  ( Diagrammatic d
  , CategoryDisjunctive h
  , HomOrientedDisjunctive h
  , FunctorialOriented h
  , NaturalTransformable h (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m))
  , t ~ Dual (Dual t)
  )
  => NaturalDiagrammatic h d t n m

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

-- Diagram -


instance
  ( HomOrientedDisjunctive h
  , t ~ Dual (Dual t)
  )
  => ApplicativeG (SDualBi (DiagramG Diagram t n m)) h (->) where
  amapG :: forall x y.
h x y
-> SDualBi (DiagramG Diagram t n m) x
   -> SDualBi (DiagramG Diagram t n m) y
amapG h x y
h = SDualBi (Diagram t n m) y -> SDualBi (DiagramG Diagram t n m) y
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (d t n m) x -> SDualBi (DiagramG d t n m) x
sdbFromDgmObj (SDualBi (Diagram t n m) y -> SDualBi (DiagramG Diagram t n m) y)
-> (SDualBi (DiagramG Diagram t n m) x
    -> SDualBi (Diagram t n m) y)
-> SDualBi (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) y
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
. h x y -> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall x y.
h x y -> SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG h x y
h (SDualBi (Diagram t n m) x -> SDualBi (Diagram t n m) y)
-> (SDualBi (DiagramG Diagram t n m) x
    -> SDualBi (Diagram t n m) x)
-> SDualBi (DiagramG Diagram t n m) x
-> SDualBi (Diagram t n m) y
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
. SDualBi (DiagramG Diagram t n m) x -> SDualBi (Diagram t n m) x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
(Dual1 (d t n m) ~ d (Dual t) n m) =>
SDualBi (DiagramG d t n m) x -> SDualBi (d t n m) x
sdbToDgmObj

instance
  ( HomOrientedDisjunctive h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => FunctorialG (SDualBi (DiagramG Diagram t n m)) h (->)

instance
  ( HomOrientedDisjunctive h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalTransformable h (->) (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m))

instance
  ( CategoryDisjunctive h
  , HomOrientedDisjunctive h
  , FunctorialOriented h
  , t ~ Dual (Dual t)
  )
  => NaturalDiagrammatic h Diagram t n m

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

-- NaturalDiagrammaticW -


-- | whiteness of a 'NaturalDiagrammatic'.

data NaturalDiagrammaticW h d t n m where
  NaturalDiagrammaticW :: NaturalDiagrammatic h d t n m
    => NaturalDiagrammaticW h d t n m

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

-- NaturalDiagrammaticBi -


-- | natural diagrammatic for @__t__@ and @'Dual' __t__@.

type NaturalDiagrammaticBi h d t n m =
  ( NaturalDiagrammatic h d t n m
  , NaturalDiagrammatic h d (Dual t) n m
  )


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

-- prpNaturalDiagrammatic -


-- | validity according to 'NaturalDiagrammatic'.

prpNaturalDiagrammatic :: NaturalDiagrammatic h d t n m
  => q h d t n m
  -> X (SomeNaturalApplication h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)))
  -> Statement
prpNaturalDiagrammatic :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N')
       (q :: (* -> * -> *)
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *).
NaturalDiagrammatic h d t n m =>
q h d t n m
-> X (SomeNaturalApplication
        h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)))
-> Statement
prpNaturalDiagrammatic q h d t n m
q X (SomeNaturalApplication
     h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)))
xsa = String -> Label
Prp String
"NaturalDiagrammatic"
  Label -> Statement -> Statement
:<=>: X (SomeNaturalApplication
     h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)))
-> (SomeNaturalApplication
      h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m))
    -> Statement)
-> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (SomeNaturalApplication
     h (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)))
xsa (\(SomeNaturalApplication h x y
h SDualBi (DiagramG d t n m) x
d)
                    -> [Statement] -> Statement
And [ NaturalTransformation
  h
  (->)
  (SDualBi (DiagramG d t n m))
  (SDualBi (DiagramG Diagram t n m))
-> h x y -> SDualBi (DiagramG d t n m) x -> Statement
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
NaturalTransformation a (->) f g -> a x y -> f x -> Statement
relNaturalTransformable (q h d t n m
-> NaturalTransformation
     h
     (->)
     (SDualBi (DiagramG d t n m))
     (SDualBi (DiagramG Diagram t n m))
forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N')
       (q :: (* -> * -> *)
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *).
NaturalDiagrammatic h d t n m =>
q h d t n m
-> NaturalTransformation
     h
     (->)
     (SDualBi (DiagramG d t n m))
     (SDualBi (DiagramG Diagram t n m))
n q h d t n m
q) h x y
h SDualBi (DiagramG d t n m) x
d
                           ]
                   )
  where n :: NaturalDiagrammatic h d t n m
          => q h d t n m
          -> NaturalTransformation h (->)
               (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m))
        n :: forall (h :: * -> * -> *) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N')
       (q :: (* -> * -> *)
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *).
NaturalDiagrammatic h d t n m =>
q h d t n m
-> NaturalTransformation
     h
     (->)
     (SDualBi (DiagramG d t n m))
     (SDualBi (DiagramG Diagram t n m))
n q h d t n m
_ = NaturalTransformation
  h
  (->)
  (SDualBi (DiagramG d t n m))
  (SDualBi (DiagramG Diagram t n m))
forall (a :: * -> * -> *) (b :: * -> * -> *) (f :: * -> *)
       (g :: * -> *).
NaturalTransformable a b f g =>
NaturalTransformation a b f g
NaturalTransformation

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

-- xsoOrtSite -


-- | random variable for some object classees of @'SHom' __s s 'Op' __h__@.

xsoOrtSite :: s ~ OrtSiteX => X (SomeObjectClass (SHom s s Op h))
xsoOrtSite :: forall s (h :: * -> * -> *).
(s ~ OrtSiteX) =>
X (SomeObjectClass (SHom s s Op h))
xsoOrtSite = [SomeObjectClass (SHom s s Op h)]
-> X (SomeObjectClass (SHom s s Op h))
forall a. [a] -> X a
xOneOf [ Struct (ObjectClass (SHom s s Op h)) OS
-> SomeObjectClass (SHom s s Op h)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtSiteX OS
forall s x. Structure s x => Struct s x
Struct :: Struct OrtSiteX OS)
                    , Struct (ObjectClass (SHom s s Op h)) (Op OS)
-> SomeObjectClass (SHom s s Op h)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtSiteX (Op OS)
forall s x. Structure s x => Struct s x
Struct :: Struct OrtSiteX (Op OS))
                    , Struct (ObjectClass (SHom s s Op h)) (U N)
-> SomeObjectClass (SHom s s Op h)
forall (m :: * -> * -> *) x.
Transformable (ObjectClass m) Typ =>
Struct (ObjectClass m) x -> SomeObjectClass m
SomeObjectClass (Struct OrtSiteX (U N)
forall s x. Structure s x => Struct s x
Struct :: Struct OrtSiteX (U N))
                    ]

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

-- HomTest -


-- | type for test homs.

type HomTest s = HomDisj s Op (HomId s)

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

-- xsOrtSiteXOp -


-- | random variable for some object classees of @'HomTest' __s__@.

xsOrtSiteXOp :: X (SomeMorphism (HomTest OrtSiteX))
xsOrtSiteXOp :: X (SomeMorphism (HomTest OrtSiteX))
xsOrtSiteXOp = (SomeCmpb2 (HomTest OrtSiteX) -> SomeMorphism (HomTest OrtSiteX))
-> X (SomeCmpb2 (HomTest OrtSiteX))
-> X (SomeMorphism (HomTest OrtSiteX))
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 SomeCmpb2 (HomTest OrtSiteX) -> SomeMorphism (HomTest OrtSiteX)
forall (h :: * -> * -> *).
Category h =>
SomeCmpb2 h -> SomeMorphism h
smCmpb2 (X (SomeCmpb2 (HomTest OrtSiteX))
 -> X (SomeMorphism (HomTest OrtSiteX)))
-> X (SomeCmpb2 (HomTest OrtSiteX))
-> X (SomeMorphism (HomTest OrtSiteX))
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X (SomeObjectClass (SHom OrtSiteX OrtSiteX Op (HomId OrtSiteX)))
-> X (SomeMorphism (HomId OrtSiteX))
-> X (SomeCmpb2 (HomTest OrtSiteX))
forall (o :: * -> *) s (h :: * -> * -> *).
(TransformableG o s s, Morphism h,
 Transformable (ObjectClass h) s) =>
X (SomeObjectClass (SHom s s o h))
-> X (SomeMorphism h) -> X (SomeCmpb2 (HomDisj s o h))
xscmHomDisj X (SomeObjectClass (SHom OrtSiteX OrtSiteX Op (HomId OrtSiteX)))
forall s (h :: * -> * -> *).
(s ~ OrtSiteX) =>
X (SomeObjectClass (SHom s s Op h))
xsoOrtSite X (SomeMorphism (HomId OrtSiteX))
xhid where
  xhid :: X (SomeMorphism (HomId OrtSiteX))
xhid = [SomeMorphism (HomId OrtSiteX)]
-> X (SomeMorphism (HomId OrtSiteX))
forall a. [a] -> X a
xOneOf [ HomId OrtSiteX OS (Id OS) -> SomeMorphism (HomId OrtSiteX)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (HomId OrtSiteX OS (Id OS)
forall s x. (Structure s x, Structure s (Id x)) => HomId s x (Id x)
ToId   :: HomId OrtSiteX OS (Id OS))
                , HomId OrtSiteX (Id OS) OS -> SomeMorphism (HomId OrtSiteX)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (HomId OrtSiteX (Id OS) OS
forall s y. (Structure s y, Structure s (Id y)) => HomId s (Id y) y
FromId :: HomId OrtSiteX (Id OS) OS)
                , HomId OrtSiteX (U N) (Id (U N)) -> SomeMorphism (HomId OrtSiteX)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (HomId OrtSiteX (U N) (Id (U N))
forall s x. (Structure s x, Structure s (Id x)) => HomId s x (Id x)
ToId   :: HomId OrtSiteX (U N) (Id (U N)))
                , HomId OrtSiteX (Id (U Z)) (U Z) -> SomeMorphism (HomId OrtSiteX)
forall (m :: * -> * -> *) x y. m x y -> SomeMorphism m
SomeMorphism (HomId OrtSiteX (Id (U Z)) (U Z)
forall s y. (Structure s y, Structure s (Id y)) => HomId s (Id y) y
FromId :: HomId OrtSiteX (Id (U Z)) (U Z)) 
                ]
         
--------------------------------------------------------------------------------

-- xsaChainTo -


xdChainToStruct :: (n ~ m+1, t ~ Chain To, Show2 h)
  => Any m
  -> Homomorphous OrtSiteX x y 
  -> h x y
  -> X (SomeNaturalApplication h (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdChainToStruct :: forall (n :: N') (m :: N') (t :: DiagramType) (h :: * -> * -> *) x
       y.
(n ~ (m + 1), t ~ 'Chain 'To, Show2 h) =>
Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdChainToStruct Any m
m (Struct OrtSiteX x
Struct :>: Struct OrtSiteX y
Struct) h x y
h = do
  Bool
b <- X Bool
xBool
  case Bool
b of
    Bool
True  -> do
      Diagram ('Chain 'To) n m x
d <- (Dual (Dual ('Chain 'To)) :~: 'Chain 'To)
-> XDiagram ('Chain 'To) n m x -> X (Diagram ('Chain 'To) n m x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Chain 'To)) :~: 'Chain 'To
'Chain 'To :~: 'Chain 'To
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'To x -> XDiagram ('Chain 'To) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Chain 'To) (m + 1) m a
XDiagramChainTo Any m
m XOrtSite 'To x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite)
      SomeNaturalApplication
  h
  (SDualBi (DiagramG Diagram t n m))
  (SDualBi (DiagramG Diagram t n m))
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (h x y
-> SDualBi (DiagramG Diagram t n m) x
-> SomeNaturalApplication
     h
     (SDualBi (DiagramG Diagram t n m))
     (SDualBi (DiagramG Diagram t n m))
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
a x y -> f x -> SomeNaturalApplication a f g
SomeNaturalApplication h x y
h (Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram t n m x
-> Either1
     (DiagramG Diagram ('Chain 'From) ('S m) m)
     (DiagramG Diagram t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Diagram t n m x -> DiagramG Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG Diagram t n m x
Diagram ('Chain 'To) n m x
d))))
    Bool
False -> do
      Diagram ('Chain 'From) ('S m) m x
d <- (Dual (Dual ('Chain 'From)) :~: 'Chain 'From)
-> XDiagram ('Chain 'From) ('S m) m x
-> X (Diagram ('Chain 'From) ('S m) m x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Chain 'From)) :~: 'Chain 'From
'Chain 'From :~: 'Chain 'From
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'From x -> XDiagram ('Chain 'From) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Chain 'From) (m + 1) m a
XDiagramChainFrom Any m
m XOrtSite 'From x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite)
      SomeNaturalApplication
  h
  (SDualBi (DiagramG Diagram t n m))
  (SDualBi (DiagramG Diagram t n m))
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (h x y
-> SDualBi (DiagramG Diagram t n m) x
-> SomeNaturalApplication
     h
     (SDualBi (DiagramG Diagram t n m))
     (SDualBi (DiagramG Diagram t n m))
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
a x y -> f x -> SomeNaturalApplication a f g
SomeNaturalApplication h x y
h (Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram ('Chain 'From) ('S m) m x
-> Either1
     (DiagramG Diagram ('Chain 'From) ('S m) m)
     (DiagramG Diagram t n m)
     x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Diagram ('Chain 'From) ('S m) m x
-> DiagramG Diagram ('Chain 'From) ('S m) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG Diagram ('Chain 'From) ('S m) m x
d))))

xdChainTo ::
  ( Morphism h
  , ObjectClass h ~ OrtSiteX
  , n ~ m+1, t ~ Chain To, Show2 h
  )
  => Any m
  -> h x y
  -> X (SomeNaturalApplication h
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdChainTo :: forall (h :: * -> * -> *) (n :: N') (m :: N') (t :: DiagramType) x
       y.
(Morphism h, ObjectClass h ~ OrtSiteX, n ~ (m + 1), t ~ 'Chain 'To,
 Show2 h) =>
Any m
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdChainTo Any m
m h x y
h = Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall (n :: N') (m :: N') (t :: DiagramType) (h :: * -> * -> *) x
       y.
(n ~ (m + 1), t ~ 'Chain 'To, Show2 h) =>
Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdChainToStruct Any m
m (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h) h x y
h

xsaChainTo ::(n ~ m+1, t ~ Chain To)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtSiteX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m))
       )
xsaChainTo :: forall (n :: N') (m :: N') (t :: DiagramType).
(n ~ (m + 1), t ~ 'Chain 'To) =>
Any m
-> X (SomeNaturalApplication
        (HomTest OrtSiteX)
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xsaChainTo Any m
m = do
  SomeMorphism HomTest OrtSiteX x y
h <- X (SomeMorphism (HomTest OrtSiteX))
xsOrtSiteXOp
  Any m
-> HomTest OrtSiteX x y
-> X (SomeNaturalApplication
        (HomTest OrtSiteX)
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall (h :: * -> * -> *) (n :: N') (m :: N') (t :: DiagramType) x
       y.
(Morphism h, ObjectClass h ~ OrtSiteX, n ~ (m + 1), t ~ 'Chain 'To,
 Show2 h) =>
Any m
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdChainTo Any m
m HomTest OrtSiteX x y
h

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

-- xsaSink -


xdSinkStruct :: (n ~ m+1, t ~ Star To, Show2 h)
  => Any m
  -> Homomorphous OrtSiteX x y 
  -> h x y
  -> X (SomeNaturalApplication h (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdSinkStruct :: forall (n :: N') (m :: N') (t :: DiagramType) (h :: * -> * -> *) x
       y.
(n ~ (m + 1), t ~ 'Star 'To, Show2 h) =>
Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdSinkStruct Any m
m (Struct OrtSiteX x
Struct :>: Struct OrtSiteX y
Struct) h x y
h = do
  Bool
b <- X Bool
xBool
  case Bool
b of
    Bool
True  -> do
      Diagram ('Star 'To) n m x
d <- (Dual (Dual ('Star 'To)) :~: 'Star 'To)
-> XDiagram ('Star 'To) n m x -> X (Diagram ('Star 'To) n m x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Star 'To)) :~: 'Star 'To
'Star 'To :~: 'Star 'To
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'To x -> XDiagram ('Star 'To) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'To a -> XDiagram ('Star 'To) (m + 1) m a
XDiagramSink Any m
m XOrtSite 'To x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite)
      SomeNaturalApplication
  h
  (SDualBi (DiagramG Diagram t n m))
  (SDualBi (DiagramG Diagram t n m))
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (h x y
-> SDualBi (DiagramG Diagram t n m) x
-> SomeNaturalApplication
     h
     (SDualBi (DiagramG Diagram t n m))
     (SDualBi (DiagramG Diagram t n m))
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
a x y -> f x -> SomeNaturalApplication a f g
SomeNaturalApplication h x y
h (Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram t n m x
-> Either1
     (DiagramG Diagram ('Star 'From) ('S m) m)
     (DiagramG Diagram t n m)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (Diagram t n m x -> DiagramG Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG Diagram t n m x
Diagram ('Star 'To) n m x
d))))
    Bool
False -> do
      Diagram ('Star 'From) ('S m) m x
d <- (Dual (Dual ('Star 'From)) :~: 'Star 'From)
-> XDiagram ('Star 'From) ('S m) m x
-> X (Diagram ('Star 'From) ('S m) m x)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
(Dual (Dual t) :~: t) -> XDiagram t n m a -> X (Diagram t n m a)
xDiagram Dual (Dual ('Star 'From)) :~: 'Star 'From
'Star 'From :~: 'Star 'From
forall {k} (a :: k). a :~: a
Refl (Any m -> XOrtSite 'From x -> XDiagram ('Star 'From) (m + 1) m x
forall (m :: N') a.
Any m -> XOrtSite 'From a -> XDiagram ('Star 'From) (m + 1) m a
XDiagramSource Any m
m XOrtSite 'From x
forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite)
      SomeNaturalApplication
  h
  (SDualBi (DiagramG Diagram t n m))
  (SDualBi (DiagramG Diagram t n m))
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (h x y
-> SDualBi (DiagramG Diagram t n m) x
-> SomeNaturalApplication
     h
     (SDualBi (DiagramG Diagram t n m))
     (SDualBi (DiagramG Diagram t n m))
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
a x y -> f x -> SomeNaturalApplication a f g
SomeNaturalApplication h x y
h (Either1 (Dual1 (DiagramG Diagram t n m)) (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram ('Star 'From) ('S m) m x
-> Either1
     (DiagramG Diagram ('Star 'From) ('S m) m)
     (DiagramG Diagram t n m)
     x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (Diagram ('Star 'From) ('S m) m x
-> DiagramG Diagram ('Star 'From) ('S m) m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
d t n m x -> DiagramG d t n m x
DiagramG Diagram ('Star 'From) ('S m) m x
d))))

xdSink ::
  ( Morphism h
  , ObjectClass h ~ OrtSiteX
  , n ~ m+1, t ~ Star To, Show2 h
  )
  => Any m
  -> h x y
  -> X (SomeNaturalApplication h
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdSink :: forall (h :: * -> * -> *) (n :: N') (m :: N') (t :: DiagramType) x
       y.
(Morphism h, ObjectClass h ~ OrtSiteX, n ~ (m + 1), t ~ 'Star 'To,
 Show2 h) =>
Any m
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdSink Any m
m h x y
h = Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall (n :: N') (m :: N') (t :: DiagramType) (h :: * -> * -> *) x
       y.
(n ~ (m + 1), t ~ 'Star 'To, Show2 h) =>
Any m
-> Homomorphous OrtSiteX x y
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdSinkStruct Any m
m (h x y -> Homomorphous (ObjectClass h) x y
forall x y. h x y -> Homomorphous (ObjectClass h) x y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Homomorphous (ObjectClass m) x y
homomorphous h x y
h) h x y
h

xsaSink ::(n ~ m+1, t ~ Star To)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtSiteX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xsaSink :: forall (n :: N') (m :: N') (t :: DiagramType).
(n ~ (m + 1), t ~ 'Star 'To) =>
Any m
-> X (SomeNaturalApplication
        (HomTest OrtSiteX)
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xsaSink Any m
m = do
  SomeMorphism HomTest OrtSiteX x y
h <- X (SomeMorphism (HomTest OrtSiteX))
xsOrtSiteXOp
  Any m
-> HomTest OrtSiteX x y
-> X (SomeNaturalApplication
        (HomTest OrtSiteX)
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
forall (h :: * -> * -> *) (n :: N') (m :: N') (t :: DiagramType) x
       y.
(Morphism h, ObjectClass h ~ OrtSiteX, n ~ (m + 1), t ~ 'Star 'To,
 Show2 h) =>
Any m
-> h x y
-> X (SomeNaturalApplication
        h
        (SDualBi (DiagramG Diagram t n m))
        (SDualBi (DiagramG Diagram t n m)))
xdSink Any m
m HomTest OrtSiteX x y
h

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

-- snaDual -


isoHomTest :: TransformableGRefl Op s => HomTest s x y
  -> Variant2 Contravariant (IsoHomDisj s Op (HomId s)) x (Op x) 
isoHomTest :: forall s x y.
TransformableGRefl Op s =>
HomTest s x y
-> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op x)
isoHomTest = Struct s x
-> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op x)
forall (h :: * -> * -> *) (o :: * -> *) s x.
(Morphism h, TransformableGRefl o s) =>
Struct s x -> Variant2 'Contravariant (IsoHomDisj s o h) x (o x)
isoHomDisj (Struct s x
 -> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op x))
-> (HomTest s x y -> Struct s x)
-> HomTest s x y
-> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op 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
. HomTest s x y -> Struct s x
HomTest s x y -> Struct (ObjectClass (HomDisj s Op (HomId s))) x
forall x y.
HomDisj s Op (HomId s) x y
-> Struct (ObjectClass (HomDisj s Op (HomId s))) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain

snaDual ::
  ( TransformableOrt s
  , TransformableType s
  , TransformableOp s
  , TransformableGRefl Op s
  , t ~ Dual (Dual t)
  )
  => SomeNaturalApplication (HomTest s)
        (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m))    
  -> SomeNaturalApplication (HomTest s)
        (SDualBi (DiagramG Diagram (Dual t) n m)) (SDualBi (Diagram (Dual t) n m))
snaDual :: forall s (t :: DiagramType) (n :: N') (m :: N').
(TransformableOrt s, TransformableType s, TransformableOp s,
 TransformableGRefl Op s, t ~ Dual (Dual t)) =>
SomeNaturalApplication
  (HomTest s)
  (SDualBi (DiagramG Diagram t n m))
  (SDualBi (DiagramG Diagram t n m))
-> SomeNaturalApplication
     (HomTest s)
     (SDualBi (DiagramG Diagram (Dual t) n m))
     (SDualBi (Diagram (Dual t) n m))
snaDual (SomeNaturalApplication HomTest s x y
h SDualBi (DiagramG Diagram t n m) x
sd) = case (Struct s x -> Struct Ort x
forall s x. Transformable s Ort => Struct s x -> Struct Ort x
tauOrt (HomTest s x y -> Struct (ObjectClass (HomTest s)) x
forall x y.
HomDisj s Op (HomId s) x y -> Struct (ObjectClass (HomTest s)) x
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) x
domain HomTest s x y
h), Struct s y -> Struct Ort y
forall s x. Transformable s Ort => Struct s x -> Struct Ort x
tauOrt (HomTest s x y -> Struct (ObjectClass (HomTest s)) y
forall x y.
HomDisj s Op (HomId s) x y -> Struct (ObjectClass (HomTest s)) y
forall (m :: * -> * -> *) x y.
Morphism m =>
m x y -> Struct (ObjectClass m) y
range HomTest s x y
h)) of
    (Struct Ort x
Struct,Struct Ort y
Struct) -> HomTest s (Op x) y
-> SDualBi (DiagramG Diagram (Dual t) n m) (Op x)
-> SomeNaturalApplication
     (HomTest s)
     (SDualBi (DiagramG Diagram (Dual t) n m))
     (SDualBi (Diagram (Dual t) n m))
forall (a :: * -> * -> *) (g :: * -> *) y (f :: * -> *) x.
(Show2 a, Eq (g y), Show (f x)) =>
a x y -> f x -> SomeNaturalApplication a f g
SomeNaturalApplication (HomTest s x y
h HomTest s x y -> HomTest s (Op x) x -> HomTest s (Op x) y
forall y z x. HomTest s y z -> HomTest s x y -> HomTest s x z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. HomTest s (Op x) x
f) SDualBi (DiagramG Diagram (Dual t) n m) (Op x)
sd' where

      Contravariant2 (Inv2 HomDisj s Op (HomId s) x (Op x)
t HomTest s (Op x) x
f) = HomTest s x y
-> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op x)
forall s x y.
TransformableGRefl Op s =>
HomTest s x y
-> Variant2 'Contravariant (IsoHomDisj s Op (HomId s)) x (Op x)
isoHomTest HomTest s x y
h

      sd' :: SDualBi (DiagramG Diagram (Dual t) n m) (Op x)
sd' = case HomDisj s Op (HomId s) x (Op x)
-> SDualBi (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) (Op x)
forall x y.
HomDisj s Op (HomId s) x y
-> SDualBi (DiagramG Diagram t n m) x
-> SDualBi (DiagramG Diagram t n m) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG HomDisj s Op (HomId s) x (Op x)
t SDualBi (DiagramG Diagram t n m) x
sd of
        SDualBi (Right1 DiagramG Diagram t n m (Op x)
d) -> Either1
  (Dual1 (DiagramG Diagram (Dual t) n m))
  (DiagramG Diagram (Dual t) n m)
  (Op x)
-> SDualBi (DiagramG Diagram (Dual t) n m) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram t n m (Op x)
-> Either1
     (DiagramG Diagram t n m) (DiagramG Diagram (Dual t) n m) (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 DiagramG Diagram t n m (Op x)
d)
        SDualBi (Left1 Dual1 (DiagramG Diagram t n m) (Op x)
d') -> Either1
  (Dual1 (DiagramG Diagram (Dual t) n m))
  (DiagramG Diagram (Dual t) n m)
  (Op x)
-> SDualBi (DiagramG Diagram (Dual t) n m) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (DiagramG Diagram (Dual t) n m (Op x)
-> Either1
     (DiagramG Diagram t n m) (DiagramG Diagram (Dual t) n m) (Op x)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Dual1 (DiagramG Diagram t n m) (Op x)
DiagramG Diagram (Dual t) n m (Op x)
d') 
{-
--------------------------------------------------------------------------------
-- xsaChainFrom -

xsaChainFrom :: (n ~ m+1, t ~ Chain From)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtSiteX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xsaChainFrom m = amap1 snaDual $ xsaChainTo m

--------------------------------------------------------------------------------
-- xsaSource -

xsaSource ::(n ~ m+1, t ~ Star From)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtSiteX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xsaSource m = amap1 snaDual $ xsaSink m

--------------------------------------------------------------------------------
-- OrtOrientationX -

data OrtOrientationX

type instance Structure OrtOrientationX x = (Oriented x, XStandardOrtOrientation x)

instance Transformable OrtOrientationX Typ where tau Struct = Struct

instance Transformable OrtOrientationX Ort where tau Struct = Struct
instance TransformableOrt OrtOrientationX

instance TransformableG Op OrtOrientationX OrtOrientationX where tauG Struct = Struct
instance TransformableGRefl Op OrtOrientationX
instance TransformableOp OrtOrientationX

instance Transformable OrtOrientationX Type where tau Struct = Struct
instance TransformableType OrtOrientationX

--------------------------------------------------------------------------------
-- xsoOrtOrientation -

xsoOrtOrientation :: s ~ OrtOrientationX => X (SomeObjectClass (SHom s s Op h))
xsoOrtOrientation
  = xOneOf [ SomeObjectClass (Struct :: Struct OrtOrientationX OS)
           , SomeObjectClass (Struct :: Struct OrtOrientationX (Op OS))
           , SomeObjectClass (Struct :: Struct OrtOrientationX (U Z))
           ]

xsOrtOrientationXOp ::  s ~ OrtOrientationX => X (SomeMorphism (HomTest s))
xsOrtOrientationXOp = amap1 smCmpb2 $ xscmHomDisj xsoOrtOrientation xhid where
  xhid = xOneOf [ SomeMorphism (ToId   :: HomId OrtOrientationX OS (Id OS))
                , SomeMorphism (FromId :: HomId OrtOrientationX (Id OS) OS)
                , SomeMorphism (ToId   :: HomId OrtOrientationX  (U N) (Id (U N)))
                , SomeMorphism (FromId :: HomId OrtOrientationX  (Id (U Z)) (U Z)) 
                ]

dstOrtOrientationXOp :: Int -> IO ()
dstOrtOrientationXOp n = putDstr asp n xsOrtOrientationXOp where
  asp h = [show (ind a, ind b, ind c)] where (a,b,c) = sta h

  ind :: N -> N
  ind 0 = 0
  ind _ = 1

  sta :: SomeMorphism (HomTest s) -> (N,N,N)
  sta (SomeMorphism (HomDisj h)) = staPath (form h) (0,0,0)

  staPath :: Path (SMorphism r s o h) x y -> (N,N,N) -> (N,N,N)
  staPath (IdPath _) res   = res
  staPath (h :. p) (c,t,f) = staPath p res' where
    res' = case h of
      SCov _    -> (c+1,t,f)
      SToDual   -> (c,t+1,f)
      SFromDual -> (c,t,f+1)
  
--------------------------------------------------------------------------------
-- xsaParallelLR -

xdParallelLRStruct :: (n ~ N2, t ~ Parallel LeftToRight, Show2 h)
  => Any m
  -> Homomorphous OrtOrientationX x y 
  -> h x y
  -> X (SomeNaturalApplication h (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdParallelLRStruct m (Struct :>: Struct) h = do
  b <- xBool
  case b of
    True  -> do
      d <- xDiagram Refl (XDiagramParallelLR m xStandardOrtOrientation)
      return (SomeNaturalApplication h (SDualBi (Right1 (DiagramG d))))
    False -> do
      d <- xDiagram Refl (XDiagramParallelRL m xStandardOrtOrientation)
      return (SomeNaturalApplication h (SDualBi (Left1 (DiagramG d))))

xdParallelLR ::
  ( Morphism h, Show2 h
  , ObjectClass h ~ OrtOrientationX
  , n ~ N2, t ~ Parallel LeftToRight
  )
  => Any m
  -> h x y
  -> X (SomeNaturalApplication h
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xdParallelLR m h = xdParallelLRStruct m (homomorphous h) h

xsaParallelLR ::(n ~ N2, t ~ Parallel LeftToRight)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtOrientationX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xsaParallelLR m = do
  SomeMorphism h <- xsOrtOrientationXOp
  xdParallelLR m h

--------------------------------------------------------------------------------
-- xsaParallelRL -

xsaParallelRL ::(n ~ N2, t ~ Parallel RightToLeft)
  => Any m
  -> X (SomeNaturalApplication (HomTest OrtOrientationX)
         (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)))
xsaParallelRL m = amap1 snaDual $ xsaParallelLR m

--------------------------------------------------------------------------------
-- prpDiagrammtic -

-- | validity according to 'NaturalDiagrmmaticS' for some @'HomDisjEmpty' 'OrtSiteX' 'Op'@
-- acting on some 'Diagram's.
prpDiagrammatic :: N -> Statement
prpDiagrammatic nMax = Prp "Diagrammatic"
  :<=>: And [ Forall (xNB 0 nMax)
                (\m -> case someNatural m of
                  SomeNatural m' -> And [ prpNaturalDiagrammatic (chT m') (xsaChainTo m')
                                        , prpNaturalDiagrammatic (chF m') (xsaChainFrom m')
                                        , prpNaturalDiagrammatic (skT m') (xsaSink m')
                                        , prpNaturalDiagrammatic (skF m') (xsaSource m')
                                        , prpNaturalDiagrammatic (lrT m') (xsaParallelLR m')
                                        , prpNaturalDiagrammatic (lrF m') (xsaParallelRL m')
                                        ]
                )
            ]
  where chT :: s ~ OrtSiteX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram (Chain To) (m+1) m
        chT _ = NaturalDiagrammaticW

        chF :: s ~ OrtSiteX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram (Chain From) (m+1) m
        chF _ = NaturalDiagrammaticW

        skT :: s ~ OrtSiteX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram (Star To) (m+1) m
        skT _ = NaturalDiagrammaticW

        skF :: s ~ OrtSiteX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram (Star From) (m+1) m
        skF _ = NaturalDiagrammaticW

        lrT :: s ~ OrtOrientationX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram
               (Parallel LeftToRight) N2 m
        lrT _ = NaturalDiagrammaticW

        lrF :: s ~ OrtOrientationX
          => Any m -> NaturalDiagrammaticW (HomTest s) Diagram
               (Parallel RightToLeft) N2 m
        lrF _ = NaturalDiagrammaticW
-}