{-# OPTIONS_GHC -fno-warn-orphans #-}

{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Cone.Definition

-- Description : definition of cones over diagrammatic objects.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- definition of 'Cone's over 'Diagrammatic' objects.

module OAlg.Limes.Cone.Definition
  (
    -- * Cone

    Cone(..), diagrammaticObject, coneDiagram
  , Perspective(..), cnMltOrDst, coneStruct
  , cnDiagramTypeRefl
  , tip, shell, cnArrows, cnPoints

    -- * Duality

  , module Dl

    -- * Constructions

  , cnDstAdjZero
  , cnPrjOrnt, cnInjOrnt
  , cnPrjDstOrnt, cnInjDstOrnt
  
    -- * X

  , xCnPrjOrnt, xCnPrjDstOrnt
  , xCnInjOrnt, xCnInjDstOrnt

  ) where

import Control.Monad

import Data.Typeable
import Data.Array hiding (range)

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either

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

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

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative
import OAlg.Hom.Distributive

import OAlg.Limes.Perspective

import OAlg.Limes.Cone.Core
import OAlg.Limes.Cone.Duality as Dl

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

-- relConePrjMlt -


prm :: N -> Message
prm :: N -> Message
prm N
i = [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i]

lE, lS, lO, lC, lB :: Label
lE :: Label
lE = String -> Label
Label String
"end"
lS :: Label
lS = String -> Label
Label String
"start"
lO :: Label
lO = String -> Label
Label String
"orientation"
lC :: Label
lC = String -> Label
Label String
"commutative"
lB :: Label
lB = String -> Label
Label String
"bound"

tp2 :: FinList N2 a -> (a,a)
tp2 :: forall a. FinList N2 a -> (a, a)
tp2 (a
a:|a
b:|FinList n1 a
Nil) = (a
a,a
b)

ht :: FinList (n+1) a -> (a,FinList n a)
ht :: forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht (a
x:|FinList n1 a
xs) = (a
x,FinList n a
FinList n1 a
xs)

relConePrjMlt :: Multiplicative a
  => Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt :: forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt Diagram t n m a
DiagramEmpty Point a
t FinList n a
Nil = Point a -> Statement
forall a. Validable a => a -> Statement
valid Point a
t

relConePrjMlt (DiagramDiscrete FinList n (Point a)
ps) Point a
t FinList n a
cs = Point a -> Statement
forall a. Validable a => a -> Statement
valid Point a
t Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld N
0 Point a
t FinList n (Point a)
ps FinList n a
cs where
  vld :: Multiplicative a => N -> Point a -> FinList n (Point a) -> FinList n a
         -> Statement
  vld :: forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld N
_ Point a
_ FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
  vld N
i Point a
t (Point a
p:|FinList n1 (Point a)
ps) (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
t Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
p) Bool -> Message -> Statement
:?> N -> Message
prm N
i
          , N -> Point a -> FinList n1 (Point a) -> FinList n1 a -> Statement
forall a (n :: N').
Multiplicative a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Point a
t FinList n1 (Point a)
ps FinList n1 a
FinList n1 a
cs
          ]

relConePrjMlt (DiagramChainTo Point a
l FinList m a
as) Point a
t FinList n a
cs = a -> Statement
forall a. Validable a => a -> Statement
valid a
cl Statement -> Statement -> Statement
forall a. Logical a => a -> a -> a
&& N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
l FinList m a
as Point a
t a
cl FinList m a
cs' where
  (a
cl,FinList m a
cs') = FinList (m + 1) a -> (a, FinList m a)
forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
FinList (m + 1) a
cs
  vld :: Multiplicative a
    => N -> Point a -> FinList m a -> Point a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
i Point a
l FinList m a
Nil Point a
t a
cl FinList m a
Nil
    = Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
  vld N
i Point a
l (a
a:|FinList n1 a
as) Point a
t a
cl (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
a
          , a -> Statement
forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
end a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>a -> Point a
forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
cl)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N
-> Point a
-> FinList n1 a
-> Point a
-> a
-> FinList n1 a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) (a -> Point a
forall q. Oriented q => q -> Point q
start a
a) FinList n1 a
as Point a
t a
c FinList n1 a
FinList n1 a
cs 
          ]

relConePrjMlt (DiagramChainFrom Point a
l FinList m a
as) Point a
t FinList n a
cs = N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
l FinList m a
as Point a
t a
cl FinList m a
cs' where
  (a
cl,FinList m a
cs') = FinList (m + 1) a -> (a, FinList m a)
forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
FinList (m + 1) a
cs
  vld :: Multiplicative a
    => N -> Point a -> FinList m a -> Point a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld N
i Point a
l FinList m a
Nil Point a
t a
cl FinList m a
Nil
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
cl
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
t Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          ]
  vld N
i Point a
l (a
a:|FinList n1 a
as) Point a
t a
cl (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
cl
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
start a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
l)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cl Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>a -> Point a
forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
cl a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N
-> Point a
-> FinList n1 a
-> Point a
-> a
-> FinList n1 a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> FinList m a
-> Point a
-> a
-> FinList m a
-> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) (a -> Point a
forall q. Oriented q => q -> Point q
end a
a) FinList n1 a
as Point a
t a
c FinList n1 a
FinList n1 a
cs
          ]

