{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.MinimaAndMaxima

-- Description : minima and maxima

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- minima and maxima within a 'Multiplicative' structure, i.e. limits of @'Diagram' ('Chain' __t__)@.

module OAlg.Limes.MinimaAndMaxima
  (
    -- * Minima

    Minima, MinimaG
  , Minimum, MinimumG
  , MinimumCone, MinimumConic
  , MinimumDiagram, MinimumDiagrammatic
  , minimaTo, minimaGTo
  , minimaFrom, minimaGFrom

    -- * Maxima

  , Maxima, MaximaG
  , Maximum, MaximumG
  , MaximumCone, MaximumConic
  , MaximumDiagram, MaximumDiagrammatic
  , maximaTo, maximaFrom, maximaTo', maximaFrom'

    -- * Duality

  , DualisableGChain
  , coMinimaGTo, coMinimaGFrom
  )
  where

import Control.Monad

import Data.Typeable
import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality

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

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

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

import OAlg.Hom.Definition
import OAlg.Hom.Multiplicative

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


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

-- Minima -


-- | 'Diagrammatic' object for a minimum.

type MinimumDiagrammatic d t n = d (Chain t) (n+1) n :: Type -> Type

-- | 'Diagram' for a minimum.

type MinimumDiagram t n = MinimumDiagrammatic Diagram t n

-- | 'Conic' object for a minimum.

type MinimumConic c (d :: DiagramType -> N' -> N' -> Type -> Type) t n
  = c Mlt Projective d (Chain t) (n+1) n :: Type -> Type

-- | 'Cone' for a minimum.

type MinimumCone t n = MinimumConic Cone Diagram t n

-- | generic minimum as 'LimesG'.

type MinimumG c d t n = LimesG c Mlt Projective d (Chain t) (n+1) n

-- | minimum as 'Limes'.

type Minimum t n = MinimumG Cone Diagram t n

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

type MinimaG c d t n = LimitsG c Mlt Projective d (Chain t) (n+1) n

-- | minima for a 'Multiplicative' structure.

type Minima t n = MinimaG Cone Diagram t n

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

-- minima -


-- | generic minima according to @'OAlg.Entity.Diagram.Definition.Chain' 'To'@.

minimaGTo ::
  ( Multiplicative x
  , Diagrammatic d
  ) => MinimaG Cone d To n x
minimaGTo :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimaG Cone d 'To n x
minimaGTo = (d ('Chain 'To) ('S n) n x
 -> LimesG Cone Mlt 'Projective d ('Chain 'To) ('S n) n x)
-> LimitsG Cone Mlt 'Projective d ('Chain 'To) ('S n) 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.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG MinimumDiagrammatic d 'To n x -> MinimumG Cone d 'To n x
d ('Chain 'To) ('S n) n x
-> LimesG Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimumDiagrammatic d 'To n x -> MinimumG Cone d 'To n x
lMin where
  lMin :: (Multiplicative x, Diagrammatic d)
       => MinimumDiagrammatic d To n x -> MinimumG Cone d To n x
  lMin :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimumDiagrammatic d 'To n x -> MinimumG Cone d 'To n x
lMin MinimumDiagrammatic d 'To n x
d = Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
-> (Cone Mlt 'Projective d ('Chain 'To) ('S n) n x -> x)
-> LimesG Cone Mlt 'Projective d ('Chain 'To) ('S n) n 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 d ('Chain 'To) (n + 1) n x
Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
l Cone Mlt 'Projective d ('Chain 'To) ('S n) n x -> x
forall {d :: DiagramType -> N' -> N' -> * -> *} {n :: N'} {x}.
Cone Mlt 'Projective d ('Chain 'To) ('S n) n x -> x
u where
    l :: Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
