{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}

-- |
-- 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, Minimum, MinimumCone, MinimumDiagram
  , minimaTo, minimaFrom

    -- * Maxima
  , Maxima, Maximum, MaximumCone, MaximumDiagram
  , maximaTo, maximaTo', maximaFrom, maximaFrom'

    -- * Duality
  , maxLimitsDualityTo, maxLimitsDualityFrom

  )
  where

import Data.Typeable

import OAlg.Prelude

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

import OAlg.Structure.Multiplicative

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


--------------------------------------------------------------------------------
-- Minima -

-- | 'Diagram' for a minimum.
type MinimumDiagram t n = Diagram (Chain t) (n+1) n

-- | 'Cone' for a minimum.
type MinimumCone t n = Cone Mlt Projective (Chain t) (n+1) n

-- | minimum as 'Limes'.
type Minimum t n = Limes Mlt Projective (Chain t) (n+1) n

-- | minima for a 'Multiplicative' structure.
type Minima t n = Limits Mlt Projective (Chain t) (n+1) n

--------------------------------------------------------------------------------
-- minima -

-- | minima according to @'Chain' 'To'@.
minimaTo :: Multiplicative a => Minima To n a
minimaTo :: forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'To n a -> Minimum 'To n a
lMin where
  lMin :: Multiplicative a => MinimumDiagram To n a -> Minimum To n a
  lMin :: forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'To n a -> Minimum 'To n a
lMin MinimumDiagram 'To n a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
l forall {n :: N'} {a}.
Cone Mlt 'Projective ('Chain 'To) ('S n) n a -> a
u where
    l :: Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
l = forall a (n :: N').
Multiplicative a =>
FactorChain 'To n a
-> Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
cnPrjChainTo (forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain (forall c. Multiplicative c => Point c -> c
one (forall a (n :: N') (m :: N').
Oriented a =>
Diagram ('Chain 'To) n m a -> Point a
chnToStart MinimumDiagram 'To n a
d)) MinimumDiagram 'To n a
d)
    u :: Cone Mlt 'Projective ('Chain 'To) ('S n) n a -> a
u Cone Mlt 'Projective ('Chain 'To) ('S n) n a
c = a
f where FactorChain a
f Diagram ('Chain 'To) (n + 1) n a
_ = forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'To) (n + 1) n a
-> FactorChain 'To n a
cnPrjChainToInv Cone Mlt 'Projective ('Chain 'To) ('S n) n a
c