relConePrjMlt (DiagramParallelLR Point a
p Point a
q FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
cp
        , a -> Statement
forall a. Validable a => a -> Statement
valid a
cq
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cp Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cq Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
q)Bool -> Message -> Statement
:?>N -> Message
prm N
1
        , N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
0 (Point a
pPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
q) FinList m a
as a
cp a
cq
        ] where
  (a
cp,a
cq) = FinList N2 a -> (a, a)
forall a. FinList N2 a -> (a, a)
tp2 FinList n a
FinList N2 a
cs
  vld :: Multiplicative a => N -> Orientation (Point a)
    -> FinList m a -> a -> a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
_ Orientation (Point a)
_ FinList m a
Nil a
_ a
_ = Statement
SValid
  vld N
i Orientation (Point a)
o (a
a:|FinList n1 a
as) a
cp a
cq
    = [Statement] -> Statement
And [ Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
cp a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
cq)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N -> Orientation (Point a) -> FinList n1 a -> a -> a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n1 a
as a
cp a
cq
          ]
      
relConePrjMlt (DiagramParallelRL Point a
p Point a
q FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
cp
        , a -> Statement
forall a. Validable a => a -> Statement
valid a
cq
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cp Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
cq Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
q)Bool -> Message -> Statement
:?>N -> Message
prm N
1
        , N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
0 (Point a
qPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
p) FinList m a
as a
cp a
cq
        ] where
  (a
cp,a
cq) = FinList N2 a -> (a, a)
forall a. FinList N2 a -> (a, a)
tp2 FinList n a
FinList N2 a
cs
  vld :: Multiplicative a => N -> Orientation (Point a)
    -> FinList n a -> a -> a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld N
_ Orientation (Point a)
_ FinList n a
Nil a
_ a
_ = Statement
SValid
  vld N
i Orientation (Point a)
o (a
a:|FinList n1 a
as) a
cp a
cq
    = [Statement] -> Statement
And [ Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Orientation (Point a)
o)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
cq a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
cp)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N -> Orientation (Point a) -> FinList n1 a -> a -> a -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Orientation (Point a) -> FinList m a -> a -> a -> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Orientation (Point a)
o FinList n1 a
as a
cp a
cq
          ]

relConePrjMlt (DiagramSource Point a
s FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
c0
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c0 Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
s)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
t Point a
s FinList m a
as a
c0 FinList m a
cs'
        ] where
  (a
c0,FinList m a
cs')  = FinList (m + 1) a -> (a, FinList m a)
forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
FinList (m + 1) a
cs 
  vld :: Multiplicative a => N -> Point a -> Point a
         -> FinList m a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
_ Point a
_ Point a
_ FinList m a
Nil a
_ FinList m a
Nil = Statement
SValid
  vld N
i Point a
t Point a
s (a
a:|FinList n1 a
as) a
c0 (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ Label
lS Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
start a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
s)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>a -> Point a
forall q. Oriented q => q -> Point q
end a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
c0 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N
-> Point a
-> Point a
-> FinList n1 a
-> a
-> FinList n1 a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Point a
t Point a
s FinList n1 a
as a
c0 FinList n1 a
FinList n1 a
cs
          ]

relConePrjMlt (DiagramSink Point a
e FinList m a
as) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
c0
        , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c0 Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
0
        , N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
