{-# LANGUAGE NoImplicitPrelude #-}

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

-- |

-- Module      : OAlg.Limes.Cone.Conic.Core

-- Description : basic definition for objects with a naturally underlying cone.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- basic definition for objects with a naturally underlying cone.

module OAlg.Limes.Cone.Conic.Core
  (
    -- * Conic

    Conic(..)
  , ConeG(..)

    -- * Natural

  , NaturalConic
  , crohS
  ) where

import Data.Kind

import OAlg.Prelude

import OAlg.Category.SDuality
import OAlg.Category.NaturalTransformable

import OAlg.Data.Either

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

import OAlg.Hom.Oriented
import OAlg.Hom.Multiplicative

import OAlg.Limes.Cone.Definition

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

-- Conic -


-- | object @__c__@ having an underlying 'Cone'.

class Conic c where
  cone :: c s p d t n m x -> Cone s p d t n m x

instance Conic Cone where cone :: forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
Cone s p d t n m x -> Cone s p d t n m x
cone = Cone s p d t n m x -> Cone s p d t n m x
forall x. x -> x
id

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

-- ConeG -


-- | wrapper for 'Conic'-objects.

newtype ConeG (c :: Type -> Perspective
                 -> (DiagramType -> N' -> N' -> Type -> Type)
                 -> DiagramType -> N' -> N'
                 -> Type
                 -> Type
              ) s p d t n m x
  = ConeG (c s p d t n m x)
  deriving (Int -> ConeG c s p d t n m x -> ShowS
[ConeG c s p d t n m x] -> ShowS
ConeG c s p d t n m x -> String
(Int -> ConeG c s p d t n m x -> ShowS)
-> (ConeG c s p d t n m x -> String)
-> ([ConeG c s p d t n m x] -> ShowS)
-> Show (ConeG c s p d t n m x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
Int -> ConeG c s p d t n m x -> ShowS
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
[ConeG c s p d t n m x] -> ShowS
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
ConeG c s p d t n m x -> String
$cshowsPrec :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
Int -> ConeG c s p d t n m x -> ShowS
showsPrec :: Int -> ConeG c s p d t n m x -> ShowS
$cshow :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
ConeG c s p d t n m x -> String
show :: ConeG c s p d t n m x -> String
$cshowList :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Show (c s p d t n m x) =>
[ConeG c s p d t n m x] -> ShowS
showList :: [ConeG c s p d t n m x] -> ShowS
Show,ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
(ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool)
-> (ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool)
-> Eq (ConeG c s p d t n m x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Eq (c s p d t n m x) =>
ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
$c== :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Eq (c s p d t n m x) =>
ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
== :: ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
$c/= :: forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (p :: Perspective) (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N') x.
Eq (c s p d t n m x) =>
ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
/= :: ConeG c s p d t n m x -> ConeG c s p d t n m x -> Bool
Eq)

type instance Dual1 (ConeG c s p d t n m) = ConeG c s (Dual p) d (Dual t) n m

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

-- croh -


-- | the underlying cone.

croh :: Conic c => ConeG c s p d t n m x -> ConeG Cone s p d t n m x
croh :: 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 =>
ConeG c s p d t n m x -> ConeG Cone s p d t n m x
croh (ConeG c s p d t n m x
c) = Cone s p d t n m x -> ConeG 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.
c s p d t n m x -> ConeG c s p d t n m x
ConeG (c s p d t n m x -> Cone s p d t n m 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 s p d t n m x
c)

instance Conic c => Natural r (->) (ConeG c s p d t n m) (ConeG Cone s p d t n m) where
  roh :: forall x.
Struct r x -> ConeG c s p d t n m x -> ConeG Cone s p d t n m x
roh Struct r x
_ = ConeG c s p d t n m x -> ConeG 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 =>
ConeG c s p d t n m x -> ConeG Cone s p d t n m x
croh

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

-- crohS -


-- | natural assocition induced by 'croh' betewwn @'SDualBi' ('ConeG' __c s p d t n m__)@ and

-- @'SDualBi' ('Cone' __s p d t n m__)@.

crohS :: Conic c => SDualBi (ConeG c s p d t n m) x -> SDualBi (ConeG Cone s p d t n m) x
crohS :: 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 =>
SDualBi (ConeG c s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
crohS (SDualBi (Right1 ConeG c s p d t n m x
c)) = Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s p d t n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 (ConeG c s p d t n m x -> ConeG 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 =>
ConeG c s p d t n m x -> ConeG Cone s p d t n m x
croh ConeG c s p d t n m x
c))
crohS (SDualBi (Left1 Dual1 (ConeG c s p d t n m) x
c')) = Either1 (Dual1 (ConeG Cone s p d t n m)) (ConeG Cone s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (ConeG Cone s (Dual p) d (Dual t) n m x
-> Either1
     (ConeG Cone s (Dual p) d (Dual t) n m) (ConeG Cone s p d t n m) x
forall (f :: * -> *) x (g :: * -> *). f x -> Either1 f g x
Left1 (ConeG c s (Dual p) d (Dual t) n m x
-> ConeG Cone s (Dual p) d (Dual 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 =>
ConeG c s p d t n m x -> ConeG Cone s p d t n m x
croh Dual1 (ConeG c s p d t n m) x
ConeG c s (Dual p) d (Dual t) n m x
c'))

instance Conic c
  => Natural r (->) (SDualBi (ConeG c s p d t n m)) (SDualBi (ConeG Cone s p d t n m)) where
  roh :: forall x.
Struct r x
-> SDualBi (ConeG c s p d t n m) x
   -> SDualBi (ConeG Cone s p d t n m) x
roh Struct r x
_ = SDualBi (ConeG c s p d t n m) x
-> SDualBi (ConeG 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 =>
SDualBi (ConeG c s p d t n m) x
-> SDualBi (ConeG Cone s p d t n m) x
crohS

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

-- NaturalConic -


-- | natural transformation for 'Conic' objects from @'SDualBi' ('ConeG' __c s p d t n m__)@ to

-- @'SDualBi' ('Cone' __s p d t n m__)@.

class
  ( Conic c
  , HomMultiplicativeDisjunctive h
  , FunctorialOriented h
  , NaturalDiagrammatic h d t n m
  , NaturalTransformable h (->) (SDualBi (ConeG c s p d t n m)) (SDualBi (ConeG Cone s p d t n m))
  , p ~ Dual (Dual p)
  )
  => NaturalConic h c s p d t n m