l = FactorChain d 'To n x
-> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'To n x
-> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
cnPrjChainTo (x -> MinimumDiagrammatic d 'To n x -> FactorChain d 'To n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain (Point x -> x
forall c. Multiplicative c => Point c -> c
one (Diagram ('Chain 'To) ('S n) n x -> Point x
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart (Diagram ('Chain 'To) ('S n) n x -> Point x)
-> Diagram ('Chain 'To) ('S n) n x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d ('Chain 'To) ('S n) n x -> Diagram ('Chain 'To) ('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 MinimumDiagrammatic d 'To n x
d ('Chain 'To) ('S n) n x
d)) MinimumDiagrammatic d 'To n x
d)
    u :: Cone Mlt 'Projective d ('Chain 'To) ('S n) n x -> x
u Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
c = x
f where FactorChain x
f d ('Chain 'To) (n + 1) n x
_ = Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
-> FactorChain d 'To n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
-> FactorChain d 'To n x
cnPrjChainToInv Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
c

-- | minima according to @'Chain' 'To'@.

minimaTo :: Multiplicative x => Minima To n x
minimaTo :: forall x (n :: N'). Multiplicative x => Minima 'To n x
minimaTo = MinimaG Cone Diagram 'To n x
forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimaG Cone d 'To n x
minimaGTo

-- | generic minima according to @'Chain' 'From'@.

minimaGFrom ::
  ( Multiplicative x
  , Diagrammatic d
  ) => MinimaG Cone d From n x
minimaGFrom :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimaG Cone d 'From n x
minimaGFrom = (d ('Chain 'From) ('S n) n x
 -> LimesG Cone Mlt 'Projective d ('Chain 'From) ('S n) n x)
-> LimitsG Cone Mlt 'Projective d ('Chain 'From) ('S n) 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.
(d t n m x -> LimesG c s p d t n m x) -> LimitsG c s p d t n m x
LimitsG MinimumDiagrammatic d 'From n x -> MinimumG Cone d 'From n x
d ('Chain 'From) ('S n) n x
-> LimesG Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimumDiagrammatic d 'From n x -> MinimumG Cone d 'From n x
lMin where
  lMin :: ( Multiplicative x, Diagrammatic d)
       => MinimumDiagrammatic d From n x -> MinimumG Cone d From n x
  lMin :: forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimumDiagrammatic d 'From n x -> MinimumG Cone d 'From n x
lMin MinimumDiagrammatic d 'From n x
d = Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
-> (Cone Mlt 'Projective d ('Chain 'From) ('S n) n x -> x)
-> LimesG Cone Mlt 'Projective d ('Chain 'From) ('S n) n 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 d ('Chain 'From) (n + 1) n x
Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
l Cone Mlt 'Projective d ('Chain 'From) ('S n) n x -> x
forall {d :: DiagramType -> N' -> N' -> * -> *} {n :: N'} {x}.
Cone Mlt 'Projective d ('Chain 'From) ('S n) n x -> x
u where
    l :: Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
l = FactorChain d 'From n x
-> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'From n x
-> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
cnPrjChainFrom (x -> MinimumDiagrammatic d 'From n x -> FactorChain d 'From n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain (Point x -> x
forall c. Multiplicative c => Point c -> c
one (Diagram ('Chain 'From) ('S n) n x -> Point x
forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart (Diagram ('Chain 'From) ('S n) n x -> Point x)
-> Diagram ('Chain 'From) ('S n) n x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ d ('Chain 'From) ('S n) n x -> Diagram ('Chain '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 MinimumDiagrammatic d 'From n x
d ('Chain 'From) ('S n) n x
d)) MinimumDiagrammatic d 'From n x
d)
    u :: Cone Mlt 'Projective d ('Chain 'From) ('S n) n x -> x
u Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
c = x
f where FactorChain x
f d ('Chain 'From) (n + 1) n x
_ = Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
-> FactorChain d 'From n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (n :: N') x.
Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
-> FactorChain d 'From n x
cnPrjChainFromInv Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
c

-- | minima according to @'Chain' 'From'@.

minimaFrom :: Multiplicative x => Minima From n x
minimaFrom :: forall x (n :: N'). Multiplicative x => Minima 'From n x
minimaFrom = MinimaG Cone Diagram 'From n x
forall x (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, Diagrammatic d) =>
MinimaG Cone d 'From n x
minimaGFrom

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

-- Maxima -


-- | 'Diagrammatic' object for a maximum.

type MaximumDiagrammatic d t n = d (Chain t) (n+1) n :: Type -> Type

-- | 'Diagram' for a maximum.

type MaximumDiagram t n = MaximumDiagrammatic Diagram t n

-- | 'Conic' object for a maximum.

type MaximumConic c (d :: DiagramType -> N' -> N' -> Type -> Type) t n
  = c Mlt Injective d (Chain t) (n+1) n :: Type -> Type

-- | 'Cone' for a maximum.

type MaximumCone t n = MaximumConic Cone Diagram t n

-- | generic maximum as 'LimesG'.

type MaximumG c d t n = LimesG c Mlt Injective d (Chain t) (n+1) n

-- | maximum as 'Limes'.

type Maximum t n = MaximumG Cone Diagram t n

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

type MaximaG c d t n = LimitsG c Mlt Injective d (Chain t) (n+1) n

-- | maxima for a 'Multiplicative' structure.

type Maxima t n = MaximaG Cone Diagram t n

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

-- DualisableGChain -


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

type DualisableGChain p t o c d n
  = NaturalConicBi (IsoO Mlt o) c Mlt p d (Chain t) (n+1) n

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

-- coMinimumTo -


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

coMinimumGTo ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableGChain Projective To o c d n
  )
  => MinimumG c d To n x -> MaximumG c d From n (o x)
coMinimumGTo :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGChain 'Projective 'To o c d n) =>
MinimumG c d 'To n x -> MaximumG c d 'From n (o x)
coMinimumGTo MinimumG c d 'To n x
min = Dual1 (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n) (o x)
LimesG c Mlt 'Injective d ('Chain 'From) (n + 1) n (o x)
max 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 (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n) (o x)
max) = IsoO Mlt o x (o x)
-> SDualBi (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n) x
-> SDualBi (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n) (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 (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n))
  (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n)
  x
-> SDualBi (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n x
-> Either1
     (Dual1 (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n))
     (LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 MinimumG c d 'To n x
LimesG c Mlt 'Projective d ('Chain 'To) ('S n) n x
min))

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

-- coMinimaTo -


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

coMinimaGTo ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableGChain Projective To o c d n
  )
  => MinimaG c d To n x -> MaximaG c d From n (o x)
coMinimaGTo :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGChain 'Projective 'To o c d n) =>
MinimaG c d 'To n x -> MaximaG c d 'From n (o x)
coMinimaGTo MinimaG c d 'To n x
min = Dual1 (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n) (o x)
LimitsG c Mlt 'Injective d ('Chain 'From) (n + 1) n (o x)
max 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 ('Chain 'To) ('S n) n) (o x)
max) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n) x
-> SDualBi
     (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n) (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 ('Chain 'To) ('S n) n))
  (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n)
  x
-> SDualBi (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n x
-> Either1
     (Dual1 (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n))
     (LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 MinimaG c d 'To n x
LimitsG c Mlt 'Projective d ('Chain 'To) ('S n) n x
min))

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

-- coMinimaFrom -


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

coMinimaGFrom ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableGChain Projective From o c d n
  )
  => MinimaG c d From n x -> MaximaG c d To n (o x)