0 Point a
t Point a
e FinList m a
as a
c0 FinList m a
cs'
        ] where
  (a
c0,FinList m a
cs') = FinList (m + 1) a -> (a, FinList m a)
forall (n :: N') a. FinList (n + 1) a -> (a, FinList n a)
ht FinList n a
FinList (m + 1) a
cs
  vld :: Multiplicative a => N -> Point a -> Point a
         -> FinList m a -> a -> FinList m a -> Statement
  vld :: forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld N
_ Point a
_ Point a
_ FinList m a
Nil a
_ FinList m a
Nil = Statement
SValid
  vld N
i Point a
t Point a
e (a
a:|FinList n1 a
as) a
c0 (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ Label
lE Label -> Statement -> Statement
:<=>: (a -> Point a
forall q. Oriented q => q -> Point q
end a
a Point a -> Point a -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
e)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>a -> Point a
forall q. Oriented q => q -> Point q
start a
a)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
c a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
c0)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N
-> Point a
-> Point a
-> FinList n1 a
-> a
-> FinList n1 a
-> Statement
forall a (m :: N').
Multiplicative a =>
N
-> Point a
-> Point a
-> FinList m a
-> a
-> FinList m a
-> Statement
vld (N -> N
forall a. Enum a => a -> a
succ N
i) Point a
t Point a
e FinList n1 a
as a
c0 FinList n1 a
FinList n1 a
cs
          ]
      
relConePrjMlt (DiagramGeneral FinList n (Point a)
ps FinList m (a, Orientation N)
aijs) Point a
t FinList n a
cs
  = [Statement] -> Statement
And [ N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO N
0 Point a
t FinList n (Point a)
ps FinList n a
cs
        , N -> Array N a -> FinList m (a, Orientation N) -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC N
0 (FinList n a -> Array N a
forall (n :: N') a. FinList n a -> Array N a
toArray FinList n a
cs) FinList m (a, Orientation N)
aijs
        ] where
  vldO :: Oriented a => N -> Point a
    -> FinList n (Point a) -> FinList n a -> Statement
  vldO :: forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO N
_ Point a
_ FinList n (Point a)
Nil FinList n a
Nil = Statement
SValid
  vldO N
i Point a
t (Point a
p:|FinList n1 (Point a)
ps) (a
c:|FinList n1 a
cs)
    = [Statement] -> Statement
And [ a -> Statement
forall a. Validable a => a -> Statement
valid a
c
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
c Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
p)Bool -> Message -> Statement
:?>N -> Message
prm N
i
          , N -> Point a -> FinList n1 (Point a) -> FinList n1 a -> Statement
forall a (n :: N').
Oriented a =>
N -> Point a -> FinList n (Point a) -> FinList n a -> Statement
vldO (N -> N
forall a. Enum a => a -> a
succ N
i) Point a
t FinList n1 (Point a)
ps FinList n1 a
FinList n1 a
cs
          ]

  vldC :: Multiplicative a => N -> Array N a
    -> FinList m (a,Orientation N) -> Statement
  vldC :: forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC N
_ Array N a
_ FinList m (a, Orientation N)
Nil = Statement
SValid
  vldC N
l Array N a
cs ((a
a,N
i:>N
j):|FinList n1 (a, Orientation N)
aijs)
    = [Statement] -> Statement
And [ Label
lB Label -> Statement -> Statement
:<=>: ((N, N) -> N -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (Array N a -> (N, N)
forall i e. Array i e -> (i, i)
bounds Array N a
cs) N
i) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
l,String
"i"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
i]
          , Label
lB Label -> Statement -> Statement
:<=>: ((N, N) -> N -> Bool
forall a. Ix a => (a, a) -> a -> Bool
inRange (Array N a -> (N, N)
forall i e. Array i e -> (i, i)
bounds Array N a
cs) N
j) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
l,String
"j"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
j]
          , Label
lO Label -> Statement -> Statement
:<=>: (a -> Orientation (Point a)
forall q. Oriented q => q -> Orientation (Point q)
orientation a
a Orientation (Point a) -> Orientation (Point a) -> Bool
forall a. Eq a => a -> a -> Bool
== a -> Point a
forall q. Oriented q => q -> Point q
end a
ci Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> a -> Point a
forall q. Oriented q => q -> Point q
end a
cj)
                     Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
l,String
"(i,j)"String -> String -> Parameter
:=(N, N) -> String
forall a. Show a => a -> String
show (N
i,N
j)]
          , Label
lC Label -> Statement -> Statement
:<=>: (a
aa -> a -> a
forall c. Multiplicative c => c -> c -> c
*a
ci a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
cj)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params[String
"l"String -> String -> Parameter
:=N -> String
forall a. Show a => a -> String
show N
l,String
"(i,j)"String -> String -> Parameter
:=(N, N) -> String
forall a. Show a => a -> String
show (N
i,N
j)]
          , N -> Array N a -> FinList n1 (a, Orientation N) -> Statement
forall a (m :: N').
Multiplicative a =>
N -> Array N a -> FinList m (a, Orientation N) -> Statement
vldC (N -> N
forall a. Enum a => a -> a
succ N
l) Array N a
cs FinList n1 (a, Orientation N)
aijs
          ] where ci :: a
