{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Cone.Core

-- Description : basic definitions for cones

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

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

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

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

import Data.Typeable

import OAlg.Prelude

import OAlg.Category.NaturalTransformable

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.Limes.Perspective

import OAlg.Limes.Cone.Structure

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

-- Cone -


-- | cone over a diagram.

--

-- __Properties__ Let @c@ be in @'Cone' __s__ __p__ __d__ __t__ __n__ __m__ __a__@ for a

-- 'Diagrammatic' @__d__@, then holds:

--

-- (1) If @c@ matches @'ConeProjective' d t cs@ for a 'Multiplicative' structure __@a@__

-- then holds:

--

--     (1) For all @ci@ in @cs@ holds: @'start' ci '==' t@ and

--     @'end' ci '==' pi@ where @pi@ in @'dgPoints' ('diagram' d)@.

--

--     (2) For all @aij@ in @'dgArrows' ('diagram' d)@ holds: @aij 'Mlt.*' ci '==' cj@

--     where @ci@, @cj@ in @cs@.

--

-- (2) If @c@ matches @'ConeInjective' d t cs@ for a 'Multiplicative' structure __@a@__

-- then holds: 

--

--     (1) For all @ci@ in @cs@ holds: @'end' ci '==' t@ and

--     @'start' ci '==' pi@ where @pi@ in @'dgPoints' ('diagram' d)@.

--

--     (2) For all @aij@ in @'dgArrows' ('diagram' d)@ holds: @cj 'Mlt.*' aij '==' ci@

--     where @ci@, @cj@ in @cs@.

--

-- (3) If @c@ matches @'ConeKernel' p k@ for a 'Distributive' structure __@a@__ then holds:

--

--     (1) @'end' k '==' p0@ where @p0@ in @'dgPoints' ('diagram' p)@

--

--     (2) For all @a@ in @'dgArrows' ('diagram' p)@ holds: @a 'Mlt.*' k '==' 'zero' (t ':>' p1)@

--     where @t = 'start' k@ and @p0@, @p1@ in @'dgPoints' ('diagram' p)@.

--

-- (4) If @c@ matches @'ConeCokernel' p k@ for a 'Distributive' structure __@a@__ then

-- holds:

--

--     (1) @'start' k '==' p0@ where @p0@ in @'dgPoints' ('diagram' p)@

--

--     (2) For all @a@ in @'dgArrows' ('diagram' p)@ holds: @k 'Mlt.*' a '==' 'zero' (p1 ':>' t)@

--     where @t = 'end' k@ and @p0@, @p1@ in @'dgPoints' ('diagram' p)@.

--

-- __Note__

--

-- (1) Let @'OAlg.Hom.Multiplicative.HomMultiplicativeDisjunctive' __h__@ and

-- @'NaturalDiagrammatic' __h d t n m__@,then holds:

-- @'NaturalTransformable' __h__ (->) ('DiagramG' __d t n m__) ('Diagram' __t n m__)@

-- (as required by the definition of @'NaturalDiagrammatic' __h d t n m__@)

-- and

-- @'NaturalTransformable' __h__ (->) ('Cone' 'Mlt' __p d t n m__) ('DiagramG' __d t n m__)@

-- (see comment in source code of its instance declaration and the property of 'dmap')

-- and therefore this establish a natural

-- transformation according to @__h__@ from @'Cone' 'Mlt' __p d t n m__@ to @'Diagram' __t n m__@.

--

-- (2) The same holds for @'OAlg.Hom.Multiplicative.HomMultiplicativeDisjunctive' __h__@ and

-- @'Cone' 'Dst' __p d t n m__@.

data Cone s (p :: Perspective) d (t :: DiagramType) (n :: N') (m :: N') a where
  ConeProjective :: Multiplicative a
    => d t n m a -> Point a -> FinList n a -> Cone Mlt Projective d t n m a
  ConeInjective  :: Multiplicative a
    => d t n m a -> Point a -> FinList n a -> Cone Mlt Injective d t n m a
  ConeKernel     :: Distributive a
    => d (Parallel LeftToRight) N2 m a -> a
    -> Cone Dst Projective d (Parallel LeftToRight)  N2 m a
  ConeCokernel   :: Distributive a
    => d (Parallel RightToLeft) N2 m a -> a
    -> Cone Dst Injective d (Parallel RightToLeft) N2 m a

deriving instance Show (d t n m a) => Show (Cone s p d t n m a)
deriving instance Eq (d t n m a) => Eq (Cone s p d t n m a)

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

-- coneStruct -


-- | the associated 'ConeStruct'.

coneStruct :: Cone s p d t n m a -> ConeStruct s a
coneStruct :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> ConeStruct s a
coneStruct (ConeProjective d t n m a
_ Point a
_ FinList n a
_) = ConeStruct s a
ConeStruct Mlt a
forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt
coneStruct (ConeInjective d t n m a
_ Point a
_ FinList n a
_)  = ConeStruct s a
ConeStruct Mlt a
forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt
coneStruct (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
_ a
_)       = ConeStruct s a
ConeStruct Dst a
forall a. Distributive a => ConeStruct Dst a
ConeStructDst
coneStruct (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
_ a
_)     = ConeStruct s a
ConeStruct Dst a
forall a. Distributive a => ConeStruct Dst a
ConeStructDst

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

-- cnMltOrDst -


-- | proof of @__s__@ being either 'Mlt' or 'Dst'.

cnMltOrDst :: Cone s p d t n m a -> Either (s :~: Mlt) (s :~: Dst)
cnMltOrDst :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Either (s :~: Mlt) (s :~: Dst)
cnMltOrDst = ConeStruct s a -> Either (s :~: Mlt) (s :~: Dst)
forall s a. ConeStruct s a -> Either (s :~: Mlt) (s :~: Dst)
cnStructMltOrDst (ConeStruct s a -> Either (s :~: Mlt) (s :~: Dst))
-> (Cone s p d t n m a -> ConeStruct s a)
-> Cone s p d t n m a
-> Either (s :~: Mlt) (s :~: Dst)
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 -> ConeStruct s a
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> ConeStruct s a
coneStruct

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

-- diagrammaticObject -


-- | the underlying 'Diagrammatic' object.

diagrammaticObject :: Cone s p d t n m a -> d t n m a
diagrammaticObject :: 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 (ConeProjective d t n m a
d Point a
_ FinList n a
_) = d t n m a
d
diagrammaticObject (ConeInjective d t n m a
d Point a
_ FinList n a
_)  = d t n m a
d
diagrammaticObject (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
d a
_)       = d t n m a
d ('Parallel 'LeftToRight) ('S N1) m a
d
diagrammaticObject (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
d a
_)     = d t n m a
d ('Parallel 'RightToLeft) ('S N1) m a
d

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

-- cdroh -


-- | the diagrammatic object as generalized diagram.

cdroh :: Cone s p d t n m x -> DiagramG d t n m x
cdroh :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Cone s p d t n m x -> DiagramG d t n m x
cdroh = 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 -> DiagramG d t n m x)
-> (Cone s p d t n m x -> d t n m x)
-> Cone s p d t n m x
-> DiagramG d t n m 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
. Cone s p d t n m x -> d t n m x
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

instance Natural r (->) (Cone s p d t n m) (DiagramG d t n m) where
  roh :: forall x. Struct r x -> Cone s p d t n m x -> DiagramG d t n m x
roh Struct r x
_ = Cone s p d t n m x -> DiagramG d t n m x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Cone s p d t n m x -> DiagramG d t n m x
cdroh

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

-- cnDiagramTypeRefl -


-- | reflexivity of the underlying diagram type.

cnDiagramTypeRefl :: Diagrammatic d => Cone s p d t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl :: 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 = Diagram t n m a -> Dual (Dual t) :~: t
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> Dual (Dual t) :~: t
dgTypeRefl (Diagram t n m a -> Dual (Dual t) :~: t)
-> (Cone s p d t n m a -> Diagram t n m a)
-> Cone s p d t n m a
-> Dual (Dual t) :~: t
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 t n m a -> Diagram t n 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 t n m a -> Diagram t n m a)
-> (Cone s p d t n m a -> d t n m a)
-> Cone s p d t n m a
-> Diagram t n 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 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

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

-- cnTypeRefl -


cnTypeRefl :: Cone s p d t n m a -> Dual (Dual p) :~: p
cnTypeRefl :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Dual (Dual p) :~: p
cnTypeRefl (ConeProjective d t n m a
_ Point a
_ FinList n a
_) = p :~: p
Dual (Dual p) :~: p
forall {k} (a :: k). a :~: a
Refl
cnTypeRefl (ConeInjective d t n m a
_ Point a
_ FinList n a
_)  = p :~: p
Dual (Dual p) :~: p
forall {k} (a :: k). a :~: a
Refl
cnTypeRefl (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
_ a
_)       = p :~: p
Dual (Dual p) :~: p
forall {k} (a :: k). a :~: a
Refl
cnTypeRefl (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
_ a
_)     = p :~: p
Dual (Dual p) :~: p
forall {k} (a :: k). a :~: a
Refl

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

-- coneDiagram -


-- | mapping a 'Diagrammatic'-'Cone' to a 'Diagram'-'Cone'.

coneDiagram :: Diagrammatic d => Cone s p d t n m a -> Cone s p Diagram t n m a
coneDiagram :: 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 (ConeProjective d t n m a
d Point a
t FinList n a
s) = Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective Diagram t n 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 (d t n m a -> Diagram t n 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 t n m a
d) Point a
t FinList n a
s
coneDiagram (ConeInjective d t n m a
d Point a
t FinList n a
s)  = Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective Diagram t n 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 'Injective d t n m a
ConeInjective (d t n m a -> Diagram t n 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 t n m a
d) Point a
t FinList n a
s
coneDiagram (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
d a
k)       = Diagram ('Parallel 'LeftToRight) ('S N1) m a
-> a
-> Cone
     Dst 'Projective Diagram ('Parallel 'LeftToRight) ('S N1) m a
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'LeftToRight) ('S N1) m a
-> a -> Cone Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) m a
ConeKernel (d ('Parallel 'LeftToRight) ('S N1) m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) 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 'LeftToRight) ('S N1) m a
d) a
k
coneDiagram (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
d a
k)     = Diagram ('Parallel 'RightToLeft) ('S N1) m a
-> a
-> Cone Dst 'Injective Diagram ('Parallel 'RightToLeft) ('S N1) m a
forall a (d :: DiagramType -> N' -> N' -> * -> *) (m :: N').
Distributive a =>
d ('Parallel 'RightToLeft) ('S N1) m a
-> a -> Cone Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) m a
ConeCokernel (d ('Parallel 'RightToLeft) ('S N1) m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) 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 'RightToLeft) ('S N1) m a
d) a
k

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

-- tip -


-- | the tip of a cone.

--

-- __Property__ Let @c@ be in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ for a

-- 'Oriented' structure then holds:

--

-- (1) If __@p@__ is equal to __'Projective'__ then holds:

-- @'start' ci '==' 'tip' c@ for all @ci@ in @'shell' c@.

--

-- (2) If __@p@__ is equal to __'Injective'__ then holds:

-- @'end' ci '==' 'tip' c@ for all @ci@ in @'shell' c@.

tip :: Cone s p d t n m a -> Point a
tip :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone s p d t n m a
c = case Cone s p d t n m a
c of
  ConeProjective d t n m a
_ Point a
t FinList n a
_ -> Point a
t
  ConeInjective d t n m a
_ Point a
t FinList n a
_  -> Point a
t
  ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
_ a
k       -> a -> Point a
forall q. Oriented q => q -> Point q
start a
k
  ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
_ a
k     -> a -> Point a
forall q. Oriented q => q -> Point q
end a
k

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

-- shell -


-- | the shell of a cone.

--

-- __Property__ Let @c@ be in @'Cone' __s__ __p__ __t__ __n__ __m__ __a__@ for a

-- 'Oriented' structure then holds:

--

-- (1) If __@p@__ is equal to __'Projective'__ then holds:

-- @'amap' 'end' ('shell' c) '==' 'cnPoints' c@.

--

-- (2) If __@p@__ is equal to __'Injective'__ then holds:

-- @'amap' 'start' ('shell' c) '==' 'cnPoints' c@.

shell :: Diagrammatic d => Cone s p d t n m a -> FinList n a
shell :: 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 -> FinList n a
shell (ConeProjective d t n m a
_ Point a
_ FinList n a
as) = FinList n a
as
shell (ConeInjective d t n m a
_ Point a
_ FinList n a
as)  = FinList n a
as
shell (ConeKernel d ('Parallel 'LeftToRight) ('S N1) m a
d a
k)        = 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 (a -> Point a
forall q. Oriented q => q -> Point q
start a
k Point a -> Point a -> Orientation (Point a)
forall p. p -> p -> Orientation p
:> Point a
q)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 DiagramParallelLR Point a
_ Point a
q FinList m a
_ = d ('Parallel 'LeftToRight) ('S N1) m a
-> Diagram ('Parallel 'LeftToRight) ('S N1) 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 'LeftToRight) ('S N1) m a
d
shell (ConeCokernel d ('Parallel 'RightToLeft) ('S N1) m a
d a
k)      = 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
q 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
k)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 DiagramParallelRL Point a
_ Point a
q FinList m a
_ = d ('Parallel 'RightToLeft) ('S N1) m a
-> Diagram ('Parallel 'RightToLeft) ('S N1) 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 'RightToLeft) ('S N1) m a
d

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

-- cnPoints -


-- | the points of the underlying diagram.

cnPoints :: (Diagrammatic d, Oriented a) => Cone s p d t n m a -> FinList n (Point a)
cnPoints :: forall (d :: DiagramType -> N' -> N' -> * -> *) a s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N').
(Diagrammatic d, Oriented a) =>
Cone s p d t n m a -> FinList n (Point a)
cnPoints = Diagram t n m a -> FinList n (Point a)
forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints (Diagram t n m a -> FinList n (Point a))
-> (Cone s p d t n m a -> Diagram t n m a)
-> Cone s p d t n m a
-> FinList n (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
. Cone s p Diagram t n m a -> Diagram 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 Diagram t n m a -> Diagram t n m a)
-> (Cone s p d t n m a -> Cone s p Diagram t n m a)
-> Cone s p d t n m a
-> Diagram t n 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 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

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

-- cnArrows -


-- | the arrows of the underlying diagram.

cnArrows :: Diagrammatic d => Cone s p d t n m a -> FinList m a
cnArrows :: 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 -> FinList m a
cnArrows = Diagram t n m a -> FinList m a
forall (t :: DiagramType) (n :: N') (m :: N') a.
Diagram t n m a -> FinList m a
dgArrows (Diagram t n m a -> FinList m a)
-> (Cone s p d t n m a -> Diagram t n m a)
-> Cone s p d t n m a
-> FinList 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 Diagram t n m a -> Diagram 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 Diagram t n m a -> Diagram t n m a)
-> (Cone s p d t n m a -> Cone s p Diagram t n m a)
-> Cone s p d t n m a
-> Diagram t n 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 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