{-# LANGUAGE NoImplicitPrelude #-}

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


-- |
-- Module      : OAlg.Limes.ProductsAndSums
-- Description : products and sums
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- products and sums, i.e. limits of @'Diagram' 'Discrete'@.
module OAlg.Limes.ProductsAndSums
  (
    -- * Products
    Products, Product, ProductCone, ProductDiagram

    -- ** Construction
  , prdDiagram, prdCone
  , products, products0, products1, products2

    -- *** Orientation
  , prdConeOrnt, productOrnt, productsOrnt

    -- * Sums
  , Sums, Sum, SumCone, SumDiagram

    -- ** Duality
  , sumLimitsDuality

    -- ** Construction
  , sumDiagram, sumCone
  , sums, sums', sums0, sums1, sums2

    -- *** Orientation
  , sumConeOrnt, sumOrnt, sumsOrnt

  )
  where

import Data.Typeable

import OAlg.Prelude

import OAlg.Entity.FinList
import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.Diagram as D

import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative

import OAlg.Limes.Cone
import OAlg.Limes.Definition
import OAlg.Limes.Limits

import OAlg.Limes.TerminalAndInitialPoint
import OAlg.Limes.MinimaAndMaxima

--------------------------------------------------------------------------------
-- Product -

-- | 'Diagram' for a product.
type ProductDiagram n = Diagram Discrete n N0

-- | 'Cone' for a product.
type ProductCone n = Cone Mlt Projective Discrete n N0

-- | product as a 'Limes'.
type Product n = Limes Mlt Projective Discrete n N0

-- | products for a 'Multiplicative' structure.
type Products n = Limits Mlt Projective Discrete n N0

--------------------------------------------------------------------------------
-- prdDiagram -

-- | the underlying product diagram.
prdDiagram :: Oriented a => Diagram (Star From) (n+1) n a -> ProductDiagram n a
prdDiagram :: forall a (n :: N').
Oriented a =>
Diagram ('Star 'From) (n + 1) n a -> ProductDiagram n a
prdDiagram (DiagramSource Point a
_ FinList n a
as) = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
end FinList n a
as)

--------------------------------------------------------------------------------
-- prdCone -

-- | the product cone.
prdCone :: Multiplicative a => Diagram (Star From) (n+1) n a -> ProductCone n a
prdCone :: forall a (n :: N').
Multiplicative a =>
Diagram ('Star 'From) (n + 1) n a -> ProductCone n a
prdCone d :: Diagram ('Star 'From) (n + 1) n a
d@(DiagramSource Point a
p FinList n a
as) = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective (forall a (n :: N').
Oriented a =>
Diagram ('Star 'From) (n + 1) n a -> ProductDiagram n a
prdDiagram Diagram ('Star 'From) (n + 1) n a
d) Point a
p FinList n a
as

--------------------------------------------------------------------------------
-- products0 -

-- | products of zero points given by a terminal point.
products0 :: Multiplicative a => TerminalPoint a -> Products N0 a
products0 :: forall a. Multiplicative a => TerminalPoint a -> Products N0 a
products0 TerminalPoint a
t = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a.
Multiplicative a =>
TerminalPoint a -> ProductDiagram N0 a -> Product N0 a
prd TerminalPoint a
t) where
  prd :: Multiplicative a => TerminalPoint a -> ProductDiagram N0 a -> Product N0 a
  prd :: forall a.
Multiplicative a =>
TerminalPoint a -> ProductDiagram N0 a -> Product N0 a
prd TerminalPoint a
t d :: ProductDiagram N0 a
d@(DiagramDiscrete FinList N0 (Point a)
Nil) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective 'Discrete N0 N0 a
l Cone Mlt 'Projective 'Discrete N0 N0 a -> a
u where 
    l :: Cone Mlt 'Projective 'Discrete N0 N0 a
l = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective ProductDiagram N0 a
d (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone TerminalPoint a
t) forall a. FinList N0 a
Nil
    u :: Cone Mlt 'Projective 'Discrete N0 N0 a -> a
u (ConeProjective ProductDiagram N0 a
_ Point a
x FinList N0 a
Nil) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor TerminalPoint a
t (forall a. Multiplicative a => Point a -> TerminalCone a
trmCone Point a
x)

--------------------------------------------------------------------------------
-- products1 -

-- | products of one point, i.e. 'Minima'.
products1 :: Multiplicative a => Products N1 a
products1 :: forall a. Multiplicative a => Products N1 a
products1 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a. Multiplicative a => ProductDiagram N1 a -> Product N1 a
prd where
  prd :: Multiplicative a => ProductDiagram N1 a -> Product N1 a
  prd :: forall a. Multiplicative a => ProductDiagram N1 a -> Product N1 a
prd d :: ProductDiagram N1 a
d@(DiagramDiscrete (Point a
p:|FinList n (Point a)
Nil)) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective 'Discrete N1 N0 a
l Cone Mlt 'Projective 'Discrete N1 N0 a -> a
u where
    min :: Limes Mlt 'Projective ('Chain 'From) N1 N0 a
min = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes forall a (n :: N'). Multiplicative a => Minima 'From n a
minimaFrom (forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom Point a
p forall a. FinList N0 a
Nil)
    ConeProjective Diagram ('Chain 'From) N1 N0 a
d' Point a
t FinList N1 a
cs = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes Mlt 'Projective ('Chain 'From) N1 N0 a
min
    l :: Cone Mlt 'Projective 'Discrete N1 N0 a
l = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective ProductDiagram N1 a
d Point a
t FinList N1 a
cs
    u :: Cone Mlt 'Projective 'Discrete N1 N0 a -> a
u (ConeProjective ProductDiagram N1 a
_ Point a
t FinList N1 a
cs) = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a -> a
universalFactor Limes Mlt 'Projective ('Chain 'From) N1 N0 a
min (forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram ('Chain 'From) N1 N0 a
d' Point a
t FinList N1 a
cs) 

--------------------------------------------------------------------------------
-- products2 -

-- | products of at least two points given by products of two points.
products2 :: Multiplicative a => Products N2 a -> Products (n+2) a
products2 :: forall a (n :: N').
Multiplicative a =>
Products N2 a -> Products (n + 2) a
products2 Products N2 a
prd2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Products N2 a -> ProductDiagram n a -> Product n a
prd Products N2 a
prd2) where
  prd :: (Multiplicative a, n ~ (n'+2))
      => Products N2 a -> ProductDiagram n a -> Product n a
  prd :: forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Products N2 a -> ProductDiagram n a -> Product n a
prd Products N2 a
prd2 d :: ProductDiagram n a
d@(DiagramDiscrete (Point a
_:|Point a
_:|FinList n (Point a)
Nil))        = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Products N2 a
prd2 ProductDiagram n a
d
  prd Products N2 a
prd2 d :: ProductDiagram n a
d@(DiagramDiscrete (Point a
p0:|pN :: FinList n (Point a)
pN@(Point a
_:|Point a
_:|FinList n (Point a)
_))) = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective 'Discrete n N0 a
l Cone Mlt 'Projective 'Discrete n N0 a -> a
u where
    dN :: Diagram 'Discrete n N0 a
dN = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n (Point a)
pN
    LimesProjective Cone Mlt 'Projective 'Discrete n N0 a
Cone Mlt 'Projective 'Discrete ('S ('S n)) N0 a
lN Cone Mlt 'Projective 'Discrete n N0 a -> a
Cone Mlt 'Projective 'Discrete ('S ('S n)) N0 a -> a
uN = forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Products N2 a -> ProductDiagram n a -> Product n a
prd Products N2 a
prd2 Diagram 'Discrete n N0 a
dN
    tN :: Point a
tN = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Projective 'Discrete ('S ('S n)) N0 a
lN
    cN :: FinList ('S ('S n)) a
cN = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell Cone Mlt 'Projective 'Discrete ('S ('S n)) N0 a
lN

    d2 :: Diagram 'Discrete N2 N0 a
d2 = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (Point a
p0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|Point a
tNforall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)
    LimesProjective Cone Mlt 'Projective 'Discrete N2 N0 a
l2 Cone Mlt 'Projective 'Discrete N2 N0 a -> a
u2 = forall a (n :: N') (n' :: N').
(Multiplicative a, n ~ (n' + 2)) =>
Products N2 a -> ProductDiagram n a -> Product n a
prd Products N2 a
prd2 Diagram 'Discrete N2 N0 a
d2
    t2 :: Point a
t2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Projective 'Discrete N2 N0 a
l2
    a
l0:|a
l1:|FinList n a
Nil = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell Cone Mlt 'Projective 'Discrete N2 N0 a
l2
    
    l :: Cone Mlt 'Projective 'Discrete n N0 a
l = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective ProductDiagram n a
d Point a
t2 FinList ('S ('S n) + 1) a
ls
    ls :: FinList ('S ('S n) + 1) a
ls = a
l0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall c. Multiplicative c => c -> c -> c
*a
l1) FinList ('S ('S n)) a
cN

    u :: Cone Mlt 'Projective 'Discrete n N0 a -> a
u (ConeProjective ProductDiagram n a
_ Point a
t (a
c0:|cN :: FinList n a
cN@(a
_:|a
_:|FinList n a
_)))
      = Cone Mlt 'Projective 'Discrete N2 N0 a -> a
u2 (forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram 'Discrete N2 N0 a
d2 Point a
t (a
c0forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|a
c1forall a (p :: N'). a -> FinList p a -> FinList (p + 1) a
:|forall a. FinList N0 a
Nil)) where
        c1 :: a
c1 = Cone Mlt 'Projective 'Discrete ('S ('S n)) N0 a -> a
uN (forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram 'Discrete n N0 a
dN Point a
tN FinList n a
cN)

--------------------------------------------------------------------------------
-- products -

-- | products of @n@ points given by products of zero and two points.
products :: Multiplicative a => Products N0 a -> Products N2 a -> Products n a
products :: forall a (n :: N').
Multiplicative a =>
Products N0 a -> Products N2 a -> Products n a
products Products N0 a
prd0 Products N2 a
prd2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Multiplicative a =>
Products N0 a -> Products N2 a -> ProductDiagram n a -> Product n a
prd Products N0 a
prd0 Products N2 a
prd2) where
  prd :: Multiplicative a
      => Products N0 a -> Products N2 a -> ProductDiagram n a -> Product n a
  prd :: forall a (n :: N').
Multiplicative a =>
Products N0 a -> Products N2 a -> ProductDiagram n a -> Product n a
prd Products N0 a
prd0 Products N2 a
prd2 ProductDiagram n a
d = case ProductDiagram n a
d of
    DiagramDiscrete FinList n (Point a)
Nil       -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Products N0 a
prd0 ProductDiagram n a
d
    DiagramDiscrete (Point a
_:|FinList n (Point a)
Nil)  -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes forall a. Multiplicative a => Products N1 a
products1 ProductDiagram n a
d
    DiagramDiscrete (Point a
_:|Point a
_:|FinList n (Point a)
_) -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (forall a (n :: N').
Multiplicative a =>
Products N2 a -> Products (n + 2) a
products2 Products N2 a
prd2) ProductDiagram n a
d

--------------------------------------------------------------------------------
-- prdConeOrnt -

-- | product cone for 'Orientation'.
prdConeOrnt :: Entity p => p -> FinList n p -> ProductCone n (Orientation p)
prdConeOrnt :: forall p (n :: N').
Entity p =>
p -> FinList n p -> ProductCone n (Orientation p)
prdConeOrnt p
p FinList n p
ps = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Projective t n m (Orientation p)
cnPrjOrnt p
p (forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n p
ps)

--------------------------------------------------------------------------------
-- productOrnt -

-- | product for 'Orientation'.
productOrnt :: Entity p => p -> FinList n p -> Product n (Orientation p)
productOrnt :: forall p (n :: N').
Entity p =>
p -> FinList n p -> Product n (Orientation p)
productOrnt p
p FinList n p
ps = forall p a (t :: DiagramType) (n :: N') (m :: N').
(Entity p, a ~ Orientation p) =>
p -> Diagram t n m a -> Limes Mlt 'Projective t n m a
lmToPrjOrnt p
p (forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n p
ps)

--------------------------------------------------------------------------------
-- productsOrnt -

-- | products for 'Orientation'.
productsOrnt :: Entity p => p -> Products n (Orientation p)
productsOrnt :: forall p (n :: N'). Entity p => p -> Products n (Orientation p)
productsOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsToPrjOrnt


--------------------------------------------------------------------------------
-- Sum -

-- | 'Diagram' for a sum. 
type SumDiagram n = Diagram Discrete n N0

-- | 'Cone' for a sum.
type SumCone n = Cone Mlt Injective Discrete n N0

-- | sum as a 'Limes.
type Sum n = Limes Mlt Injective Discrete n N0

-- | sums for a 'Multiplicative' structure.
type Sums n = Limits Mlt Injective Discrete n N0

--------------------------------------------------------------------------------
-- sumDiagram -

-- | the underlying sum diagram given by a sink diagram.
sumDiagram :: Oriented a => Diagram (Star To) (n+1) n a -> SumDiagram n a
sumDiagram :: forall a (n :: N').
Oriented a =>
Diagram ('Star 'To) (n + 1) n a -> SumDiagram n a
sumDiagram (DiagramSink Point a
_ FinList n a
as) = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete (forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall q. Oriented q => q -> Point q
start FinList n a
as)

--------------------------------------------------------------------------------
-- sumCone -

-- | the sum cone given by a sink diagram.
sumCone :: Multiplicative a => Diagram (Star To) (n+1) n a -> SumCone n a
sumCone :: forall a (n :: N').
Multiplicative a =>
Diagram ('Star 'To) (n + 1) n a -> SumCone n a
sumCone d :: Diagram ('Star 'To) (n + 1) n a
d@(DiagramSink Point a
p FinList n a
as) = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective (forall a (n :: N').
Oriented a =>
Diagram ('Star 'To) (n + 1) n a -> SumDiagram n a
sumDiagram Diagram ('Star 'To) (n + 1) n a
d) Point a
p FinList n a
as

--------------------------------------------------------------------------------
-- Sum - Duality - 

-- | duality between sums and products.
sumLimitsDuality :: Multiplicative a => LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- sums0 -

-- | sums of zero points given by a initial point.
sums0 :: Multiplicative a => InitialPoint a -> Sums N0 a
sums0 :: forall a. Multiplicative a => InitialPoint a -> Sums N0 a
sums0 InitialPoint a
int = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Multiplicative a => TerminalPoint a -> Products N0 a
products0 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (f :: * -> *) (g :: * -> *) a.
LimesDuality s f g a -> f a -> g (Op a)
lmToOp forall a.
Multiplicative a =>
LimesDuality Mlt InitialPoint TerminalPoint a
intLimesDuality InitialPoint a
int

-- | sums of one point, i.e. 'Maxima'.
sums1 :: Multiplicative a => Sums N1 a
sums1 :: forall a. Multiplicative a => Sums N1 a
sums1 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a. Multiplicative a => Products N1 a
products1

-- | sums of at least two points given by sums of two points.
sums2 :: Multiplicative a => Sums N2 a -> Sums (n+2) a
sums2 :: forall a (n :: N'). Multiplicative a => Sums N2 a -> Sums (n + 2) a
sums2 Sums N2 a
sum2 = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (n :: N').
Multiplicative a =>
Products N2 a -> Products (n + 2) a
products2 forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> f a -> g (Op a)
lmsToOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Sums n) (Products n) a
sumLimitsDuality Sums N2 a
sum2

-- | sums of @n@ points given by sums of zero and two points.
sums :: Multiplicative a => Sums N0 a -> Sums N2 a -> Sums n a
sums :: forall a (n :: N').
Multiplicative a =>
Sums N0 a -> Sums N2 a -> Sums n a
sums Sums N0 a
sum0 Sums N2 a
sum2 = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits (forall a (n :: N').
Multiplicative a =>
Sums N0 a -> Sums N2 a -> SumDiagram n a -> Sum n a
sum Sums N0 a
sum0 Sums N2 a
sum2) where
  sum :: Multiplicative a
      => Sums N0 a -> Sums N2 a -> SumDiagram n a -> Sum n a
  sum :: forall a (n :: N').
Multiplicative a =>
Sums N0 a -> Sums N2 a -> SumDiagram n a -> Sum n a
sum Sums N0 a
sum0 Sums N2 a
sum2 SumDiagram n a
d = case SumDiagram n a
d of
    DiagramDiscrete FinList n (Point a)
Nil       -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Sums N0 a
sum0 SumDiagram n a
d
    DiagramDiscrete (Point a
_:|FinList n (Point a)
Nil)  -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes forall a. Multiplicative a => Sums N1 a
sums1 SumDiagram n a
d
    DiagramDiscrete (Point a
_:|Point a
_:|FinList n (Point a)
_) -> forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes (forall a (n :: N'). Multiplicative a => Sums N2 a -> Sums (n + 2) a
sums2 Sums N2 a
sum2) SumDiagram n a
d 

-- | sums given by a proxy type for @n@.
sums' :: Multiplicative a => p n -> Sums N0 a -> Sums N2 a -> Sums n a
sums' :: forall a (p :: N' -> *) (n :: N').
Multiplicative a =>
p n -> Sums N0 a -> Sums N2 a -> Sums n a
sums' p n
_ = forall a (n :: N').
Multiplicative a =>
Sums N0 a -> Sums N2 a -> Sums n a
sums

--------------------------------------------------------------------------------
-- sumConeOrnt -

-- | sum cone for 'Orientation'.
sumConeOrnt :: Entity p => p -> FinList n p -> SumCone n (Orientation p)
sumConeOrnt :: forall p (n :: N').
Entity p =>
p -> FinList n p -> SumCone n (Orientation p)
sumConeOrnt p
p FinList n p
ps = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p
-> Diagram t n m (Orientation p)
-> Cone Mlt 'Injective t n m (Orientation p)
cnInjOrnt p
p (forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n p
ps)

--------------------------------------------------------------------------------
-- sumOrnt -

-- | sum for 'Orientation'.
sumOrnt :: Entity p => p -> FinList n p -> Sum n (Orientation p)
sumOrnt :: forall p (n :: N').
Entity p =>
p -> FinList n p -> Sum n (Orientation p)
sumOrnt p
p FinList n p
ps = forall p a (t :: DiagramType) (n :: N') (m :: N').
(Entity p, a ~ Orientation p) =>
p -> Diagram t n m a -> Limes Mlt 'Injective t n m a
lmFromInjOrnt p
p (forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n p
ps)
  
--------------------------------------------------------------------------------
-- sumsOnt -

-- | sums for 'Orientation'.
sumsOrnt :: Entity p => p -> Sums n (Orientation p)
sumsOrnt :: forall p (n :: N'). Entity p => p -> Sums n (Orientation p)
sumsOrnt = forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsFromInjOrnt