{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- 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, ProductsG
  , Product, ProductG
  , ProductCone, ProductConic
  , ProductDiagram, ProductDiagrammatic

    -- ** Construction

  , prdDiagram, prdCone
  , products, products0, products1, products2

    -- *** Orientation

  , prdConeOrnt, productOrnt, productsOrnt

    -- * Sums

  , Sums, SumsG
  , Sum, SumG
  , SumCone, SumConic
  , SumDiagram, SumDiagrammatic

    -- ** Duality

  , DualisableGDiscrete
  , coProducts, coProductsG

    -- ** Construction

  , sumDiagram, sumCone
  , sums, sums', sums0, sums1, sums2

    -- *** Orientation

  , sumConeOrnt, sumOrnt, sumsOrnt
  )
  where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Either
import OAlg.Data.Variant

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.Hom.Definition
import OAlg.Hom.Multiplicative

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

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

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

-- Product -


-- | 'Diagrammatic' object for a product.

type ProductDiagrammatic d (n :: N') = d Discrete n N0 :: Type -> Type

-- | 'Diagram' for a product.

type ProductDiagram n = ProductDiagrammatic Diagram n

-- | 'Conic' object for a product.

type ProductConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Projective d Discrete n N0 :: Type -> Type

-- | 'Cone' for a product.

type ProductCone n = ProductConic Cone Diagram n

-- | generic product as a 'LimesG'.

type ProductG c d n = LimesG c Mlt Projective d Discrete (n :: N') N0

-- | product as a 'Limes'.

type Product n = ProductG Cone Diagram n

-- | generic products for a 'Multiplicative' structure.

type ProductsG c d n = LimitsG c Mlt Projective d Discrete (n :: N') N0

-- | products for a 'Multiplicative' structure.

type Products n = ProductsG Cone Diagram n

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

-- prdDiagram -


-- | the underlying product diagram.

prdDiagram :: (Oriented x, Diagrammatic d)
  => d (Star From) (n+1) n x -> ProductDiagram n x
prdDiagram :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Oriented x, Diagrammatic d) =>
d ('Star 'From) (n + 1) n x -> ProductDiagram n x
prdDiagram d ('Star 'From) (n + 1) n x
d = FinList n (Point x) -> Diagram 'Discrete n 'N0 x
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete ((x -> Point x) -> FinList n x -> FinList n (Point x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 x -> Point x
forall q. Oriented q => q -> Point q
end FinList n x
as) where DiagramSource Point x
_ FinList n x
as = d ('Star 'From) ('S n) n x -> Diagram ('Star 'From) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Star 'From) (n + 1) n x
d ('Star 'From) ('S n) n x
d 

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

-- prdCone -


-- | the product cone.

prdCone :: (Multiplicative x, Diagrammatic d)
  => d (Star From) (n+1) n x -> ProductCone n x
prdCone :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
d ('Star 'From) (n + 1) n x -> ProductCone n x
prdCone d ('Star 'From) (n + 1) n x
d = Diagram 'Discrete n 'N0 x
-> Point x
-> FinList n x
-> Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
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 ('Star 'From) (n + 1) n x -> Diagram 'Discrete n 'N0 x
forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Oriented x, Diagrammatic d) =>
d ('Star 'From) (n + 1) n x -> ProductDiagram n x
prdDiagram d ('Star 'From) (n + 1) n x
d) Point x
p FinList n x
as where DiagramSource Point x
p FinList n x
as = d ('Star 'From) ('S n) n x -> Diagram ('Star 'From) ('S n) n x
forall (t :: DiagramType) (n :: N') (m :: N') x.
d t n m x -> Diagram t n m x
forall (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Diagrammatic d =>
d t n m x -> Diagram t n m x
diagram d ('Star 'From) (n + 1) n x
d ('Star 'From) ('S n) n x
d

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

-- products0 -


-- | products of zero points given by a terminal point.

products0 :: Multiplicative x => TerminalPoint x -> Products N0 x
products0 :: forall x. Multiplicative x => TerminalPoint x -> Products 'N0 x
products0 TerminalPoint x
t = (Diagram 'Discrete 'N0 'N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x)
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (TerminalPoint x
-> Diagram 'Discrete 'N0 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
forall x.
Multiplicative x =>
TerminalPoint x -> ProductDiagram 'N0 x -> Product 'N0 x
prd TerminalPoint x
t) where
  prd :: Multiplicative x => TerminalPoint x -> ProductDiagram N0 x -> Product N0 x
  prd :: forall x.
Multiplicative x =>
TerminalPoint x -> ProductDiagram 'N0 x -> Product 'N0 x
prd TerminalPoint x
t d :: ProductDiagram 'N0 x
d@(DiagramDiscrete FinList 'N0 (Point x)
Nil) = Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
-> (Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x -> x)
-> LimesG Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
l Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x -> x
u where 
    l :: Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
l = ProductDiagram 'N0 x
-> Point x
-> FinList 'N0 x
-> Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x
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 ProductDiagram 'N0 x
d (Cone Mlt 'Projective Diagram 'Empty 'N0 'N0 x -> Point x
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 Mlt 'Projective Diagram 'Empty 'N0 'N0 x -> Point x)
-> Cone Mlt 'Projective Diagram 'Empty 'N0 'N0 x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ TerminalPoint x -> Cone Mlt 'Projective Diagram 'Empty 'N0 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone TerminalPoint x
t) FinList 'N0 x
forall a. FinList 'N0 a
Nil
    u :: Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0 x -> x
u (ConeProjective ProductDiagram 'N0 x
_ Point x
x FinList 'N0 x
Nil) = TerminalPoint x
-> Cone Mlt 'Projective Diagram 'Empty 'N0 'N0 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor TerminalPoint x
t (Point x -> Cone Mlt 'Projective Diagram 'Empty 'N0 'N0 x
forall x. Multiplicative x => Point x -> TerminalCone x
trmCone Point x
x)

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

-- products1 -


-- | products of one point, i.e. 'Minima'.

products1 :: Multiplicative x => Products N1 x
products1 :: forall x. Multiplicative x => Products N1 x
products1 = (Diagram 'Discrete N1 'N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x)
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG Diagram 'Discrete N1 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
forall x. Multiplicative x => ProductDiagram N1 x -> Product N1 x
prd where
  prd :: Multiplicative x => ProductDiagram N1 x -> Product N1 x
  prd :: forall x. Multiplicative x => ProductDiagram N1 x -> Product N1 x
prd d :: ProductDiagram N1 x
d@(DiagramDiscrete (Point x
p:|FinList n1 (Point x)
Nil)) = Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
-> (Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x -> x)
-> LimesG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
l Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x -> x
u where
    min :: LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
min = LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
-> Diagram ('Chain 'From) N1 'N0 x
-> LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Minima 'From 'N0 x
LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
forall x (n :: N'). Multiplicative x => Minima 'From n x
minimaFrom (Point x -> FinList 'N0 x -> Diagram ('Chain 'From) ('N0 + 1) 'N0 x
forall a (m :: N').
Point a -> FinList m a -> Diagram ('Chain 'From) (m + 1) m a
DiagramChainFrom Point x
p FinList 'N0 x
forall a. FinList 'N0 a
Nil)
    ConeProjective Diagram ('Chain 'From) N1 'N0 x
d' Point x
t FinList N1 x
cs = LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
-> Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> c s p d t n m x
universalCone LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
min
    l :: Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
l = ProductDiagram N1 x
-> Point x
-> FinList N1 x
-> Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x
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 ProductDiagram N1 x
d Point x
t FinList N1 x
cs
    u :: Cone Mlt 'Projective Diagram 'Discrete N1 'N0 x -> x
u (ConeProjective ProductDiagram N1 x
_ Point x
t FinList N1 x
cs) = LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
-> Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x -> x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimesG c s p d t n m x -> Cone s p d t n m x -> x
universalFactor LimesG Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
min (Diagram ('Chain 'From) N1 'N0 x
-> Point x
-> FinList N1 x
-> Cone Mlt 'Projective Diagram ('Chain 'From) N1 'N0 x
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 ('Chain 'From) N1 'N0 x
d' Point x
t FinList N1 x
cs) 

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

-- products2 -


-- | products of at least two points given by products of two points.

products2 :: Multiplicative x => Products N2 x -> Products (n+2) x
products2 :: forall x (n :: N').
Multiplicative x =>
Products N2 x -> Products (n + 2) x
products2 Products N2 x
prd2 = (Diagram 'Discrete ('S ('S n)) 'N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Discrete ('S ('S n)) 'N0 x)
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete ('S ('S n)) 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Products N2 x
-> Diagram 'Discrete ('S ('S n)) 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete ('S ('S n)) 'N0 x
forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Products N2 x -> ProductDiagram n x -> Product n x
prd Products N2 x
prd2) where
  prd :: (Multiplicative x, n ~ (n'+2))
      => Products N2 x -> ProductDiagram n x -> Product n x
  prd :: forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Products N2 x -> ProductDiagram n x -> Product n x
prd Products N2 x
prd2 d :: ProductDiagram n x
d@(DiagramDiscrete (Point x
_:|Point x
_:|FinList n1 (Point x)
Nil))        = LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
-> ProductDiagram n x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
Products N2 x
prd2 ProductDiagram n x
d
  prd Products N2 x
prd2 d :: ProductDiagram n x
d@(DiagramDiscrete (Point x
p0:|pN :: FinList n1 (Point x)
pN@(Point x
_:|Point x
_:|FinList n1 (Point x)
_))) = Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
-> (Cone Mlt 'Projective Diagram 'Discrete n 'N0 x -> x)
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Projective d t n m x
-> (Cone s 'Projective d t n m x -> x)
-> LimesG c s 'Projective d t n m x
LimesProjective Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
l Cone Mlt 'Projective Diagram 'Discrete n 'N0 x -> x
u where
    dN :: Diagram 'Discrete n1 'N0 x
dN = FinList n1 (Point x) -> Diagram 'Discrete n1 'N0 x
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n1 (Point x)
pN
    LimesProjective Cone Mlt 'Projective Diagram 'Discrete n1 'N0 x
Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x
lN Cone Mlt 'Projective Diagram 'Discrete n1 'N0 x -> x
Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x -> x
uN = Products N2 x
-> Diagram 'Discrete n1 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n1 'N0 x
forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Products N2 x -> ProductDiagram n x -> Product n x
prd Products N2 x
prd2 Diagram 'Discrete n1 'N0 x
dN
    tN :: Point x
tN = Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x
-> Point x
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 Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x
lN
    cN :: FinList ('S ('S n1)) x
cN = Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x
-> FinList ('S ('S n1)) x
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 Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x
lN

    d2 :: Diagram 'Discrete N2 'N0 x
d2 = FinList N2 (Point x) -> Diagram 'Discrete N2 'N0 x
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete (Point x
p0Point x -> FinList N1 (Point x) -> FinList (N1 + 1) (Point x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|Point x
tNPoint x -> FinList 'N0 (Point x) -> FinList ('N0 + 1) (Point x)
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 (Point x)
forall a. FinList 'N0 a
Nil)
    LimesProjective Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
l2 Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> x
u2 = Products N2 x
-> Diagram 'Discrete N2 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
forall x (n :: N') (n' :: N').
(Multiplicative x, n ~ (n' + 2)) =>
Products N2 x -> ProductDiagram n x -> Product n x
prd Products N2 x
prd2 Diagram 'Discrete N2 'N0 x
d2
    t2 :: Point x
t2 = Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> Point x
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 Mlt 'Projective Diagram 'Discrete N2 'N0 x
l2
    x
l0:|x
l1:|FinList n1 x
Nil = Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> FinList N2 x
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 Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
l2
    
    l :: Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
l = ProductDiagram n x
-> Point x
-> FinList n x
-> Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
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 ProductDiagram n x
d Point x
t2 FinList n x
FinList ('S ('S n1) + 1) x
ls
    ls :: FinList ('S ('S n1) + 1) x
ls = x
l0x -> FinList ('S ('S n1)) x -> FinList ('S ('S n1) + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|(x -> x) -> FinList ('S ('S n1)) x -> FinList ('S ('S n1)) x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (x -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
l1) FinList ('S ('S n1)) x
cN

    u :: Cone Mlt 'Projective Diagram 'Discrete n 'N0 x -> x
u (ConeProjective ProductDiagram n x
_ Point x
t (x
c0:|cN :: FinList n1 x
cN@(x
_:|x
_:|FinList n1 x
_)))
      = Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x -> x
u2 (Diagram 'Discrete N2 'N0 x
-> Point x
-> FinList N2 x
-> Cone Mlt 'Projective Diagram 'Discrete N2 'N0 x
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 'Discrete N2 'N0 x
d2 Point x
t (x
c0x -> FinList N1 x -> FinList (N1 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|x
c1x -> FinList 'N0 x -> FinList ('N0 + 1) x
forall a (n1 :: N'). a -> FinList n1 a -> FinList (n1 + 1) a
:|FinList 'N0 x
forall a. FinList 'N0 a
Nil)) where
        c1 :: x
c1 = Cone Mlt 'Projective Diagram 'Discrete n1 'N0 x -> x
Cone Mlt 'Projective Diagram 'Discrete ('S ('S n1)) 'N0 x -> x
uN (Diagram 'Discrete n1 'N0 x
-> Point x
-> FinList n1 x
-> Cone Mlt 'Projective Diagram 'Discrete n1 'N0 x
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 'Discrete n1 'N0 x
dN Point x
tN FinList n1 x
FinList n1 x
cN)

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

-- products -


-- | products of @n@ points given by products of zero and two points.

products :: Multiplicative x => Products N0 x -> Products N2 x -> Products n x
products :: forall x (n :: N').
Multiplicative x =>
Products 'N0 x -> Products N2 x -> Products n x
products Products 'N0 x
prd0 Products N2 x
prd2 = (Diagram 'Discrete n 'N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x)
-> LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Products 'N0 x
-> Products N2 x
-> Diagram 'Discrete n 'N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
forall x (n :: N').
Multiplicative x =>
Products 'N0 x
-> Products N2 x -> ProductDiagram n x -> Product n x
prd Products 'N0 x
prd0 Products N2 x
prd2) where
  prd :: Multiplicative x
      => Products N0 x -> Products N2 x -> ProductDiagram n x -> Product n x
  prd :: forall x (n :: N').
Multiplicative x =>
Products 'N0 x
-> Products N2 x -> ProductDiagram n x -> Product n x
prd Products 'N0 x
prd0 Products N2 x
prd2 ProductDiagram n x
d = case ProductDiagram n x
d of
    DiagramDiscrete FinList n (Point x)
Nil       -> LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
-> ProductDiagram n x -> Product n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
Products 'N0 x
prd0 ProductDiagram n x
d
    DiagramDiscrete (Point x
_:|FinList n1 (Point x)
Nil)  -> LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
-> ProductDiagram n x -> Product n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
Products N1 x
forall x. Multiplicative x => Products N1 x
products1 ProductDiagram n x
d
    DiagramDiscrete (Point x
_:|Point x
_:|FinList n1 (Point x)
_) -> LimitsG Cone Mlt 'Projective Diagram 'Discrete n 'N0 x
-> ProductDiagram n x -> Product n x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (Products N2 x -> Products (n1 + 2) x
forall x (n :: N').
Multiplicative x =>
Products N2 x -> Products (n + 2) x
products2 Products N2 x
prd2) ProductDiagram n x
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 = p
-> Diagram 'Discrete n 'N0 (Orientation p)
-> Cone Mlt 'Projective Diagram 'Discrete n 'N0 (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 (FinList n (Point (Orientation p))
-> Diagram 'Discrete n 'N0 (Orientation p)
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n p
FinList n (Point (Orientation 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 = p
-> Diagram 'Discrete n 'N0 (Orientation p)
-> Product n (Orientation p)
forall p x (t :: DiagramType) (n :: N') (m :: N').
(Entity p, x ~ Orientation p) =>
p -> Diagram t n m x -> Limes Mlt 'Projective t n m x
lmMltPrjOrnt p
p (Diagram 'Discrete n 'N0 (Orientation p)
 -> Product n (Orientation p))
-> (FinList n p -> Diagram 'Discrete n 'N0 (Orientation p))
-> FinList n p
-> Product n (Orientation p)
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
. FinList n p -> Diagram 'Discrete n 'N0 (Orientation p)
FinList n (Point (Orientation p))
-> Diagram 'Discrete n 'N0 (Orientation p)
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete

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

-- 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 = p -> Limits Mlt 'Projective 'Discrete n 'N0 (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Projective t n m (Orientation p)
lmsMltPrjOrnt

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

-- Sum -


-- | 'Diagrammatic' object for a sum.

type SumDiagrammatic d (n :: N') = d Discrete n N0 :: Type -> Type

-- | 'Diagram' for a sum.

type SumDiagram n = SumDiagrammatic Diagram n

-- | 'Conic' object for a sum.

type SumConic c (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N')
  = c Mlt Injective d Discrete n N0 :: Type -> Type

-- | 'Cone' for a sum.

type SumCone n = SumConic Cone Diagram n

-- | generic sum as a 'LimesG'.

type SumG c d n = LimesG c Mlt Injective d Discrete (n :: N') N0

-- | sum as a 'Limes'.

type Sum n = SumG Cone Diagram n

-- | generic sums for a 'Multiplicative' structure.

type SumsG c d n = LimitsG c Mlt Injective d Discrete (n :: N') N0

-- | sums for a 'Multiplicative' structure.

type Sums n = SumsG Cone Diagram n

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

-- DualisableGDiscrete -


-- | type for dualisable generic limits of 'Conic' objects over t'Discrete' 'Diagrammatic' objects.

type DualisableGDiscrete p o c d n
  = NaturalConicBi (IsoO Mlt o) c Mlt p d Discrete n N0
  
--------------------------------------------------------------------------------

-- coProductsG -


-- | the co-object of 'ProductsG'.

coProductsG ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableGDiscrete Projective o c d n
  )
  => ProductsG c d n x -> SumsG c d n (o x)
coProductsG :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGDiscrete 'Projective o c d n) =>
ProductsG c d n x -> SumsG c d n (o x)
coProductsG ProductsG c d n x
ps = Dual1 (LimitsG c Mlt 'Projective d 'Discrete n 'N0) (o x)
LimitsG c Mlt 'Injective d 'Discrete n 'N0 (o x)
ss where
  Contravariant2 IsoO Mlt o x (o x)
i = Struct Mlt x
-> Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt o)) x (o x)
forall (o :: * -> *) r x.
TransformableGRefl o r =>
Struct r x -> Variant2 'Contravariant (IsoO r o) x (o x)
toDualO (Struct Mlt x
forall {x}. Multiplicative x => Struct Mlt x
forall s x. Structure s x => Struct s x
Struct :: Multiplicative x => Struct Mlt x)

  SDualBi (Left1 Dual1 (LimitsG c Mlt 'Projective d 'Discrete n 'N0) (o x)
ss) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Projective d 'Discrete n 'N0) x
-> SDualBi (LimitsG c Mlt 'Projective d 'Discrete n 'N0) (o x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt o x (o x)
i (Either1
  (Dual1 (LimitsG c Mlt 'Projective d 'Discrete n 'N0))
  (LimitsG c Mlt 'Projective d 'Discrete n 'N0)
  x
-> SDualBi (LimitsG c Mlt 'Projective d 'Discrete n 'N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ProductsG c d n x
-> Either1
     (LimitsG c Mlt 'Injective d 'Discrete n 'N0)
     (LimitsG c Mlt 'Projective d 'Discrete n 'N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ProductsG c d n x
ps))

-- | the co-object of 'Products'.

coProducts ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableMultiplicative Mlt o
  )
  => Products n x -> Sums n (o x)
coProducts :: forall x (o :: * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableMultiplicative Mlt o) =>
Products n x -> Sums n (o x)
coProducts = ProductsG Cone Diagram n x -> SumsG Cone Diagram n (o x)
forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGDiscrete 'Projective o c d n) =>
ProductsG c d n x -> SumsG c d n (o x)
coProductsG

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

-- 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) = FinList n (Point a) -> Diagram 'Discrete n 'N0 a
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete ((a -> Point a) -> FinList n a -> FinList n (Point a)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 a -> Point a
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) = Diagram 'Discrete n 'N0 a
-> Point a
-> FinList n a
-> Cone Mlt 'Injective Diagram 'Discrete n 'N0 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 (Diagram ('Star 'To) (n + 1) n a -> Diagram 'Discrete n 'N0 a
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

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

-- sums0 -


-- | sums of zero points given by a initial point.

sums0 :: Multiplicative x => InitialPoint x -> Sums N0 x
sums0 :: forall x. Multiplicative x => InitialPoint x -> Sums 'N0 x
sums0 InitialPoint x
ip = LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0 x
sms where
  Contravariant2 IsoO Mlt Op x (Op x)
i = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt

  SDualBi (Left1 Dual1 (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0) (Op x)
tp)   = IsoO Mlt Op x (Op x)
-> SDualBi (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0) x
-> SDualBi
     (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt Op x (Op x)
i (Either1
  (Dual1 (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0))
  (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0)
  x
-> SDualBi (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (InitialPoint x
-> Either1
     (LimesG Cone Mlt 'Projective Diagram 'Empty 'N0 'N0)
     (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 InitialPoint x
ip))
  pds :: Products 'N0 (Op x)
pds                  = TerminalPoint (Op x) -> Products 'N0 (Op x)
forall x. Multiplicative x => TerminalPoint x -> Products 'N0 x
products0 Dual1 (LimesG Cone Mlt 'Injective Diagram 'Empty 'N0 'N0) (Op x)
TerminalPoint (Op x)
tp
  SDualBi (Right1 LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0 x
sms) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0) (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Mlt Op x (Op x) -> Inv2 (HomDisjEmpty Mlt Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Mlt Op x (Op x)
i) (Either1
  (Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Products 'N0 (Op x)
-> Either1
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete 'N0 'N0)
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete 'N0 'N0)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Products 'N0 (Op x)
pds)) 


-- | sums of one point, i.e. 'Maxima'.

sums1 :: Multiplicative x => Sums N1 x
sums1 :: forall x. Multiplicative x => Sums N1 x
sums1 = LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0 x
ss where
  Contravariant2 IsoO Mlt Op x (Op x)
i = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt
  SDualBi (Right1 LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0 x
ss) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0) (Op x)
-> SDualBi (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Mlt Op x (Op x) -> Inv2 (HomDisjEmpty Mlt Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Mlt Op x (Op x)
i) (Either1
  (Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 (Op x)
-> Either1
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete N1 'N0)
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N1 'N0)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 LimitsG Cone Mlt 'Projective Diagram 'Discrete N1 'N0 (Op x)
forall x. Multiplicative x => Products N1 x
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
s2 = LimitsG Cone Mlt 'Injective Diagram 'Discrete (n + 2) 'N0 a
LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0 a
ss where
  Contravariant2 IsoO Mlt Op a (Op a)
i = Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) a (Op a)
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt

  SDualBi (Left1 Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op a)
p2)  = IsoO Mlt Op a (Op a)
-> SDualBi (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) a
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op a)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF IsoO Mlt Op a (Op a)
i (Either1
  (Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0)
  a
-> SDualBi (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) a
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Sums N2 a
-> Either1
     (LimitsG Cone Mlt 'Projective Diagram 'Discrete N2 'N0)
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0)
     a
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Sums N2 a
s2))
  ps :: Products (n + 2) (Op a)
ps                  = Products N2 (Op a) -> Products (n + 2) (Op a)
forall x (n :: N').
Multiplicative x =>
Products N2 x -> Products (n + 2) x
products2 Dual1 (LimitsG Cone Mlt 'Injective Diagram 'Discrete N2 'N0) (Op a)
Products N2 (Op a)
p2 
  SDualBi (Right1 LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0 a
ss) = Inv2 (HomDisjEmpty Mlt Op) (Op a) a
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
     (Op a)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0) a
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Mlt Op a (Op a) -> Inv2 (HomDisjEmpty Mlt Op) (Op a) a
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Mlt Op a (Op a)
i) (Either1
  (Dual1
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0))
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
  (Op a)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
     (Op a)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Dual1
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
  (Op a)
-> Either1
     (Dual1
        (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0))
     (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
     (Op a)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 Dual1
  (LimitsG Cone Mlt 'Injective Diagram 'Discrete ('S ('S n)) 'N0)
  (Op a)
Products (n + 2) (Op a)
ps))
  

-- | 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 = (Diagram 'Discrete n 'N0 a
 -> LimesG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a)
-> LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG (Sums 'N0 a
-> Sums N2 a
-> Diagram 'Discrete n 'N0 a
-> LimesG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
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       -> LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
-> SumDiagram n a -> Sum n a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
Sums 'N0 a
sum0 SumDiagram n a
d
    DiagramDiscrete (Point a
_:|FinList n1 (Point a)
Nil)  -> LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
-> SumDiagram n a -> Sum n a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
Sums N1 a
forall x. Multiplicative x => Sums N1 x
sums1 SumDiagram n a
d
    DiagramDiscrete (Point a
_:|Point a
_:|FinList n1 (Point a)
_) -> LimitsG Cone Mlt 'Injective Diagram 'Discrete n 'N0 a
-> SumDiagram n a -> Sum n a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes (Sums N2 a -> Sums (n1 + 2) a
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
_ = Sums 'N0 a -> Sums N2 a -> Sums n a
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 = p
-> Diagram 'Discrete n 'N0 (Orientation p)
-> Cone Mlt 'Injective Diagram 'Discrete n 'N0 (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 (FinList n (Point (Orientation p))
-> Diagram 'Discrete n 'N0 (Orientation p)
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n p
FinList n (Point (Orientation 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 = p
-> Diagram 'Discrete n 'N0 (Orientation p)
-> Limes Mlt 'Injective 'Discrete n 'N0 (Orientation p)
forall p x (t :: DiagramType) (n :: N') (m :: N').
(Entity p, x ~ Orientation p) =>
p -> Diagram t n m x -> Limes Mlt 'Injective t n m x
lmMltInjOrnt p
p (FinList n (Point (Orientation p))
-> Diagram 'Discrete n 'N0 (Orientation p)
forall (n :: N') a.
FinList n (Point a) -> Diagram 'Discrete n 'N0 a
DiagramDiscrete FinList n p
FinList n (Point (Orientation 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 = p -> Limits Mlt 'Injective 'Discrete n 'N0 (Orientation p)
forall p (t :: DiagramType) (n :: N') (m :: N').
Entity p =>
p -> Limits Mlt 'Injective t n m (Orientation p)
lmsMltInjOrnt