ci = Array N a
cs Array N a -> N -> a
forall i e. Ix i => Array i e -> i -> e
! N
i
                  cj :: a
cj = Array N a
cs Array N a -> N -> a
forall i e. Ix i => Array i e -> i -> e
! N
j

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

-- cnDstAdjZero -


-- | adjoins a 'zero' arrow to the diagram and the cone.

cnDstAdjZero :: Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m+1) a
cnDstAdjZero :: forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
cnDstAdjZero (ConeKernel d :: Diagram ('Parallel 'LeftToRight) N2 m a
d@(DiagramParallelLR Point a
_ Point a
r FinList m a
_) a
k)
  = Diagram t n ('S m) a
-> Point a
-> FinList n a
-> Cone Mlt 'Projective Diagram t n ('S m) a
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective (Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
forall a (n :: N') (m :: N').
Distributive a =>
Diagram ('Parallel 'LeftToRight) n m a
-> Diagram ('Parallel 'LeftToRight) n (m + 1) a
dgPrlAdjZero Diagram ('Parallel 'LeftToRight) n m a
Diagram ('Parallel 'LeftToRight) N2 m a
d) Point a
t (a
ka -> FinList N1 a -> FinList (N1 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Root a -> a
forall a. Additive a => Root a -> a
zero (Point a
tPoint a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:>Point a
r)a -> FinList 'N0 a -> FinList ('N0 + 1) a
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 a
forall a. FinList 'N0 a
Nil) where t :: Point a
t = a -> Point a
forall q. Oriented q => q -> Point q
start a
k
cnDstAdjZero c :: Cone Dst p Diagram t n m a
c@(ConeCokernel Diagram ('Parallel 'RightToLeft) N2 m a
_ a
_) = Cone Mlt p Diagram t n (m + 1) a
Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m) a
cMlt where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op a (Op a)
t HomDisjEmpty Dst Op (Op a) a
f) = Variant2 'Contravariant (IsoO Dst Op) a (Op a)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  
  SDualBi (Left1 Dual1
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 m) (Op a)
c')    = HomDisjEmpty Dst Op a (Op a)
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 m) a
-> SDualBi
     (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 m) (Op a)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op a (Op a)
t (Either1
  (Dual1 (Cone Dst p Diagram t n m)) (Cone Dst p Diagram t n m) a
-> SDualBi (Cone Dst p Diagram t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone Dst p Diagram t n m a
-> Either1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m)
     (Cone Dst p Diagram t n m)
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cone Dst p Diagram t n m a
c))
  cMlt' :: Cone
  Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 (m + 1) (Op a)
cMlt'                 = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m (Op a)
-> Cone
     Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 (m + 1) (Op a)
forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
cnDstAdjZero Dual1
  (Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) N2 m) (Op a)
Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m (Op a)
c'
  SDualBi (Right1 Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m) a