-- | minima according to @'Chain' 'From'@.
minimaFrom :: Multiplicative a => Minima From n a
minimaFrom :: forall a (n :: N'). Multiplicative a => Minima 'From n a
minimaFrom = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
(Diagram t n m a -> Limes s p t n m a) -> Limits s p t n m a
Limits forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'From n a -> Minimum 'From n a
lMin where
  lMin :: Multiplicative a => MinimumDiagram From n a -> Minimum From n a
  lMin :: forall a (n :: N').
Multiplicative a =>
MinimumDiagram 'From n a -> Minimum 'From n a
lMin MinimumDiagram 'From n a
d = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Projective t n m a
-> (Cone s 'Projective t n m a -> a) -> Limes s 'Projective t n m a
LimesProjective Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
l forall {n :: N'} {a}.
Cone Mlt 'Projective ('Chain 'From) ('S n) n a -> a
u where
    l :: Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
l = forall a (n :: N').
Multiplicative a =>
FactorChain 'From n a
-> Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
cnPrjChainFrom (forall (s :: Site) (n :: N') a.
a -> Diagram ('Chain s) (n + 1) n a -> FactorChain s n a
FactorChain (forall c. Multiplicative c => Point c -> c
one (forall (n :: N') (m :: N') a.
Diagram ('Chain 'From) n m a -> Point a
chnFromStart MinimumDiagram 'From n a
d)) MinimumDiagram 'From n a
d)
    u :: Cone Mlt 'Projective ('Chain 'From) ('S n) n a -> a
u Cone Mlt 'Projective ('Chain 'From) ('S n) n a
c = a
f where FactorChain a
f Diagram ('Chain 'From) (n + 1) n a
_ = forall (n :: N') a.
Cone Mlt 'Projective ('Chain 'From) (n + 1) n a
-> FactorChain 'From n a
cnPrjChainFromInv Cone Mlt 'Projective ('Chain 'From) ('S n) n a
c

--------------------------------------------------------------------------------
-- Maxima -

-- | 'Diagram' for a maximum.
type MaximumDiagram t n = Diagram (Chain t) (n+1) n

-- | 'Cone' for a maximum.
type MaximumCone t n = Cone Mlt Injective (Chain t) (n+1) n

-- | maximum as a 'Limes'.
type Maximum t n = Limes Mlt Injective (Chain t) (n+1) n

-- | maxima for a 'Multiplicative' structure.
type Maxima t n = Limits Mlt Injective (Chain t) (n+1) n

--------------------------------------------------------------------------------
-- Duality - Max -

-- | duality between @'Maxima' 'To'@ and @'Minima' 'From'@.
maxLimitsDualityTo :: Multiplicative a => LimitsDuality Mlt (Maxima To n) (Minima From n) a
maxLimitsDualityTo :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'To n) (Minima 'From n) a
maxLimitsDualityTo = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

-- | duality between @'Maxima' 'From'@ and @'Minima' 'To'@.
maxLimitsDualityFrom :: Multiplicative a
  => LimitsDuality Mlt (Maxima From n) (Minima To n) a
maxLimitsDualityFrom :: forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'From n) (Minima 'To n) a
maxLimitsDualityFrom = forall s a (f :: * -> *) (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') (g :: * -> *).
ConeStruct s a
-> (f a :~: Limits s p t n m a)
-> (g (Op a) :~: Dual (Limits s p t n m a))
-> (Dual (Dual p) :~: p)
-> (Dual (Dual t) :~: t)
-> LimitsDuality s f g a
LimitsDuality forall a. Multiplicative a => ConeStruct Mlt a
ConeStructMlt forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl forall {k} (a :: k). a :~: a
Refl

--------------------------------------------------------------------------------
-- maxima -

-- | maxima according to @'Chain' 'To'@.
maximaTo :: Multiplicative a => Maxima To n a
maximaTo :: forall a (n :: N'). Multiplicative a => Maxima 'To n a
maximaTo = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'To n) (Minima 'From n) a
maxLimitsDualityTo forall a (n :: N'). Multiplicative a => Minima 'From n a
minimaFrom

-- | maxima according to @'Chain' 'From'@.
maximaFrom :: Multiplicative a => Maxima From n a
maximaFrom :: forall a (n :: N'). Multiplicative a => Maxima 'From n a
maximaFrom = forall s (f :: * -> *) (g :: * -> *) a.
LimitsDuality s f g a -> g (Op a) -> f a
lmsFromOp forall a (n :: N').
Multiplicative a =>
LimitsDuality Mlt (Maxima 'From n) (Minima 'To n) a
maxLimitsDualityFrom forall a (n :: N'). Multiplicative a => Minima 'To n a
minimaTo

-- | maxima according to @'Chain' 'To'@ given by two proxy types.
maximaTo' :: Multiplicative a => p n -> f a -> Maxima To n a
maximaTo' :: forall a (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative a =>
p n -> f a -> Maxima 'To n a
maximaTo' p n
_ f a
_ = forall a (n :: N'). Multiplicative a => Maxima 'To n a
maximaTo

-- | maxima according to @'Chain' 'From'@ given by two proxy types.
maximaFrom' :: Multiplicative a => p n -> f a -> Maxima From n a
maximaFrom' :: forall a (p :: N' -> *) (n :: N') (f :: * -> *).
Multiplicative a =>
p n -> f a -> Maxima 'From n a
maximaFrom' p n
_ f a
_ = forall a (n :: N'). Multiplicative a => Maxima 'From n a
maximaFrom