{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Exact.ZeroPoint

-- Description : zero points.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- zero points within a 'Distributive' structure.

module OAlg.Limes.Exact.ZeroPoint
  (
    -- * Zero Point

    ZeroPoint(..), isZeroPoint

    -- * Limes

  , zrPointTerminal, zrPointTerminals
  , zrPointInitial, zrPointInitials
  ) where

import OAlg.Prelude

import OAlg.Category.SDuality

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

import OAlg.Structure.Oriented
import OAlg.Structure.Additive
import OAlg.Structure.Multiplicative
import OAlg.Structure.Distributive

import OAlg.Hom.Distributive

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

import OAlg.Entity.Diagram

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

-- ZeroPoint -


-- | predicate for a zero point within a 'Distributive' structure @__x__@.

--

-- __Property__ Let @'ZeroPoint' z@ be in @'ZeroPoint' __x__@ within a

-- 'Distributive' structure @__x__@, then holds:

--

-- (1) @'zero' (z ':>' z) '==' 'one' z@,

newtype ZeroPoint x = ZeroPoint (Point x)

deriving instance ShowPoint x => Show (ZeroPoint x)
deriving instance EqPoint x => Eq (ZeroPoint x)

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

-- isZeroPoint -


-- | testing of being a zero point accroding to the given proxy type.

isZeroPoint :: Distributive x => q x -> Point x -> Bool
isZeroPoint :: forall x (q :: * -> *). Distributive x => q x -> Point x -> Bool
isZeroPoint q x
q Point x
p = q x -> Root x -> x
forall a (p :: * -> *). Additive a => p a -> Root a -> a
zero' q x
q (Point x
p Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:> Point x
p) x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== Point x -> x
forall c. Multiplicative c => Point c -> c
one Point x
p

instance Distributive x => Validable (ZeroPoint x) where
  valid :: ZeroPoint x -> Statement
valid z :: ZeroPoint x
z@(ZeroPoint Point x
p) = String -> Label
Label String
"ZeroPoint" Label -> Statement -> Statement
:<=>: ZeroPoint x -> Point x -> Bool
forall x (q :: * -> *). Distributive x => q x -> Point x -> Bool
isZeroPoint ZeroPoint x
z Point x
p Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"p"String -> String -> Parameter
:=Point x -> String
forall a. Show a => a -> String
show Point x
p]

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

-- zrPointTerminal -


-- | a zero point as terminal point.

zrPointTerminal :: Distributive x => ZeroPoint x -> TerminalPoint x
zrPointTerminal :: forall x. Distributive x => ZeroPoint x -> TerminalPoint x
zrPointTerminal (ZeroPoint Point x
z) = Cone Mlt 'Projective Diagram 'Empty N0 N0 x
-> (Cone Mlt 'Projective Diagram 'Empty N0 N0 x -> x)
-> LimesG Cone Mlt 'Projective Diagram 'Empty 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 (Point x -> Cone Mlt 'Projective Diagram 'Empty N0 N0 x
forall x. Multiplicative x => Point x -> TerminalCone x
trmCone Point x
z) (Point x -> Cone Mlt 'Projective Diagram 'Empty N0 N0 x -> x
forall x. Distributive x => Point x -> TerminalCone x -> x
univ Point x
z) where
  univ :: Distributive x => Point x -> TerminalCone x -> x
  univ :: forall x. Distributive x => Point x -> TerminalCone x -> x
univ Point x
z (ConeProjective Diagram 'Empty N0 N0 x
DiagramEmpty Point x
p FinList N0 x
_) = Root x -> x
forall a. Additive a => Root a -> a
zero (Point x
pPoint x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:>Point x
z)

-- | the induced terminals.

zrPointTerminals :: Distributive x => ZeroPoint x -> Terminals x
zrPointTerminals :: forall x. Distributive x => ZeroPoint x -> Terminals x
zrPointTerminals = (Diagram 'Empty N0 N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x)
-> Terminals 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 'Empty N0 N0 x
  -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x)
 -> Terminals x)
-> (ZeroPoint x
    -> Diagram 'Empty N0 N0 x
    -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x)
-> ZeroPoint x
-> Terminals 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 Cone Mlt 'Projective Diagram 'Empty N0 N0 x
-> Diagram 'Empty N0 N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x
forall b a. b -> a -> b
const (LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x
 -> Diagram 'Empty N0 N0 x
 -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x)
-> (ZeroPoint x
    -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x)
-> ZeroPoint x
-> Diagram 'Empty N0 N0 x
-> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 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
. ZeroPoint x -> LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0 x
forall x. Distributive x => ZeroPoint x -> TerminalPoint x
zrPointTerminal

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

-- zrPointInitial -


-- | a zero point as initial point.

zrPointInitial :: Distributive x => ZeroPoint x -> InitialPoint x
zrPointInitial :: forall x. Distributive x => ZeroPoint x -> InitialPoint x
zrPointInitial (ZeroPoint Point x
z) = LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x
intPnt where
  Contravariant2 IsoO Dst Op x (Op x)
i        = Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
forall x.
Distributive x =>
Variant2 'Contravariant (Inv2 (HomDisjEmpty Dst Op)) x (Op x)
toDualOpDst
  
  trmPnt :: TerminalPoint (Op x)
trmPnt                  = ZeroPoint (Op x) -> TerminalPoint (Op x)
forall x. Distributive x => ZeroPoint x -> TerminalPoint x
zrPointTerminal (Point (Op x) -> ZeroPoint (Op x)
forall x. Point x -> ZeroPoint x
ZeroPoint Point x
Point (Op x)
z) -- z as a zero point in Op x

  SDualBi (Right1 LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x
intPnt) = Inv2 (HomDisjEmpty Dst Op) (Op x) x
-> SDualBi (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0) (Op x)
-> SDualBi (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0) x
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF (IsoO Dst Op x (Op x) -> Inv2 (HomDisjEmpty Dst Op) (Op x) x
forall (c :: * -> * -> *) x y. Inv2 c x y -> Inv2 c y x
inv2 IsoO Dst Op x (Op x)
i) (Either1
  (Dual1 (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0))
  (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0)
  (Op x)
-> SDualBi (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0) (Op x)
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (TerminalPoint (Op x)
-> Either1
     (LimesG Cone Mlt 'Projective Diagram 'Empty N0 N0)
     (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0)
     (Op x)
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 TerminalPoint (Op x)
trmPnt))

-- | the induced initials.

zrPointInitials :: Distributive x => ZeroPoint x -> Initials x
zrPointInitials :: forall x. Distributive x => ZeroPoint x -> Initials x
zrPointInitials = (Diagram 'Empty N0 N0 x
 -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x)
-> Initials 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 'Empty N0 N0 x
  -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x)
 -> Initials x)
-> (ZeroPoint x
    -> Diagram 'Empty N0 N0 x
    -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x)
-> ZeroPoint x
-> Initials 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 Cone Mlt 'Injective Diagram 'Empty N0 N0 x
-> Diagram 'Empty N0 N0 x
-> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x
forall b a. b -> a -> b
const (LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x
 -> Diagram 'Empty N0 N0 x
 -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x)
-> (ZeroPoint x
    -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x)
-> ZeroPoint x
-> Diagram 'Empty N0 N0 x
-> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 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
. ZeroPoint x -> LimesG Cone Mlt 'Injective Diagram 'Empty N0 N0 x
forall x. Distributive x => ZeroPoint x -> InitialPoint x
zrPointInitial