cMlt) = HomDisjEmpty Dst Op (Op a) a
-> SDualBi
     (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
     (Op a)
-> SDualBi
     (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m)) a
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF HomDisjEmpty Dst Op (Op a) a
f (Either1
  (Dual1
     (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m)))
  (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
  (Op a)
-> SDualBi
     (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
     (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
  (Op a)
-> Either1
     (Dual1
        (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m)))
     (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
     (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (Cone Mlt 'Injective Diagram ('Parallel 'RightToLeft) N2 ('S m))
  (Op a)
Cone
  Mlt 'Projective Diagram ('Parallel 'LeftToRight) N2 (m + 1) (Op a)
cMlt'))

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

-- relConeDiagram -


-- | validity of a 'Diagram'-'Cone'.

relConeDiagram :: Cone s p Diagram t n m a -> Statement
relConeDiagram :: forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p Diagram t n m a -> Statement
relConeDiagram (ConeProjective Diagram t n m a
d Point a
t FinList n a
cs) = Diagram t n m a -> Point a -> FinList n a -> Statement
forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a -> Point a -> FinList n a -> Statement
relConePrjMlt Diagram t n m a
d Point a
t FinList n a
cs
relConeDiagram c :: Cone s p Diagram t n m a
c@(ConeInjective Diagram t n m a
_ Point a
_ FinList n a
_) = case Cone s p Diagram t n m a -> Dual (Dual t) :~: t
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl Cone s p Diagram t n m a
c of
  Dual (Dual t) :~: t
Refl -> Cone Mlt 'Projective Diagram (Dual t) n m (Op a) -> Statement
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p Diagram t n m a -> Statement
relConeDiagram Dual1 (Cone s p Diagram t n m) (Op a)
Cone Mlt 'Projective Diagram (Dual t) n m (Op a)
c' where
    Contravariant2 (Inv2 HomDisjEmpty Mlt Op a (Op a)
t HomDisjEmpty Mlt Op (Op a) a
_) = Variant2 'Contravariant (IsoO Mlt Op) a (Op a)
forall x.
Multiplicative x =>
Variant2 'Contravariant (IsoO Mlt Op) x (Op x)
toDualOpMlt
    SDualBi (Left1 Dual1 (Cone s p Diagram t n m) (Op a)
c') = HomDisjEmpty Mlt Op a (Op a)
-> SDualBi (Cone s p Diagram t n m) a
-> SDualBi (Cone s p Diagram t n m) (Op a)
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (p :: Perspective) x y.
(HomD s h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS HomDisjEmpty Mlt Op a (Op a)
t (Either1 (Dual1 (Cone s p Diagram t n m)) (Cone s p Diagram t n m) a
-> SDualBi (Cone s p Diagram t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone s p Diagram t n m a
-> Either1
     (Cone Mlt 'Projective Diagram (Dual t) n m)
     (Cone s p Diagram t n m)
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cone s p Diagram t n m a
c))
relConeDiagram c :: Cone s p Diagram t n m a
c@(ConeKernel Diagram ('Parallel 'LeftToRight) N2 m a
_ a
_)      = Cone Mlt p Diagram t n ('S m) a -> Statement
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p Diagram t n m a -> Statement
relConeDiagram (Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
forall (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Cone Dst p Diagram t n m a -> Cone Mlt p Diagram t n (m + 1) a
cnDstAdjZero Cone s p Diagram t n m a
Cone Dst p Diagram t n m a
c)
relConeDiagram c :: Cone s p Diagram t n m a
c@(ConeCokernel Diagram ('Parallel 'RightToLeft) N2 m a
_ a
_)    = Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m (Op a)
-> Statement
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p Diagram t n m a -> Statement
relConeDiagram Dual1 (Cone s p Diagram t n m) (Op a)
Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m (Op a)
c' where
  Contravariant2 (Inv2 HomDisjEmpty Dst Op a (Op a)
t HomDisjEmpty Dst Op (Op a) a
_) = Variant2 'Contravariant (IsoO Dst Op) a (Op a)
forall x.
Distributive x =>
Variant2 'Contravariant (IsoO Dst Op) x (Op x)
toDualOpDst
  SDualBi (Left1 Dual1 (Cone s p Diagram t n m) (Op a)
c') = HomDisjEmpty Dst Op a (Op a)
-> SDualBi (Cone s p Diagram t n m) a
-> SDualBi (Cone s p Diagram t n m) (Op a)
forall s (h :: * -> * -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') (p :: Perspective) x y.
(HomD s h, NaturalDiagrammatic h d t n m,
 NaturalDiagrammatic h d (Dual t) n m, p ~ Dual (Dual p)) =>
h x y
-> SDualBi (Cone s p d t n m) x -> SDualBi (Cone s p d t n m) y
cnMapS HomDisjEmpty Dst Op a (Op a)
t (Either1 (Dual1 (Cone s p Diagram t n m)) (Cone s p Diagram t n m) a
-> SDualBi (Cone s p Diagram t n m) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Cone s p Diagram t n m a
-> Either1
     (Cone Dst 'Projective Diagram ('Parallel 'LeftToRight) N2 m)
     (Cone s p Diagram t n m)
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Cone s p Diagram t n m a
c))

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

-- relCone -


-- | validity of a 'Cone'.

relCone :: Diagrammatic d => Cone s p d t n m a -> Statement
relCone :: forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> Statement
relCone = Cone s p Diagram t n m a -> Statement
forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p Diagram t n m a -> Statement
relConeDiagram (Cone s p Diagram t n m a -> Statement)
-> (Cone s p d t n m a -> Cone s p Diagram t n m a)
-> Cone s p d t n m a
-> Statement
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
. Cone s p d t n m a -> Cone s p Diagram t n m a
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> Cone s p Diagram t n m a
coneDiagram

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

-- Cone - Validable -


instance (Diagrammatic d, Validable (d t n m a)) => Validable (Cone s p d t n m a) where
  valid :: Cone s p d t n m a -> Statement
valid Cone s p d t n m a
c = String -> Label
Label String
"Cone" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ d t n m a -> Statement
forall a. Validable a => a -> Statement
valid (Cone s p d t n m a -> d t n m a
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject Cone s p d t n m a
c)
        , Cone s p d t n m a -> Statement
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> Statement
relCone Cone s p d t n m a
c
        ]

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

-- Cone - Parallel - Oriented -


type instance Point (Cone s p d (Parallel t) N2 m a) = Point a
instance ShowPoint a => ShowPoint (Cone s p d (Parallel t) N2 m a)
instance EqPoint a => EqPoint (Cone s p d (Parallel t) N2 m a)
instance ValidablePoint a => ValidablePoint (Cone s p d (Parallel t) N2 m a)
instance TypeablePoint a => TypeablePoint (Cone s p d (Parallel t) N2 m a)

instance ( Oriented a, Diagrammatic d, Entity (d (Parallel t) N2 m a)
         , Typeable d, Typeable s, Typeable p, Typeable t, Typeable m
         )
  => Oriented (Cone s p d (Parallel t) N2 m a) where
  orientation :: Cone s p d ('Parallel t) N2 m a
-> Orientation (Point (Cone s p d ('Parallel t) N2 m a))
orientation = Diagram ('Parallel t) N2 m a -> Orientation (Point a)
Diagram ('Parallel t) N2 m a
-> Orientation (Point (Diagram ('Parallel t) N2 m a))
forall q. Oriented q => q -> Orientation (Point q)
orientation (Diagram ('Parallel t) N2 m a -> Orientation (Point a))
-> (Cone s p d ('Parallel t) N2 m a
    -> Diagram ('Parallel t) N2 m a)
-> Cone s p d ('Parallel t) N2 m a
-> Orientation (Point 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
. d ('Parallel t) N2 m a -> Diagram ('Parallel t) N2 m a
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 ('Parallel t) N2 m a -> Diagram ('Parallel t) N2 m a)
-> (Cone s p d ('Parallel t) N2 m a -> d ('Parallel t) N2 m a)
-> Cone s p d ('Parallel t) N2 m a
-> Diagram ('Parallel t) N2 m 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
. Cone s p d ('Parallel t) N2 m a -> d ('Parallel t) N2 m a
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> d t n m a
diagrammaticObject

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

-- cnPrjOrnt -


-- | the multiplicatve projective cone on 'Orientation' with the underlying given diagram and tip

-- with the given point. 

cnPrjOrnt :: (Diagrammatic d, Entity p)
  => p -> d t n m (Orientation p) -> Cone Mlt Projective d t n m (Orientation p)
cnPrjOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
p
-> d t n m (Orientation p)
-> Cone Mlt 'Projective d t n m (Orientation p)
cnPrjOrnt p
p d t n m (Orientation p)
d = d t n m (Orientation p)
-> Point (Orientation p)
-> FinList n (Orientation p)
-> Cone Mlt 'Projective d t n m (Orientation p)
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective d t n m a
ConeProjective d t n m (Orientation p)
d p
Point (Orientation p)
p ((p -> Orientation p) -> FinList n p -> FinList n (Orientation p)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (p
pp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>) (FinList n p -> FinList n (Orientation p))
-> FinList n p -> FinList n (Orientation p)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m (Orientation p) -> FinList n p
Diagram t n m (Orientation p) -> FinList n (Point (Orientation p))
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m (Orientation p) -> FinList n p)
-> Diagram t n m (Orientation p) -> FinList n p
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m (Orientation p) -> Diagram t n m (Orientation p)
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 (Orientation p)
d)

-- | the distributive projective cone on 'Orientation' with the underlying given diagram and tip

-- with the given point. 

cnPrjDstOrnt :: (Diagrammatic d, Entity p, t ~ Parallel LeftToRight, n ~ N2)
  => p -> d t n m (Orientation p) -> Cone Dst Projective d t n m (Orientation p)
cnPrjDstOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2) =>
p
-> d t n m (Orientation p)
-> Cone Dst 'Projective d t n m (Orientation p)
cnPrjDstOrnt p
t d t n m (Orientation p)
d = d ('Parallel 'LeftToRight) N2 m (Orientation p)
-> Orientation p
-> Cone
     Dst 'Projective d ('Parallel 'LeftToRight) N2 m (Orientation p)
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) N2 m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) N2 m a
ConeKernel d t n m (Orientation p)
d ('Parallel 'LeftToRight) N2 m (Orientation p)
d (p
tp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
p) where DiagramParallelLR p
Point (Orientation p)
p Point (Orientation p)
_ FinList m (Orientation p)
_ = d t n m (Orientation p) -> Diagram t n m (Orientation p)
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 (Orientation p)
d

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

-- cnInjOrnt -


-- | the multiplicative injective cone on 'Orientation' with the underlying given diagram and tip

-- with the given point. 

cnInjOrnt :: (Diagrammatic d, Entity p)
  => p -> d t n m (Orientation p) -> Cone Mlt Injective d t n m (Orientation p)
cnInjOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
p
-> d t n m (Orientation p)
-> Cone Mlt 'Injective d t n m (Orientation p)
cnInjOrnt p
p d t n m (Orientation p)
d = d t n m (Orientation p)
-> Point (Orientation p)
-> FinList n (Orientation p)
-> Cone Mlt 'Injective d t n m (Orientation p)
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeInjective d t n m (Orientation p)
d p
Point (Orientation p)
p ((p -> Orientation p) -> FinList n p -> FinList n (Orientation p)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (p -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
p) (FinList n p -> FinList n (Orientation p))
-> FinList n p -> FinList n (Orientation p)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m (Orientation p) -> FinList n p
Diagram t n m (Orientation p) -> FinList n (Point (Orientation p))
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m (Orientation p) -> FinList n p)
-> Diagram t n m (Orientation p) -> FinList n p
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d t n m (Orientation p) -> Diagram t n m (Orientation p)
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 (Orientation p)
d)

-- | the distributive injective cone on 'Orientation' with the underlying given diagram and tip

-- with the given point. 

cnInjDstOrnt :: (Diagrammatic d, Entity p, t ~ Parallel RightToLeft, n ~ N2)
  => p -> d t n m (Orientation p) -> Cone Dst Injective d t n m (Orientation p)
cnInjDstOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2) =>
p
-> d t n m (Orientation p)
-> Cone Dst 'Injective d t n m (Orientation p)
cnInjDstOrnt p
t d t n m (Orientation p)
d = d ('Parallel 'RightToLeft) N2 m (Orientation p)
-> Orientation p
-> Cone
     Dst 'Injective d ('Parallel 'RightToLeft) N2 m (Orientation p)
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) N2 m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) N2 m a
ConeCokernel d t n m (Orientation p)
d ('Parallel 'RightToLeft) N2 m (Orientation p)
d (p
pp -> p -> Orientation p
forall p. p -> p -> Orientation p
:>p
t) where DiagramParallelRL p
Point (Orientation p)
p Point (Orientation p)
_ FinList m (Orientation p)
_ = d t n m (Orientation p) -> Diagram t n m (Orientation p)
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 (Orientation p)
d

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

-- xCnPrjOrnt -


-- | randorm variable for projecive multiplicative cones over 'Orientation'.

xCnPrjOrnt :: (Diagrammatic d, Entity p)
  => X p -> X (d t n m (Orientation p)) -> X (Cone Mlt Projective d t n m (Orientation p))
xCnPrjOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Projective d t n m (Orientation p))
xCnPrjOrnt X p
xp X (d t n m (Orientation p))
xd = do
  d t n m (Orientation p)
d <- X (d t n m (Orientation p))
xd
  p
p <- X p
xp
  Cone Mlt 'Projective d t n m (Orientation p)
-> X (Cone Mlt 'Projective d t n m (Orientation p))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (p
-> d t n m (Orientation p)
-> Cone Mlt 'Projective d t n m (Orientation p)
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
p
-> d t n m (Orientation p)
-> Cone Mlt 'Projective d t n m (Orientation p)
cnPrjOrnt p
p d t n m (Orientation p)
d)
  
instance
  ( Entity p
  , Diagrammatic d
  , XStandard p, XStandard (d t n m (Orientation p))
  )
  => XStandard (Cone Mlt Projective d t n m (Orientation p)) where
  xStandard :: X (Cone Mlt 'Projective d t n m (Orientation p))
xStandard = X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Projective d t n m (Orientation p))
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Projective d t n m (Orientation p))
xCnPrjOrnt X p
forall x. XStandard x => X x
xStandard X (d t n m (Orientation p))
forall x. XStandard x => X x
xStandard

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

-- xCnPrjDstOrnt -


-- | randorm variable for projecive distributive cones over 'Orientation',

xCnPrjDstOrnt ::
  ( Diagrammatic d
  , Entity p
  , t ~ Parallel LeftToRight, n ~ N2
  )
  => X p -> X (d t n m (Orientation p)) -> X (Cone Dst Projective d t n m (Orientation p))
xCnPrjDstOrnt :: forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Projective d t n m (Orientation p))
xCnPrjDstOrnt X p
xp X (d t n m (Orientation p))
xd = do
  d t n m (Orientation p)
d <- X (d t n m (Orientation p))
xd
  p
t <- X p
xp
  Cone Dst 'Projective d t n m (Orientation p)
-> X (Cone Dst 'Projective d t n m (Orientation p))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (p
-> d t n m (Orientation p)
-> Cone Dst 'Projective d t n m (Orientation p)
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2) =>
p
-> d t n m (Orientation p)
-> Cone Dst 'Projective d t n m (Orientation p)
cnPrjDstOrnt p
t d t n m (Orientation p)
d)

instance ( Entity p, t ~ Parallel LeftToRight, n ~ N2
         , Diagrammatic d
         , XStandard p, XStandard (d t n m (Orientation p))
         ) => XStandard (Cone Dst Projective d t n m (Orientation p)) where
  xStandard :: X (Cone Dst 'Projective d t n m (Orientation p))
xStandard = X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Projective d t n m (Orientation p))
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'LeftToRight, n ~ N2) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Projective d t n m (Orientation p))
xCnPrjDstOrnt X p
forall x. XStandard x => X x
xStandard X (d t n m (Orientation p))
forall x. XStandard x => X x
xStandard

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

-- xCnInjOrnt -


-- | randorm variable for injective multiplicative cones over 'Orientation',

xCnInjOrnt :: (Entity p, Diagrammatic d)
  => X p -> X (d t n m (Orientation p)) -> X (Cone Mlt Injective d t n m (Orientation p))
xCnInjOrnt :: forall p (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Entity p, Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Injective d t n m (Orientation p))
xCnInjOrnt X p
xp X (d t n m (Orientation p))
xd = do
  d t n m (Orientation p)
d <- X (d t n m (Orientation p))
xd
  p
p <- X p
xp
  Cone Mlt 'Injective d t n m (Orientation p)
-> X (Cone Mlt 'Injective d t n m (Orientation p))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (p
-> d t n m (Orientation p)
-> Cone Mlt 'Injective d t n m (Orientation p)
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p) =>
p
-> d t n m (Orientation p)
-> Cone Mlt 'Injective d t n m (Orientation p)
cnInjOrnt p
p d t n m (Orientation p)
d)

instance
  ( Entity p
  , Diagrammatic d
  , XStandard p, XStandard (d t n m (Orientation p))
  )
  => XStandard (Cone Mlt Injective d t n m (Orientation p)) where
  xStandard :: X (Cone Mlt 'Injective d t n m (Orientation p))
xStandard = X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Injective d t n m (Orientation p))
forall p (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Entity p, Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Mlt 'Injective d t n m (Orientation p))
xCnInjOrnt X p
forall x. XStandard x => X x
xStandard X (d t n m (Orientation p))
forall x. XStandard x => X x
xStandard

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

-- xCnInjDstOrnt -


-- | randorm variable for injective distributive cones over 'Orientation',

xCnInjDstOrnt ::(Entity p, t ~ Parallel RightToLeft, n ~ N2, Diagrammatic d)
  => X p -> X (d t n m (Orientation p)) -> X (Cone Dst Injective d t n m (Orientation p))
xCnInjDstOrnt :: forall p (t :: DiagramType) (n :: N')
       (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2, Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Injective d t n m (Orientation p))
xCnInjDstOrnt X p
xp X (d t n m (Orientation p))
xd = do
  d t n m (Orientation p)
d <- X (d t n m (Orientation p))
xd
  p
t <- X p
xp
  Cone Dst 'Injective d t n m (Orientation p)
-> X (Cone Dst 'Injective d t n m (Orientation p))
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (p
-> d t n m (Orientation p)
-> Cone Dst 'Injective d t n m (Orientation p)
forall (d :: DiagramType -> N' -> N' -> * -> *) p
       (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2) =>
p
-> d t n m (Orientation p)
-> Cone Dst 'Injective d t n m (Orientation p)
cnInjDstOrnt p
t d t n m (Orientation p)
d)
  
instance ( Entity p, t ~ Parallel RightToLeft, n ~ N2
         , Diagrammatic d
         , XStandard p, XStandard (d t n m (Orientation p))
         ) => XStandard (Cone Dst Injective d t n m (Orientation p)) where
  xStandard :: X (Cone Dst 'Injective d t n m (Orientation p))
xStandard = X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Injective d t n m (Orientation p))
forall p (t :: DiagramType) (n :: N')
       (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
(Entity p, t ~ 'Parallel 'RightToLeft, n ~ N2, Diagrammatic d) =>
X p
-> X (d t n m (Orientation p))
-> X (Cone Dst 'Injective d t n m (Orientation p))
xCnInjDstOrnt X p
forall x. XStandard x => X x
xStandard X (d t n m (Orientation p))
forall x. XStandard x => X x
xStandard