coMinimaGFrom :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGChain 'Projective 'From o c d n) =>
MinimaG c d 'From n x -> MaximaG c d 'To n (o x)
coMinimaGFrom MinimaG c d 'From n x
min = Dual1 (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n) (o x)
LimitsG c Mlt 'Injective d ('Chain 'To) (n + 1) n (o x)
max 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 ('Chain 'From) ('S n) n) (o x)
max) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n) x
-> SDualBi
     (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n) (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 ('Chain 'From) ('S n) n))
  (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n)
  x
-> SDualBi (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n x
-> Either1
     (Dual1 (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n))
     (LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 MinimaG c d 'From n x
LimitsG c Mlt 'Projective d ('Chain 'From) ('S n) n x
min))

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

-- coMaximaFrom -


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

coMaximaGFrom ::
  ( Multiplicative x
  , TransformableGRefl o Mlt
  , DualisableGChain Injective From o c d n
  )
  => MaximaG c d From n x -> MinimaG c d To n (o x)
coMaximaGFrom :: forall x (o :: * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (n :: N').
(Multiplicative x, TransformableGRefl o Mlt,
 DualisableGChain 'Injective 'From o c d n) =>
MaximaG c d 'From n x -> MinimaG c d 'To n (o x)
coMaximaGFrom MaximaG c d 'From n x
min = Dual1 (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n) (o x)
LimitsG c Mlt 'Projective d ('Chain 'To) (n + 1) n (o x)
max 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 'Injective d ('Chain 'From) ('S n) n) (o x)
max) = IsoO Mlt o x (o x)
-> SDualBi (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n) x
-> SDualBi
     (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n) (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 'Injective d ('Chain 'From) ('S n) n))
  (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n)
  x
-> SDualBi (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n x
-> Either1
     (Dual1 (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n))
     (LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n)
     x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 MaximaG c d 'From n x
LimitsG c Mlt 'Injective d ('Chain 'From) ('S n) n x
min))

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

-- maxima -


-- | maxima according to @'Chain' 'To'@.

maximaTo :: Multiplicative x => Maxima To n x
maximaTo :: forall x (n :: N'). Multiplicative x => Maxima 'To n x
maximaTo = Dual1
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n) x
LimitsG Cone Mlt 'Injective Diagram ('Chain 'To) (n + 1) n x
maxs 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
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n) x
maxs) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n)
     (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n) 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 'Projective Diagram ('Chain 'From) ('S n) n))
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n)
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n (Op x)
-> Either1
     (Dual1
        (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n))
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n)
     (Op x)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Minima 'From n (Op x)
LimitsG Cone Mlt 'Projective Diagram ('Chain 'From) ('S n) n (Op x)
forall x (n :: N'). Multiplicative x => Minima 'From n x
minimaFrom)) 

-- | maxima according to @'Chain' 'From'@.

maximaFrom :: Multiplicative x => Maxima From n x
maximaFrom :: forall x (n :: N'). Multiplicative x => Maxima 'From n x
maximaFrom = Dual1
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n) x
LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) (n + 1) n x
maxs 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
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n) x
maxs) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n) (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n) 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 'Projective Diagram ('Chain 'To) ('S n) n))
  (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n)
  (Op x)
-> SDualBi
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n (Op x)
-> Either1
     (Dual1
        (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n))
     (LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n)
     (Op x)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Minima 'To n (Op x)
LimitsG Cone Mlt 'Projective Diagram ('Chain 'To) ('S n) n (Op x)
forall x (n :: N'). Multiplicative x => Minima 'To n x
minimaTo)) 

-- | maxima according to @'Chain' 'To'@ given by two proxy types.

maximaTo' :: Multiplicative x => p n -> f x -> Maxima To n x
maximaTo' :: forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'To n x
maximaTo' p n
_ f x
_ = Maxima 'To n x
forall x (n :: N'). Multiplicative x => Maxima 'To n x
maximaTo

-- | maxima according to @'Chain' 'From'@ given by two proxy types.

maximaFrom' :: Multiplicative x => p n -> f x -> Maxima From n x
maximaFrom' :: forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'From n x
maximaFrom' p n
_ f x
_ = Maxima 'From n x
forall x (n :: N'). Multiplicative x => Maxima 'From n x
maximaFrom

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

-- xecOrtSiteChain -


xecPrjOrtSiteTo :: (Conic c, Diagrammatic d, Multiplicative x)
  => XOrtSite To x -> MinimumG c d t n x -> X (MinimumConic Cone d t n x)
xecPrjOrtSiteTo :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x (t :: Site) (n :: N').
(Conic c, Diagrammatic d, Multiplicative x) =>
XOrtSite 'To x
-> MinimumG c d t n x -> X (MinimumConic Cone d t n x)
xecPrjOrtSiteTo XOrtSite 'To x
xe = XOrtSite 'To x
-> d ('Chain t) (n + 1) n x
-> X (Cone Mlt 'Projective d ('Chain t) (n + 1) n x)
forall (d :: DiagramType -> N' -> N' -> * -> *) x (t :: Site)
       (n :: N').
(Diagrammatic d, Multiplicative x) =>
XOrtSite 'To x
-> d ('Chain t) (n + 1) n x -> X (MinimumConic Cone d t n x)
xcn XOrtSite 'To x
xe (d ('Chain t) ('S n) n x
 -> X (Cone Mlt 'Projective d ('Chain t) ('S n) n x))
-> (LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
    -> d ('Chain t) ('S n) n x)
-> LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
-> X (Cone Mlt 'Projective d ('Chain t) ('S n) n 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 Mlt 'Projective d ('Chain t) ('S n) n x
-> d ('Chain t) ('S n) n 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 (Cone Mlt 'Projective d ('Chain t) ('S n) n x
 -> d ('Chain t) ('S n) n x)
-> (LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
    -> Cone Mlt 'Projective d ('Chain t) ('S n) n x)
-> LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
-> d ('Chain t) ('S n) n 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
. c Mlt 'Projective d ('Chain t) ('S n) n x
-> Cone Mlt 'Projective d ('Chain t) ('S n) n x
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s p d t n m x -> Cone s p d t n m x
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Conic c =>
c s p d t n m x -> Cone s p d t n m x
cone (c Mlt 'Projective d ('Chain t) ('S n) n x
 -> Cone Mlt 'Projective d ('Chain t) ('S n) n x)
-> (LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
    -> c Mlt 'Projective d ('Chain t) ('S n) n x)
-> LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
-> Cone Mlt 'Projective d ('Chain t) ('S n) n 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
. LimesG c Mlt 'Projective d ('Chain t) ('S n) n x
-> c Mlt 'Projective d ('Chain t) ('S n) 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.
LimesG c s p d t n m x -> c s p d t n m x
universalCone where
  
  xcn :: (Diagrammatic d, Multiplicative x)
    => XOrtSite To x -> d (Chain t) (n+1) n x -> X (MinimumConic Cone d t n x)
  xcn :: forall (d :: DiagramType -> N' -> N' -> * -> *) x (t :: Site)
       (n :: N').
(Diagrammatic d, Multiplicative x) =>
XOrtSite 'To x
-> d ('Chain t) (n + 1) n x -> X (MinimumConic Cone d t n x)
xcn (XEnd X (Point x)
_ Point x -> X x
xe) d ('Chain t) (n + 1) n x
d = case d ('Chain t) ('S n) n x -> Diagram ('Chain t) ('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 ('Chain t) (n + 1) n x
d ('Chain t) ('S n) n x
d of
    d' :: Diagram ('Chain t) ('S n) n x
d'@(DiagramChainTo Point x
_ FinList n x
_)   -> do
      x
f <- Point x -> X x
xe (Point x -> X x) -> Point x -> X x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram ('Chain 'To) ('S n) n x -> Point x
forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart Diagram ('Chain t) ('S n) n x
Diagram ('Chain 'To) ('S n) n x
d'
      Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
-> X (Cone Mlt 'Projective d ('Chain 'To) ('S n) n x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
 -> X (Cone Mlt 'Projective d ('Chain 'To) ('S n) n x))
-> Cone Mlt 'Projective d ('Chain 'To) ('S n) n x
-> X (Cone Mlt 'Projective d ('Chain 'To) ('S n) n x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FactorChain d 'To n x
-> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'To n x
-> Cone Mlt 'Projective d ('Chain 'To) (n + 1) n x
cnPrjChainTo (x -> d ('Chain 'To) (n + 1) n x -> FactorChain d 'To n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain x
f d ('Chain t) (n + 1) n x
d ('Chain 'To) (n + 1) n x
d)
    DiagramChainFrom Point x
s FinList n x
_      -> do
      x
f <- Point x -> X x
xe Point x
s
      Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
-> X (Cone Mlt 'Projective d ('Chain 'From) ('S n) n x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
 -> X (Cone Mlt 'Projective d ('Chain 'From) ('S n) n x))
-> Cone Mlt 'Projective d ('Chain 'From) ('S n) n x
-> X (Cone Mlt 'Projective d ('Chain 'From) ('S n) n x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ FactorChain d 'From n x
-> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
forall (d :: DiagramType -> N' -> N' -> * -> *) x (n :: N').
(Diagrammatic d, Multiplicative x) =>
FactorChain d 'From n x
-> Cone Mlt 'Projective d ('Chain 'From) (n + 1) n x
cnPrjChainFrom (x -> d ('Chain 'From) (n + 1) n x -> FactorChain d 'From n x
forall (d :: DiagramType -> N' -> N' -> * -> *) (s :: Site)
       (n :: N') x.
x -> d ('Chain s) (n + 1) n x -> FactorChain d s n x
FactorChain x
f d ('Chain t) (n + 1) n x
d ('Chain 'From) (n + 1) n x
d)

xecInjOrtSiteFrom ::
  ( Multiplicative x
  , NaturalConicBi (IsoO Mlt Op) c Mlt Injective d (Chain t) (n+1) n
  )
  => XOrtSite From x -> MaximumG c d t n x -> X (MaximumConic Cone d t n x)
xecInjOrtSiteFrom :: forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Multiplicative x,
 NaturalConicBi
   (Inv2 (HomDisjEmpty Mlt Op))
   c
   Mlt
   'Injective
   d
   ('Chain t)
   (n + 1)
   n) =>
XOrtSite 'From x
-> MaximumG c d t n x -> X (MaximumConic Cone d t n x)
xecInjOrtSiteFrom XOrtSite 'From x
xosFrom = LimesG c Mlt 'Injective d ('Chain t) (n + 1) n x
-> X (Cone Mlt 'Injective d ('Chain t) (n + 1) n x)
LimesG c Mlt 'Injective d ('Chain t) ('S n) n x
-> X (Cone Mlt 'Injective d ('Chain t) ('S n) n x)
xec where
  xec' :: MinimumG c d (Dual t) n (Op x)
-> X (MinimumConic Cone d (Dual t) n (Op x))
xec' = XOrtSite 'To (Op x)
-> MinimumG c d (Dual t) n (Op x)
-> X (MinimumConic Cone d (Dual t) n (Op x))
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x (t :: Site) (n :: N').
(Conic c, Diagrammatic d, Multiplicative x) =>
XOrtSite 'To x
-> MinimumG c d t n x -> X (MinimumConic Cone d t n x)
xecPrjOrtSiteTo (XOrtSite 'From x -> Dual (XOrtSite 'From x)
forall (s :: Site) q. XOrtSite s q -> Dual (XOrtSite s q)
coXOrtSite XOrtSite 'From x
xosFrom)
  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 (XEligibleConeG LimesG c Mlt 'Injective d ('Chain t) ('S n) n x
-> X (Cone Mlt 'Injective d ('Chain t) ('S n) n x)
xec)) = Inv2 (HomDisjEmpty Mlt Op) (Op x) x
-> SDualBi
     (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n)
     (Op x)
-> SDualBi
     (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n) x
forall (h :: * -> * -> *)
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x y.
NaturalConicBi (Inv2 h) c s p d t n m =>
Inv2 h x y
-> SDualBi (XEligibleConeG c s p d t n m) x
-> SDualBi (XEligibleConeG c s p d t n m) y
xecMapS (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
     (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n))
  (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n)
  (Op x)
-> SDualBi
     (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n)
     (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (XEligibleConeG
  c Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op x)
-> Either1
     (XEligibleConeG
        c Mlt 'Injective d ('Chain (Dual (Dual t))) ('S n) n)
     (XEligibleConeG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n)
     (Op x)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 ((LimesG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op x)
 -> X (Cone Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op x)))
-> XEligibleConeG
     c Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op 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 -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG MinimumG c d (Dual t) n (Op x)
-> X (MinimumConic Cone d (Dual t) n (Op x))
LimesG c Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op x)
-> X (Cone Mlt 'Projective d ('Chain (Dual t)) ('S n) n (Op x))
xec')))

xecOrtSiteChain ::
  (  Multiplicative x
  , s ~ Mlt
  , NaturalConicBi (IsoO Mlt Op) c Mlt Injective d (Chain t) (n+1) n
  )
  => XOrtSite r x -> XEligibleConeG c s (ToPerspective r) d (Chain t) (n+1) n x
xecOrtSiteChain :: forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N')
       (r :: Site).
(Multiplicative x, s ~ Mlt,
 NaturalConicBi
   (Inv2 (HomDisjEmpty Mlt Op))
   c
   Mlt
   'Injective
   d
   ('Chain t)
   (n + 1)
   n) =>
XOrtSite r x
-> XEligibleConeG c s (ToPerspective r) d ('Chain t) (n + 1) n x
xecOrtSiteChain xe :: XOrtSite r x
xe@(XEnd X (Point x)
_ Point x -> X x
_)   = (LimesG c s 'Projective d ('Chain t) ('S n) n x
 -> X (Cone s 'Projective d ('Chain t) ('S n) n x))
-> XEligibleConeG c s 'Projective d ('Chain t) ('S n) 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG (XOrtSite 'To x
-> MinimumG c d t n x -> X (MinimumConic Cone d t n x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x (t :: Site) (n :: N').
(Conic c, Diagrammatic d, Multiplicative x) =>
XOrtSite 'To x
-> MinimumG c d t n x -> X (MinimumConic Cone d t n x)
xecPrjOrtSiteTo XOrtSite r x
XOrtSite 'To x
xe)
xecOrtSiteChain xs :: XOrtSite r x
xs@(XStart X (Point x)
_ Point x -> X x
_) = (LimesG c s 'Injective d ('Chain t) ('S n) n x
 -> X (Cone s 'Injective d ('Chain t) ('S n) n x))
-> XEligibleConeG c s 'Injective d ('Chain t) ('S n) 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.
(LimesG c s p d t n m x -> X (Cone s p d t n m x))
-> XEligibleConeG c s p d t n m x
XEligibleConeG (XOrtSite 'From x
-> MaximumG c d t n x -> X (MaximumConic Cone d t n x)
forall x
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N').
(Multiplicative x,
 NaturalConicBi
   (Inv2 (HomDisjEmpty Mlt Op))
   c
   Mlt
   'Injective
   d
   ('Chain t)
   (n + 1)
   n) =>
XOrtSite 'From x
-> MaximumG c d t n x -> X (MaximumConic Cone d t n x)
xecInjOrtSiteFrom XOrtSite r x
XOrtSite 'From x
xs)

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

-- prpMinimaAndMaxima -


prpMinimaAndMaxima :: N -> Statement
prpMinimaAndMaxima :: N -> Statement
prpMinimaAndMaxima N
n = case N -> SomeNatural
someNatural N
n of
  SomeNatural W n
n' -> [Statement] -> Statement
And [ XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'To)
  ('S n)
  n
  (Orientation Symbol)
-> XEligibleConeFactorG
     Cone
     Mlt
     'Injective
     Diagram
     ('Chain 'To)
     ('S n)
     n
     (Orientation Symbol)
-> X (Diagram ('Chain 'To) ('S n) n (Orientation Symbol))
-> LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Chain 'To)
     ('S n)
     n
     (Orientation Symbol)
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'To)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecMaxTo XEligibleConeFactorG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'To)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfMaxTo X (Diagram ('Chain 'To) ('S n) n (Orientation Symbol))
forall x. XStandard x => X x
xStandard Maxima 'To n (Orientation Symbol)
LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'To)
  ('S n)
  n
  (Orientation Symbol)
maxTo
                        , XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
-> XEligibleConeFactorG
     Cone
     Mlt
     'Injective
     Diagram
     ('Chain 'From)
     ('S n)
     n
     (Orientation Symbol)
-> X (Diagram ('Chain 'From) ('S n) n (Orientation Symbol))
-> LimitsG
     Cone
     Mlt
     'Injective
     Diagram
     ('Chain 'From)
     ('S n)
     n
     (Orientation Symbol)
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecMaxFm XEligibleConeFactorG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfMaxFm X (Diagram ('Chain 'From) ('S n) n (Orientation Symbol))
forall x. XStandard x => X x
xStandard Maxima 'From n (Orientation Symbol)
LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
maxFm
                        , XEligibleConeG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
-> XEligibleConeFactorG
     Cone
     Mlt
     (Dual 'Injective)
     Diagram
     (Dual ('Chain 'From))
     ('S n)
     n
     (Op (Orientation Symbol))
-> X (Diagram
        (Dual ('Chain 'From)) ('S n) n (Op (Orientation Symbol)))
-> LimitsG
     Cone
     Mlt
     (Dual 'Injective)
     Diagram
     (Dual ('Chain 'From))
     ('S n)
     n
     (Op (Orientation Symbol))
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
xecMaxFm' XEligibleConeFactorG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
xecfMaxFm' X (Diagram
     (Dual ('Chain 'From)) ('S n) n (Op (Orientation Symbol)))
forall x. XStandard x => X x
xStandard Dual1
  (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
  (Op (Orientation Symbol))
LimitsG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
maxFm'
                        , XEligibleConeG Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
-> XEligibleConeFactorG
     Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
-> X (Diagram ('Chain 'To) ('S n) n N)
-> LimitsG Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
xecMaxToN XEligibleConeFactorG
  Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
forall {s} {d :: DiagramType -> N' -> N' -> * -> *}
       {t :: DiagramType} {n :: N'} {m :: N'}.
XEligibleConeFactorG Cone s 'Injective d t n m N
xecfMaxToN X (Diagram ('Chain 'To) ('S n) n N)
forall x. XStandard x => X x
xStandard Maxima 'To n N
LimitsG Cone Mlt 'Injective Diagram ('Chain 'To) ('S n) n N
maxToN
                        , XEligibleConeG
  Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
-> XEligibleConeFactorG
     Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
-> X (Diagram ('Chain 'From) ('S n) n N)
-> LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
-> Statement
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N') x.
(Conic c, Diagrammatic d, Show (c s p d t n m x),
 Validable (c s p d t n m x), Entity (d t n m x), Entity x) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeFactorG c s p d t n m x
-> X (d t n m x)
-> LimitsG c s p d t n m x
-> Statement
prpLimitsG XEligibleConeG
  Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
xecMaxFromN XEligibleConeFactorG
  Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
forall {s} {d :: DiagramType -> N' -> N' -> * -> *}
       {t :: DiagramType} {n :: N'} {m :: N'}.
XEligibleConeFactorG Cone s 'Injective d t n m N
xecfMaxFromN X (Diagram ('Chain 'From) ('S n) n N)
forall x. XStandard x => X x
xStandard Maxima 'From n N
LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n N
maxFromN
                        ]
    where
      maxTo :: Maxima 'To n (Orientation Symbol)
maxTo     = W n
-> Proxy (Orientation Symbol) -> Maxima 'To n (Orientation Symbol)
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'To n x
maximaTo' W n
n' (Proxy (Orientation Symbol)
forall {k} (t :: k). Proxy t
Proxy :: Proxy OS)
      xecMaxTo :: XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecMaxTo  = X Symbol
-> XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt X Symbol
forall x. XStandard x => X x
xStandard
      xecfMaxTo :: XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfMaxTo = X Symbol
-> XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt X Symbol
forall x. XStandard x => X x
xStandard

      maxFm :: Maxima 'From n (Orientation Symbol)
maxFm     = W n
-> Proxy (Orientation Symbol)
-> Maxima 'From n (Orientation Symbol)
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'From n x
maximaFrom' W n
n' (Proxy (Orientation Symbol)
forall {k} (t :: k). Proxy t
Proxy :: Proxy OS)
      xecMaxFm :: XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecMaxFm  = X Symbol
-> XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeG c s p d t n m (Orientation x)
xEligibleConeGOrnt X Symbol
forall x. XStandard x => X x
xStandard
      xecfMaxFm :: XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfMaxFm = X Symbol
-> XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) x s (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
(Conic c, Diagrammatic d) =>
X x -> XEligibleConeFactorG c s p d t n m (Orientation x)
xEligibleConeFactorGOrnt X Symbol
forall x. XStandard x => X x
xStandard

      Contravariant2 IsoO Mlt Op (Orientation Symbol) (Op (Orientation Symbol))
i = Variant2
  'Contravariant
  (Inv2 (HomDisjEmpty Mlt Op))
  (Orientation Symbol)
  (Op (Orientation Symbol))
forall x.
Multiplicative x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Mlt Op)) x (Op x)
toDualOpMlt
      SDualBi (Left1 Dual1
  (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
  (Op (Orientation Symbol))
maxFm') = IsoO Mlt Op (Orientation Symbol) (Op (Orientation Symbol))
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
     (Orientation Symbol)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
     (Op (Orientation Symbol))
forall x y.
Inv2 (HomDisjEmpty Mlt Op) x y
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n) x
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n) y
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
ApplicativeG t a b =>
a x y -> b (t x) (t y)
amapG IsoO Mlt Op (Orientation Symbol) (Op (Orientation Symbol))
i (Either1
  (Dual1
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n))
  (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
  (Orientation Symbol)
-> SDualBi
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
     (Orientation Symbol)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
-> Either1
     (Dual1
        (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n))
     (LimitsG Cone Mlt 'Injective Diagram ('Chain 'From) ('S n) n)
     (Orientation Symbol)
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Maxima 'From n (Orientation Symbol)
LimitsG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
maxFm))
      xecMaxFm' :: XEligibleConeG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
xecMaxFm'  = XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
-> XEligibleConeG
     Cone
     Mlt
     (Dual 'Injective)
     Diagram
     (Dual ('Chain 'From))
     ('S n)
     n
     (Op (Orientation Symbol))
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeG c s p d t n m x
-> XEligibleConeG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeG XEligibleConeG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeG Cone s p Diagram t n m (Orientation Symbol)
xecMaxFm
      xecfMaxFm' :: XEligibleConeFactorG
  Cone
  Mlt
  (Dual 'Injective)
  Diagram
  (Dual ('Chain 'From))
  ('S n)
  n
  (Op (Orientation Symbol))
xecfMaxFm' = XEligibleConeFactorG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
-> XEligibleConeFactorG
     Cone
     Mlt
     (Dual 'Injective)
     Diagram
     (Dual ('Chain 'From))
     ('S n)
     n
     (Op (Orientation Symbol))
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x,
 NaturalConicBi (Inv2 (HomDisjEmpty s Op)) c s p d t n m,
 s ~ Mlt) =>
XEligibleConeFactorG c s p d t n m x
-> XEligibleConeFactorG c s (Dual p) d (Dual t) n m (Op x)
coXEligibleConeFactorG XEligibleConeFactorG
  Cone
  Mlt
  'Injective
  Diagram
  ('Chain 'From)
  ('S n)
  n
  (Orientation Symbol)
forall {s} {p :: Perspective} {t :: DiagramType} {n :: N'}
       {m :: N'}.
XEligibleConeFactorG Cone s p Diagram t n m (Orientation Symbol)
xecfMaxFm

      maxToN :: Maxima 'To n N
maxToN     = W n -> Proxy N -> Maxima 'To n N
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'To n x
maximaTo' W n
n' (Proxy N
forall {k} (t :: k). Proxy t
Proxy :: Proxy N)
      xecMaxToN :: XEligibleConeG
  Cone Mlt (ToPerspective 'From) Diagram ('Chain 'To) (n + 1) n N
xecMaxToN  = XOrtSite 'From N
-> XEligibleConeG
     Cone Mlt (ToPerspective 'From) Diagram ('Chain 'To) (n + 1) n N
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N')
       (r :: Site).
(Multiplicative x, s ~ Mlt,
 NaturalConicBi
   (Inv2 (HomDisjEmpty Mlt Op))
   c
   Mlt
   'Injective
   d
   ('Chain t)
   (n + 1)
   n) =>
XOrtSite r x
-> XEligibleConeG c s (ToPerspective r) d ('Chain t) (n + 1) n x
xecOrtSiteChain (XOrtOrientation N -> XOrtSite 'From N
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom (XOrtOrientation N -> XOrtSite 'From N)
-> XOrtOrientation N -> XOrtSite 'From N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X N -> XOrtOrientation N
forall q. Total q => X q -> XOrtOrientation q
xoTtl (X N -> XOrtOrientation N) -> X N -> XOrtOrientation N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
100)
      xecfMaxToN :: XEligibleConeFactorG Cone s (ToPerspective 'From) d t n m N
xecfMaxToN = XOrtSite 'From N
-> XEligibleConeFactorG Cone s (ToPerspective 'From) d t n m N
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (r :: Site) x s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Conic c =>
XOrtSite r x
-> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite (XOrtOrientation N -> XOrtSite 'From N
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom (XOrtOrientation N -> XOrtSite 'From N)
-> XOrtOrientation N -> XOrtSite 'From N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X N -> XOrtOrientation N
forall q. Total q => X q -> XOrtOrientation q
xoTtl (X N -> XOrtOrientation N) -> X N -> XOrtOrientation N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
100)

      maxFromN :: Maxima 'From n N
maxFromN     = W n -> Proxy N -> Maxima 'From n N
forall x (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative x =>
p n -> f x -> Maxima 'From n x
maximaFrom' W n
n' (Proxy N
forall {k} (t :: k). Proxy t
Proxy :: Proxy N)
      xecMaxFromN :: XEligibleConeG
  Cone Mlt (ToPerspective 'From) Diagram ('Chain 'From) (n + 1) n N
xecMaxFromN  = XOrtSite 'From N
-> XEligibleConeG
     Cone Mlt (ToPerspective 'From) Diagram ('Chain 'From) (n + 1) n N
forall x s
       (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: Site) (n :: N')
       (r :: Site).
(Multiplicative x, s ~ Mlt,
 NaturalConicBi
   (Inv2 (HomDisjEmpty Mlt Op))
   c
   Mlt
   'Injective
   d
   ('Chain t)
   (n + 1)
   n) =>
XOrtSite r x
-> XEligibleConeG c s (ToPerspective r) d ('Chain t) (n + 1) n x
xecOrtSiteChain (XOrtOrientation N -> XOrtSite 'From N
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom (XOrtOrientation N -> XOrtSite 'From N)
-> XOrtOrientation N -> XOrtSite 'From N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X N -> XOrtOrientation N
forall q. Total q => X q -> XOrtOrientation q
xoTtl (X N -> XOrtOrientation N) -> X N -> XOrtOrientation N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
100)
      xecfMaxFromN :: XEligibleConeFactorG Cone s (ToPerspective 'From) d t n m N
xecfMaxFromN = XOrtSite 'From N
-> XEligibleConeFactorG Cone s (ToPerspective 'From) d t n m N
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       (r :: Site) x s (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Conic c =>
XOrtSite r x
-> XEligibleConeFactorG c s (ToPerspective r) d t n m x
xecfOrtSite (XOrtOrientation N -> XOrtSite 'From N
forall q. Oriented q => XOrtOrientation q -> XOrtSite 'From q
xoFrom (XOrtOrientation N -> XOrtSite 'From N)
-> XOrtOrientation N -> XOrtSite 'From N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X N -> XOrtOrientation N
forall q. Total q => X q -> XOrtOrientation q
xoTtl (X N -> XOrtOrientation N) -> X N -> XOrtOrientation N
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ N -> N -> X N
xNB N
0 N
100)