{-# LANGUAGE NoImplicitPrelude #-}

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


-- |
-- Module      : OAlg.Entity.Slice.Definition
-- Description : definition of slicing a multiplicative structure
-- Copyright   : (c) Erich Gut
-- License     : BSD3
-- Maintainer  : zerich.gut@gmail.com
-- 
-- definition of slicing a 'Multiplicative' structures according a given indexed 'Point'.
module OAlg.Entity.Slice.Definition
  (
    -- * Slice
    Slice(..), slice

    -- * Factor
  , SliceFactor(..), slfDrop
  
    -- * Sliced
  , Sliced(..)

    -- * Hom
  , SliceFactorDrop(..)

    -- * Limes

  , DiagramSlicedCenter(..)
  , LimesSlicedTip(..), lstLimes

    -- ** Projective
  , slfTerminalPoint
  , slfPullback

    -- ** Injective
  , slfLimitsInjective

    -- * X
  , xSliceTo, xSliceFrom
  , xosXOrtSiteToSliceFactorTo
  , xosXOrtSiteFromSliceFactorFrom

  ) where

import Control.Monad

import Data.Typeable
import Data.List ((++))

import OAlg.Prelude

import OAlg.Data.Singleton

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative as M

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

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

import OAlg.Entity.Natural hiding ((++))
import OAlg.Entity.FinList hiding ((++))
import OAlg.Entity.Diagram

import OAlg.Data.Symbol
--------------------------------------------------------------------------------
-- Sliced -

-- | Slicing a 'Multiplicative' structures at the 'Point' given by the type of the index
--  __@i@__. 
--
--  __Note__ The constraint @'Singleton1' __i__@ ensures that the distinguished point
--  depends only on the type __@i c@__.
class (Entity1 i, Singleton1 i) => Sliced i c where
  -- | the distingueished point of the given index type @__i__@.
  slicePoint :: i c -> Point c


instance Sliced i c => Sliced i (Op c) where
  slicePoint :: i (Op c) -> Point (Op c)
slicePoint i (Op c)
i = forall (p :: * -> *) c. p (Op c) -> Point c -> Point (Op c)
to i (Op c)
i forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c. Singleton1 i => i (Op c) -> i c
fo i (Op c)
i where
    
    fo :: Singleton1 i => i (Op c) -> i c
    fo :: forall (i :: * -> *) c. Singleton1 i => i (Op c) -> i c
fo i (Op c)
_ = forall (s :: * -> *) x. Singleton1 s => s x
unit1

    to :: p (Op c) -> Point c -> Point (Op c)
    to :: forall (p :: * -> *) c. p (Op c) -> Point c -> Point (Op c)
to p (Op c)
_ = forall x. x -> x
id

--------------------------------------------------------------------------------
-- Slice -

-- | slice over __@c@__ by a given 'Site' and indexed by @__i__@.
data Slice s i c where
  SliceFrom :: i c -> c -> Slice From i c
  SliceTo :: i c -> c -> Slice To i c

instance (Show1 i, Show c) => Show (Slice s i c) where
  show :: Slice s i c -> String
show (SliceFrom i c
i c
c) = String
"SliceFrom[" forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i forall a. [a] -> [a] -> [a]
++ String
"] (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show c
c forall a. [a] -> [a] -> [a]
++ String
")"
  show (SliceTo i c
i c
c)   = String
"SliceTo[" forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i forall a. [a] -> [a] -> [a]
++ String
"] (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show c
c forall a. [a] -> [a] -> [a]
++ String
")"
  
instance (Eq1 i, Eq c) => Eq (Slice s i c) where
  SliceFrom i c
i c
f == :: Slice s i c -> Slice s i c -> Bool
== SliceFrom i c
j c
g = forall (p :: * -> *) x. Eq1 p => p x -> p x -> Bool
eq1 i c
i i c
j forall b. Boolean b => b -> b -> b
&& c
f forall a. Eq a => a -> a -> Bool
== c
g
  SliceTo i c
i c
f == SliceTo i c
j c
g     = forall (p :: * -> *) x. Eq1 p => p x -> p x -> Bool
eq1 i c
i i c
j forall b. Boolean b => b -> b -> b
&& c
f forall a. Eq a => a -> a -> Bool
== c
g

--------------------------------------------------------------------------------
-- slice -

-- | the underlying slice.
slice :: Slice s i c -> c
slice :: forall (s :: Site) (i :: * -> *) c. Slice s i c -> c
slice (SliceFrom i c
_ c
p) = c
p
slice (SliceTo i c
_ c
p)   = c
p

--------------------------------------------------------------------------------
-- Slice - Dual -

type instance Dual (Slice s i c) = Slice (Dual s) i (Op c)

-- | to the dual 'Slice'.
coSlice :: Singleton1 i => Slice s i c -> Dual (Slice s i c)
coSlice :: forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
Slice s i c -> Dual (Slice s i c)
coSlice (SliceFrom i c
_ c
f) = forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo forall (s :: * -> *) x. Singleton1 s => s x
unit1 (forall x. x -> Op x
Op c
f)
coSlice (SliceTo i c
_ c
f)   = forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom forall (s :: * -> *) x. Singleton1 s => s x
unit1 (forall x. x -> Op x
Op c
f)


--------------------------------------------------------------------------------
-- Slice - Validable -

-- | validity of a 'Slice'.
relValidSlice :: (Oriented c, Sliced i c)
  => Slice s i c -> Statement
relValidSlice :: forall c (i :: * -> *) (s :: Site).
(Oriented c, Sliced i c) =>
Slice s i c -> Statement
relValidSlice s :: Slice s i c
s@(SliceFrom i c
i c
f)
  = [Statement] -> Statement
And [ forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 i c
i
        , forall a. Validable a => a -> Statement
valid c
f
        , let p :: Point c
p = forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i in
            (forall q. Oriented q => q -> Point q
start c
f forall a. Eq a => a -> a -> Bool
== Point c
p)Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"s"String -> String -> Parameter
:=forall a. Show a => a -> String
show Slice s i c
s]
        ]
relValidSlice Slice s i c
s                 = forall c (i :: * -> *) (s :: Site).
(Oriented c, Sliced i c) =>
Slice s i c -> Statement
relValidSlice (forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
Slice s i c -> Dual (Slice s i c)
coSlice Slice s i c
s)


instance (Oriented c, Sliced i c) => Validable (Slice s i c) where
  valid :: Slice s i c -> Statement
valid Slice s i c
s = String -> Label
Label String
"Slice" Label -> Statement -> Statement
:<=>: forall c (i :: * -> *) (s :: Site).
(Oriented c, Sliced i c) =>
Slice s i c -> Statement
relValidSlice Slice s i c
s


instance (Oriented c, Sliced i c, Typeable s) => Entity (Slice s i c)

--------------------------------------------------------------------------------
-- SliceFactor -

-- | factor between two slices.
--
--  __Property__ Let @SliceFactor a b f@ be in
-- @'SliceFactor' __s__ __i__ __c__@ for a 'Multiplicative' structure __@c@__
-- constrained by @'Sliced' __i__ __c__@ then holds:
--
-- (1) If @a@ matches @'SliceFrom' _ a'@ then holds: Let @'SliceFrom' _ b' = b@ in
--
--     (1) @'orientation' f '==' 'end' a' ':>' 'end' b'@.
--
--     (2) @b' '==' f 'M.*' a'@.
--
-- (2) If @a@ matches @'SliceTo' _ a'@ then holds: Let @'SliceTo' _ b' = b@ in
--
--     (1) @'orientation' f '==' 'start' a' ':>' 'start' b'@.
--
--     (2) @a' '==' b' 'M.*' f@ .
data SliceFactor s i c = SliceFactor (Slice s i c) (Slice s i c) c
  deriving (Int -> SliceFactor s i c -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
Int -> SliceFactor s i c -> ShowS
forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
[SliceFactor s i c] -> ShowS
forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
SliceFactor s i c -> String
showList :: [SliceFactor s i c] -> ShowS
$cshowList :: forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
[SliceFactor s i c] -> ShowS
show :: SliceFactor s i c -> String
$cshow :: forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
SliceFactor s i c -> String
showsPrec :: Int -> SliceFactor s i c -> ShowS
$cshowsPrec :: forall (s :: Site) (i :: * -> *) c.
(Show1 i, Show c) =>
Int -> SliceFactor s i c -> ShowS
Show,SliceFactor s i c -> SliceFactor s i c -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: Site) (i :: * -> *) c.
(Eq1 i, Eq c) =>
SliceFactor s i c -> SliceFactor s i c -> Bool
/= :: SliceFactor s i c -> SliceFactor s i c -> Bool
$c/= :: forall (s :: Site) (i :: * -> *) c.
(Eq1 i, Eq c) =>
SliceFactor s i c -> SliceFactor s i c -> Bool
== :: SliceFactor s i c -> SliceFactor s i c -> Bool
$c== :: forall (s :: Site) (i :: * -> *) c.
(Eq1 i, Eq c) =>
SliceFactor s i c -> SliceFactor s i c -> Bool
Eq)

--------------------------------------------------------------------------------
-- slfDrop -

-- | the underlying factor.
slfDrop :: SliceFactor s i c -> c       
slfDrop :: forall (s :: Site) (i :: * -> *) c. SliceFactor s i c -> c
slfDrop (SliceFactor Slice s i c
_ Slice s i c
_ c
f) = c
f

--------------------------------------------------------------------------------
-- SliceFactor - Dual -

type instance Dual (SliceFactor s i c) = SliceFactor (Dual s) i (Op c)

-- | to the dual 'SliceFactor'.
coSliceFactor :: Singleton1 i
  => SliceFactor s i c -> Dual (SliceFactor s i c)
coSliceFactor :: forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
SliceFactor s i c -> Dual (SliceFactor s i c)
coSliceFactor (SliceFactor Slice s i c
a Slice s i c
b c
t)
  = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
Slice s i c -> Dual (Slice s i c)
coSlice Slice s i c
b) (forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
Slice s i c -> Dual (Slice s i c)
coSlice Slice s i c
a) (forall x. x -> Op x
Op c
t)

--------------------------------------------------------------------------------
-- SliceTransformatin - Entity -

-- | validity of a 'SliceFactor'.
relValidSliceFactor :: (Multiplicative c, Sliced i c) => SliceFactor s i c -> Statement
relValidSliceFactor :: forall c (i :: * -> *) (s :: Site).
(Multiplicative c, Sliced i c) =>
SliceFactor s i c -> Statement
relValidSliceFactor (SliceFactor a :: Slice s i c
a@(SliceFrom i c
_ c
a') b :: Slice s i c
b@(SliceFrom i c
_ c
b') c
t)
  = [Statement] -> Statement
And [ forall a. Validable a => a -> Statement
valid Slice s i c
a
        , forall a. Validable a => a -> Statement
valid Slice s i c
b
        , forall a. Validable a => a -> Statement
valid c
t
        , String -> Label
Label String
"1.1" Label -> Statement -> Statement
:<=>: (forall q. Oriented q => q -> Orientation (Point q)
orientation c
t forall a. Eq a => a -> a -> Bool
== forall q. Oriented q => q -> Point q
end c
a' forall p. p -> p -> Orientation p
:> forall q. Oriented q => q -> Point q
end c
b')
            Bool -> Message -> Statement
:?> Message
prm
        , String -> Label
Label String
"1.2" Label -> Statement -> Statement
:<=>: (c
b' forall a. Eq a => a -> a -> Bool
== c
tforall c. Multiplicative c => c -> c -> c
*c
a') Bool -> Message -> Statement
:?> Message
prm
        ] where prm :: Message
prm = [Parameter] -> Message
Params [String
"(a,b,t)"String -> String -> Parameter
:=forall a. Show a => a -> String
show (Slice s i c
a,Slice s i c
b,c
t)]
relValidSliceFactor SliceFactor s i c
t = forall c (i :: * -> *) (s :: Site).
(Multiplicative c, Sliced i c) =>
SliceFactor s i c -> Statement
relValidSliceFactor (forall (i :: * -> *) (s :: Site) c.
Singleton1 i =>
SliceFactor s i c -> Dual (SliceFactor s i c)
coSliceFactor SliceFactor s i c
t)

instance (Multiplicative c, Sliced i c) => Validable (SliceFactor s i c) where
  valid :: SliceFactor s i c -> Statement
valid SliceFactor s i c
t = String -> Label
Label String
"SliceFactor"
    Label -> Statement -> Statement
:<=>: forall c (i :: * -> *) (s :: Site).
(Multiplicative c, Sliced i c) =>
SliceFactor s i c -> Statement
relValidSliceFactor SliceFactor s i c
t

instance (Multiplicative c, Sliced i c, Typeable s) => Entity (SliceFactor s i c)

--------------------------------------------------------------------------------
-- SliceFactor - Multiplicative -

instance (Multiplicative c, Sliced i c, Typeable s) => Oriented (SliceFactor s i c) where
  type Point (SliceFactor s i c) = Slice s i c
  orientation :: SliceFactor s i c -> Orientation (Point (SliceFactor s i c))
orientation (SliceFactor Slice s i c
a Slice s i c
b c
_) = Slice s i c
a forall p. p -> p -> Orientation p
:> Slice s i c
b


instance (Multiplicative c, Sliced i c, Typeable s)
  => Multiplicative (SliceFactor s i c) where
  one :: Point (SliceFactor s i c) -> SliceFactor s i c
one Point (SliceFactor s i c)
s = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Point (SliceFactor s i c)
s Point (SliceFactor s i c)
s c
o where
    o :: c
o = case Point (SliceFactor s i c)
s of
      SliceFrom i c
_ c
f -> forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
end c
f)
      SliceTo i c
_ c
f   -> forall c. Multiplicative c => Point c -> c
one (forall q. Oriented q => q -> Point q
start c
f)

  SliceFactor Slice s i c
c Slice s i c
d c
f * :: SliceFactor s i c -> SliceFactor s i c -> SliceFactor s i c
* SliceFactor Slice s i c
a Slice s i c
b c
g
    | Slice s i c
c forall a. Eq a => a -> a -> Bool
== Slice s i c
b    = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice s i c
a Slice s i c
d (c
fforall c. Multiplicative c => c -> c -> c
*c
g)
    | Bool
otherwise = forall a e. Exception e => e -> a
throw ArithmeticException
NotMultiplicable

  npower :: SliceFactor s i c -> N -> SliceFactor s i c
npower (SliceFactor Slice s i c
a Slice s i c
b c
t) N
n = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice s i c
a Slice s i c
b (forall c. Multiplicative c => c -> N -> c
npower c
t N
n)

--------------------------------------------------------------------------------
-- SliceFactor - TerminalPoint -

-- | terminal point for factors sliced to a 'Point'.
slfTerminalPoint :: (Multiplicative c, Sliced i c) => TerminalPoint (SliceFactor To i c)
slfTerminalPoint :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
TerminalPoint (SliceFactor 'To i c)
slfTerminalPoint = 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 'Empty N0 N0 (SliceFactor 'To i c)
l Cone Mlt 'Projective 'Empty N0 N0 (SliceFactor 'To i c)
-> SliceFactor 'To i c
u where
  o  :: (Multiplicative c, Sliced i c) => i c -> Slice To i c
  o :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
i c -> Slice 'To i c
o i c
i = forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i (forall c. Multiplicative c => Point c -> c
one (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i))

  l :: Cone Mlt 'Projective 'Empty N0 N0 (SliceFactor 'To i c)
l = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective forall a. Diagram 'Empty N0 N0 a
DiagramEmpty (forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
i c -> Slice 'To i c
o forall (s :: * -> *) x. Singleton1 s => s x
unit1) forall a. FinList N0 a
Nil
  u :: Cone Mlt 'Projective 'Empty N0 N0 (SliceFactor 'To i c)
-> SliceFactor 'To i c
u (ConeProjective Diagram 'Empty N0 N0 (SliceFactor 'To i c)
_ s :: Point (SliceFactor 'To i c)
s@(SliceTo i c
_ c
f) FinList N0 (SliceFactor 'To i c)
Nil) = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Point (SliceFactor 'To i c)
s (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Projective 'Empty N0 N0 (SliceFactor 'To i c)
l) c
f

--------------------------------------------------------------------------------
-- DiagramSlicedCenter -

-- | predicate for a @'Star' __t__@ diagram with center 'Point' given by the index type
-- @__i__ __c__@.
--
-- __Property__ Let @'DiagramSlicedCenter' i d@ be in
-- @'DiagramSlicedCenter' __i__ __t__ __n__ __m__ __c__@ then holds:
-- @'slicePoint' i '==' 'dgCenter' d@.
data DiagramSlicedCenter i t n m c where
  DiagramSlicedCenter :: Sliced i c
    => i c
    -> Diagram (Star t) n m c
    -> DiagramSlicedCenter i t n m c

instance Oriented c => Show (DiagramSlicedCenter i t n m c) where
  show :: DiagramSlicedCenter i t n m c -> String
show (DiagramSlicedCenter i c
i Diagram ('Star t) n m c
d)
    = String
"DiagramSlicedCenter[" forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i forall a. [a] -> [a] -> [a]
++ String
"] (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Diagram ('Star t) n m c
d forall a. [a] -> [a] -> [a]
++ String
")"

instance Oriented c => Validable (DiagramSlicedCenter i t n m c) where
  valid :: DiagramSlicedCenter i t n m c -> Statement
valid (DiagramSlicedCenter i c
i Diagram ('Star t) n m c
d)
    = [Statement] -> Statement
And [ forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 i c
i
          , forall a. Validable a => a -> Statement
valid Diagram ('Star t) n m c
d
          , (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i forall a. Eq a => a -> a -> Bool
== forall (t :: Site) (n :: N') (m :: N') c.
Diagram ('Star t) n m c -> Point c
dgCenter Diagram ('Star t) n m c
d)
              Bool -> Message -> Statement
:?> [Parameter] -> Message
Params[String
"i"String -> String -> Parameter
:=forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i,String
"d"String -> String -> Parameter
:=forall a. Show a => a -> String
show Diagram ('Star t) n m c
d] 
          ]

--------------------------------------------------------------------------------
-- slfPullback -

-- | the induced pullback.
slfPullback :: Multiplicative c
  => Products n (SliceFactor To i c)
  -> DiagramSlicedCenter i To (n+1) n c -> Pullback n c
slfPullback :: forall c (n :: N') (i :: * -> *).
Multiplicative c =>
Products n (SliceFactor 'To i c)
-> DiagramSlicedCenter i 'To (n + 1) n c -> Pullback n c
slfPullback Products n (SliceFactor 'To i c)
prds (DiagramSlicedCenter i c
kc d :: Diagram ('Star 'To) (n + 1) n c
d@(DiagramSink Point c
_ FinList n c
as))
  = 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 ('Star 'To) ('S n) n c
lim Cone Mlt 'Projective ('Star 'To) ('S n) n c -> c
univ where
    pPrd :: FinList n (Slice 'To i c)
pPrd = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
kc) FinList n c
as
    dPrd :: Diagram 'Discrete n N0 (SliceFactor 'To i c)
dPrd = forall (n :: N') a. FinList n (Point a) -> Diagram 'Discrete n N0 a
DiagramDiscrete FinList n (Slice 'To i c)
pPrd
    LimesProjective Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
lPrd Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
-> SliceFactor 'To i c
uPrd = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Products n (SliceFactor 'To i c)
prds Diagram 'Discrete n N0 (SliceFactor 'To i c)
dPrd
    
    lim :: Cone Mlt 'Projective ('Star 'To) ('S n) n c
lim = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram ('Star 'To) (n + 1) n c
d (forall q. Oriented q => q -> Point q
end c
t) (c
tforall a (i :: N'). a -> FinList i a -> FinList (i + 1) a
:|FinList n c
cs) where
      SliceTo i c
_ c
t = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
lPrd
      cs :: FinList n c
cs = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(SliceFactor Slice 'To i c
_ Slice 'To i c
_ c
f) -> c
f) forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
lPrd 
      
    univ :: Cone Mlt 'Projective ('Star 'To) ('S n) n c -> c
univ (ConeProjective Diagram ('Star 'To) ('S n) n c
_ Point c
_ (c
t:|FinList n c
cs)) = c
u where
      SliceFactor Slice 'To i c
_ Slice 'To i c
_ c
u = Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
-> SliceFactor 'To i c
uPrd Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
cnPrd
      t' :: Slice 'To i c
t' = forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
kc c
t
      cnPrd :: Cone Mlt 'Projective 'Discrete n N0 (SliceFactor 'To i c)
cnPrd = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Projective t n m a
ConeProjective Diagram 'Discrete n N0 (SliceFactor 'To i c)
dPrd Slice 'To i c
t' FinList n (SliceFactor 'To i c)
csPrd
      csPrd :: FinList n (SliceFactor 'To i c)
csPrd = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'To i c
t')) (FinList n (Slice 'To i c)
pPrd forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` FinList n c
cs)

--------------------------------------------------------------------------------
-- LimesSlicedTip -

-- | predicate for a limes with a sliced tip of the universal cone.
--
--  __Property__ Let @'LimesSlicedTip' i l@ be in
-- @'LimesSlicedTip' __i__ __s__ __p__ __t__ __n__ __m__ __c__@ then holds:
-- @'tip' ('universalCone' l) '==' 'slicePoint' i@.
data LimesSlicedTip i s p t n m c where
  LimesSlicedTip :: Sliced i c => i c -> Limes s p t n m c -> LimesSlicedTip i s p t n m c

instance Oriented c => Show (LimesSlicedTip i s p t n m c) where
  show :: LimesSlicedTip i s p t n m c -> String
show (LimesSlicedTip i c
i Limes s p t n m c
l) = String
"LimesSlicedTip[" forall a. [a] -> [a] -> [a]
++ forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i forall a. [a] -> [a] -> [a]
++ String
"] (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Limes s p t n m c
l forall a. [a] -> [a] -> [a]
++ String
")"

instance (Oriented c, Validable (Limes s p t n m c))
  => Validable (LimesSlicedTip i s p t n m c) where
  valid :: LimesSlicedTip i s p t n m c -> Statement
valid (LimesSlicedTip i c
i Limes s p t n m c
l) = String -> Label
Label String
"LimesSlicedTip" Label -> Statement -> Statement
:<=>:
    [Statement] -> Statement
And [ forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 i c
i
        , forall a. Validable a => a -> Statement
valid Limes s p t n m c
l
        , (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limes s p t n m a -> Cone s p t n m a
universalCone Limes s p t n m c
l) forall a. Eq a => a -> a -> Bool
== forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i)
            Bool -> Message -> Statement
:?>[Parameter] -> Message
Params [String
"i"String -> String -> Parameter
:=forall (p :: * -> *) x. Show1 p => p x -> String
show1 i c
i, String
"l"String -> String -> Parameter
:= forall a. Show a => a -> String
show Limes s p t n m c
l]
        ]

--------------------------------------------------------------------------------
-- lstLimes -

-- | the underlying limes.
lstLimes :: LimesSlicedTip i s p t n m c -> Limes s p t n m c
lstLimes :: forall (i :: * -> *) s (p :: Perspective) (t :: DiagramType)
       (n :: N') (m :: N') c.
LimesSlicedTip i s p t n m c -> Limes s p t n m c
lstLimes (LimesSlicedTip i c
_ Limes s p t n m c
lim) = Limes s p t n m c
lim

--------------------------------------------------------------------------------
-- SliceFactorProjection -

-- | dropping a slice factor.
data SliceFactorDrop s x y where
  SliceFactorFromDrop
    :: (Multiplicative c, Sliced i c)
    => SliceFactorDrop From (SliceFactor From i c) c 
  SliceFactorToDrop
    :: (Multiplicative c, Sliced i c)
    => SliceFactorDrop To (SliceFactor To i c) c

--------------------------------------------------------------------------------
-- SliceFactorDrop - Entity -

deriving instance Show (SliceFactorDrop s x y)
instance Show2 (SliceFactorDrop s)

deriving instance Eq (SliceFactorDrop s x y)
instance Eq2 (SliceFactorDrop s)

instance Validable (SliceFactorDrop s x y) where
  valid :: SliceFactorDrop s x y -> Statement
valid SliceFactorDrop s x y
SliceFactorFromDrop = Statement
SValid
  valid SliceFactorDrop s x y
_                   = Statement
SValid
instance Validable2 (SliceFactorDrop s)

instance (Typeable s, Typeable x, Typeable y) => Entity (SliceFactorDrop s x y)
instance Typeable s => Entity2 (SliceFactorDrop s)

--------------------------------------------------------------------------------
-- SliceFactorDrop - Morphism -

instance Morphism (SliceFactorDrop s) where
  type ObjectClass (SliceFactorDrop s) = Mlt
  homomorphous :: forall x y.
SliceFactorDrop s x y
-> Homomorphous (ObjectClass (SliceFactorDrop s)) x y
homomorphous SliceFactorDrop s x y
SliceFactorFromDrop = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct
  homomorphous SliceFactorDrop s x y
SliceFactorToDrop   = forall s x. Structure s x => Struct s x
Struct forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: forall s x. Structure s x => Struct s x
Struct

instance EmbeddableMorphism (SliceFactorDrop s) Typ
instance EmbeddableMorphismTyp (SliceFactorDrop s)

instance EmbeddableMorphism (SliceFactorDrop s) Ort
instance EmbeddableMorphism (SliceFactorDrop s) Mlt

--------------------------------------------------------------------------------
-- SliceFactorDrop - Hom Mlt -

instance Applicative (SliceFactorDrop s) where
  amap :: forall a b. SliceFactorDrop s a b -> a -> b
amap SliceFactorDrop s a b
SliceFactorFromDrop = forall (s :: Site) (i :: * -> *) c. SliceFactor s i c -> c
slfDrop
  amap SliceFactorDrop s a b
SliceFactorToDrop   = forall (s :: Site) (i :: * -> *) c. SliceFactor s i c -> c
slfDrop

instance Typeable s => HomOriented (SliceFactorDrop s) where
  pmap :: forall a b. SliceFactorDrop s a b -> Point a -> Point b
pmap SliceFactorDrop s a b
SliceFactorFromDrop (SliceFrom i b
_ b
a) = forall q. Oriented q => q -> Point q
end b
a
  pmap SliceFactorDrop s a b
SliceFactorToDrop (SliceTo i b
_ b
a)     = forall q. Oriented q => q -> Point q
start b
a

instance Typeable s => HomMultiplicative (SliceFactorDrop s) where
  
--------------------------------------------------------------------------------
-- slfSliceIndex -

-- | the given attest for the slice index @__i__ __c__@ given by the diagram proxy.
slfSliceIndex :: Sliced i c => Diagram t n m (SliceFactor To i c) -> i c
slfSliceIndex :: forall (i :: * -> *) c (t :: DiagramType) (n :: N') (m :: N').
Sliced i c =>
Diagram t n m (SliceFactor 'To i c) -> i c
slfSliceIndex Diagram t n m (SliceFactor 'To i c)
_ = forall (s :: * -> *) x. Singleton1 s => s x
unit1

--------------------------------------------------------------------------------
-- dgSlfToSlicePoint -

-- | the diagram as a cone with its tip given by the 'slicePoint'.
dgSlfToSlicePoint :: (Multiplicative c, Sliced i c)
  => Diagram t n m (SliceFactor To i c) -> Cone Mlt Injective t n m c
dgSlfToSlicePoint :: forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Diagram t n m (SliceFactor 'To i c) -> Cone Mlt 'Injective t n m c
dgSlfToSlicePoint Diagram t n m (SliceFactor 'To i c)
d = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective Diagram t n m c
d' Point c
t FinList n c
cs where
  d' :: Diagram t n m c
d' = forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
SliceFactorDrop 'To (SliceFactor 'To i c) c
SliceFactorToDrop Diagram t n m (SliceFactor 'To i c)
d
  t :: Point c
t  = forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall (i :: * -> *) c (t :: DiagramType) (n :: N') (m :: N').
Sliced i c =>
Diagram t n m (SliceFactor 'To i c) -> i c
slfSliceIndex Diagram t n m (SliceFactor 'To i c)
d
  cs :: FinList n c
cs = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 forall (s :: Site) (i :: * -> *) c. Slice s i c -> c
slice forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m (SliceFactor 'To i c)
d

--------------------------------------------------------------------------------
-- slfLimesInjective -

-- | the induced 'Injective' limes for 'SliceFactor'. 
slfLimesInjective :: (Multiplicative c, Sliced i c)
  => Limits Mlt Injective t n m c
  -> Diagram t n m (SliceFactor To i c)
  -> Limes Mlt Injective t n m (SliceFactor To i c)
slfLimesInjective :: forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Limits Mlt 'Injective t n m c
-> Diagram t n m (SliceFactor 'To i c)
-> Limes Mlt 'Injective t n m (SliceFactor 'To i c)
slfLimesInjective Limits Mlt 'Injective t n m c
l Diagram t n m (SliceFactor 'To i c)
dgSlf = forall s (t :: DiagramType) (n :: N') (m :: N') a.
Cone s 'Injective t n m a
-> (Cone s 'Injective t n m a -> a) -> Limes s 'Injective t n m a
LimesInjective Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfLim Cone Mlt 'Injective t n m (SliceFactor 'To i c)
-> SliceFactor 'To i c
slfUniv where
  LimesInjective Cone Mlt 'Injective t n m c
lLim Cone Mlt 'Injective t n m c -> c
lUniv = forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Limits s p t n m a -> Diagram t n m a -> Limes s p t n m a
limes Limits Mlt 'Injective t n m c
l (forall (h :: * -> * -> *) a b (t :: DiagramType) (n :: N')
       (m :: N').
Hom Ort h =>
h a b -> Diagram t n m a -> Diagram t n m b
dgMap forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
SliceFactorDrop 'To (SliceFactor 'To i c) c
SliceFactorToDrop Diagram t n m (SliceFactor 'To i c)
dgSlf)
  
  slfLim :: Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfLim = forall a (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
Diagram t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective t n m a
ConeInjective Diagram t n m (SliceFactor 'To i c)
dgSlf Slice 'To i c
tSlf FinList n (SliceFactor 'To i c)
csSlf where
    tSlf :: Slice 'To i c
tSlf = forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo (forall (i :: * -> *) c (t :: DiagramType) (n :: N') (m :: N').
Sliced i c =>
Diagram t n m (SliceFactor 'To i c) -> i c
slfSliceIndex Diagram t n m (SliceFactor 'To i c)
dgSlf) (Cone Mlt 'Injective t n m c -> c
lUniv (forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Diagram t n m (SliceFactor 'To i c) -> Cone Mlt 'Injective t n m c
dgSlfToSlicePoint Diagram t n m (SliceFactor 'To i c)
dgSlf))
    csSlf :: FinList n (SliceFactor 'To i c)
csSlf = forall (h :: * -> * -> *) (f :: * -> *) a b.
Applicative1 h f =>
h a b -> f a -> f b
amap1 (\(Slice 'To i c
s,c
f) -> forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'To i c
s Slice 'To i c
tSlf c
f) (forall a (t :: DiagramType) (n :: N') (m :: N').
Oriented a =>
Diagram t n m a -> FinList n (Point a)
dgPoints Diagram t n m (SliceFactor 'To i c)
dgSlf forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> FinList n a
shell Cone Mlt 'Injective t n m c
lLim)
    
  slfUniv :: Cone Mlt 'Injective t n m (SliceFactor 'To i c)
-> SliceFactor 'To i c
slfUniv Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfCn = forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfLim) (forall s (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N')
       a.
Cone s p t n m a -> Point a
tip Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfCn) c
u where
    u :: c
u = Cone Mlt 'Injective t n m c -> c
lUniv forall (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall s (h :: * -> * -> *) a b (p :: Perspective)
       (t :: DiagramType) (n :: N') (m :: N').
Hom s h =>
h a b -> Cone s p t n m a -> Cone s p t n m b
cnMap forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
SliceFactorDrop 'To (SliceFactor 'To i c) c
SliceFactorToDrop Cone Mlt 'Injective t n m (SliceFactor 'To i c)
slfCn

--------------------------------------------------------------------------------
-- slfLimitsInjective -

-- | the induced 'Injective' 'Limits'.
slfLimitsInjective :: (Multiplicative c, Sliced i c)
  => Limits Mlt Injective t n m c -> Limits Mlt Injective t n m (SliceFactor To i c)
slfLimitsInjective :: forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Limits Mlt 'Injective t n m c
-> Limits Mlt 'Injective t n m (SliceFactor 'To i c)
slfLimitsInjective Limits Mlt 'Injective t n m c
lms = 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 (h :: * -> * -> *) a b. Applicative h => h a b -> a -> b
$ forall c (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative c, Sliced i c) =>
Limits Mlt 'Injective t n m c
-> Diagram t n m (SliceFactor 'To i c)
-> Limes Mlt 'Injective t n m (SliceFactor 'To i c)
slfLimesInjective Limits Mlt 'Injective t n m c
lms

--------------------------------------------------------------------------------
-- xSliceTo -

-- | the induced random variable.
xSliceTo :: Sliced i c
  => XOrtSite To c -> i c -> X (Slice To i c)
xSliceTo :: forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'To c -> i c -> X (Slice 'To i c)
xSliceTo (XEnd X (Point c)
_ Point c -> X c
xTo) i c
i = Point c -> X c
xTo (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i

--------------------------------------------------------------------------------
-- xSlicFrom -

-- | the induced random variable.
xSliceFrom :: Sliced i c
  => XOrtSite From c -> i c -> X (Slice From i c)
xSliceFrom :: forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'From c -> i c -> X (Slice 'From i c)
xSliceFrom (XStart X (Point c)
_ Point c -> X c
xFrom) i c
i = Point c -> X c
xFrom (forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i c
i) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
i

--------------------------------------------------------------------------------
-- xosXOrtSiteToSliceFactorTo -

-- | the induced random variable.
xosXOrtSiteToSliceFactorTo :: (Multiplicative c, Sliced i c)
  => XOrtSite To c -> i c -> XOrtSite To (SliceFactor To i c)
xosXOrtSiteToSliceFactorTo :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XOrtSite 'To (SliceFactor 'To i c)
xosXOrtSiteToSliceFactorTo xTo :: XOrtSite 'To c
xTo@(XEnd X (Point c)
_ Point c -> X c
xTo') i c
i = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Slice 'To i c)
xp Slice 'To i c -> X (SliceFactor 'To i c)
xsfTo where
  xp :: X (Slice 'To i c)
xp = forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'To c -> i c -> X (Slice 'To i c)
xSliceTo XOrtSite 'To c
xTo i c
i
  xsfTo :: Slice 'To i c -> X (SliceFactor 'To i c)
xsfTo e :: Slice 'To i c
e@(SliceTo i c
i c
a) = do
    c
f <- Point c -> X c
xTo' (forall q. Oriented q => q -> Point q
start c
a)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo i c
i (c
aforall c. Multiplicative c => c -> c -> c
*c
f)) Slice 'To i c
e c
f)

--------------------------------------------------------------------------------
-- xosXOrtSiteFromSliceFactorFrom -

-- | the induced random variable.
xosXOrtSiteFromSliceFactorFrom :: (Multiplicative c, Sliced i c)
  => XOrtSite From c -> i c -> XOrtSite From (SliceFactor From i c)
xosXOrtSiteFromSliceFactorFrom :: forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XOrtSite 'From (SliceFactor 'From i c)
xosXOrtSiteFromSliceFactorFrom xFrom :: XOrtSite 'From c
xFrom@(XStart X (Point c)
_ Point c -> X c
xFrom') i c
i = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Slice 'From i c)
xp Slice 'From i c -> X (SliceFactor 'From i c)
xsfFrom where
  xp :: X (Slice 'From i c)
xp = forall (i :: * -> *) c.
Sliced i c =>
XOrtSite 'From c -> i c -> X (Slice 'From i c)
xSliceFrom XOrtSite 'From c
xFrom i c
i
  xsfFrom :: Slice 'From i c -> X (SliceFactor 'From i c)
xsfFrom s :: Slice 'From i c
s@(SliceFrom i c
i c
a) = do
    c
f <- Point c -> X c
xFrom' (forall q. Oriented q => q -> Point q
end c
a)
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'From i c
s (forall (i :: * -> *) c. i c -> c -> Slice 'From i c
SliceFrom i c
i (c
fforall c. Multiplicative c => c -> c -> c
*c
a)) c
f)

--------------------------------------------------------------------------------
-- SliceFactor - XStandardOrtStite From -

instance (Multiplicative c, Sliced i c, XStandardOrtSite From c)
  => XStandardOrtSite From (SliceFactor From i c) where
  xStandardOrtSite :: XOrtSite 'From (SliceFactor 'From i c)
xStandardOrtSite = forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'From c -> i c -> XOrtSite 'From (SliceFactor 'From i c)
xosXOrtSiteFromSliceFactorFrom forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite forall (s :: * -> *) x. Singleton1 s => s x
unit1

instance (Multiplicative c, Sliced i c, XStandardOrtSite From c)
  => XStandardOrtSiteFrom (SliceFactor From i c)

instance (Multiplicative c, Sliced i c, XStandardOrtSite From c)
  => XStandard (SliceFactor From i c) where
  xStandard :: X (SliceFactor 'From i c)
xStandard = forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt ( forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
                       :: (Multiplicative c, Sliced i c, XStandardOrtSite From c)
                       => XOrtSite From (SliceFactor From i c)
                     )

instance (Multiplicative c, Sliced i c, XStandardOrtSite From c)
  => XStandard (Slice From i c) where
  xStandard :: X (Slice 'From i c)
xStandard = forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint ( forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
                         :: (Multiplicative c, Sliced i c, XStandardOrtSite From c)
                         => XOrtSite From (SliceFactor From i c)
                       )
instance (Multiplicative c, Sliced i c, XStandardOrtSite From c)
  => XStandardPoint (SliceFactor From i c)

--------------------------------------------------------------------------------
-- SliceFactor - XStandardOrtStite To -

instance (Multiplicative c, Sliced i c, XStandardOrtSite To c)
  => XStandardOrtSite To (SliceFactor To i c) where
  xStandardOrtSite :: XOrtSite 'To (SliceFactor 'To i c)
xStandardOrtSite = forall c (i :: * -> *).
(Multiplicative c, Sliced i c) =>
XOrtSite 'To c -> i c -> XOrtSite 'To (SliceFactor 'To i c)
xosXOrtSiteToSliceFactorTo forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite forall (s :: * -> *) x. Singleton1 s => s x
unit1

instance (Multiplicative c, Sliced i c, XStandardOrtSite To c)
  => XStandardOrtSiteTo (SliceFactor To i c)

instance (Multiplicative c, Sliced i c, XStandardOrtSite To c)
  => XStandard (SliceFactor To i c) where
  xStandard :: X (SliceFactor 'To i c)
xStandard = forall q (s :: Site). Oriented q => XOrtSite s q -> XOrt q
xosOrt ( forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
                       :: (Multiplicative c, Sliced i c, XStandardOrtSite To c)
                       => XOrtSite To (SliceFactor To i c)
                     )

instance (Multiplicative c, Sliced i c, XStandardOrtSite To c)
  => XStandard (Slice To i c) where
  xStandard :: X (Slice 'To i c)
xStandard = forall (s :: Site) q. XOrtSite s q -> X (Point q)
xosPoint ( forall (s :: Site) a. XStandardOrtSite s a => XOrtSite s a
xStandardOrtSite
                         :: (Multiplicative c, Sliced i c, XStandardOrtSite To c)
                         => XOrtSite To (SliceFactor To i c)
                       )
instance (Multiplicative c, Sliced i c, XStandardOrtSite To c)
  => XStandardPoint (SliceFactor To i c)

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

instance Sliced Proxy OS where
  slicePoint :: Proxy OS -> Point OS
slicePoint Proxy OS
_ = Symbol
P

instance XStandardOrtSite From (SliceFactor To Proxy OS) where
  xStandardOrtSite :: XOrtSite 'From (SliceFactor 'To Proxy OS)
xStandardOrtSite = forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Slice 'To Proxy OS)
xp Slice 'To Proxy OS -> X (SliceFactor 'To Proxy OS)
xFrom where
    xp :: X (Slice 'To Proxy OS)
xp = forall x. XStandard x => X x
xStandard
    xFrom :: Slice To Proxy OS -> X (SliceFactor To Proxy OS)
    xFrom :: Slice 'To Proxy OS -> X (SliceFactor 'To Proxy OS)
xFrom s :: Slice 'To Proxy OS
s@(SliceTo Proxy OS
i (Symbol
a:>Symbol
p)) = do
      Symbol
b <- forall x. XStandard x => X x
xStandard
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall (s :: Site) (i :: * -> *) c.
Slice s i c -> Slice s i c -> c -> SliceFactor s i c
SliceFactor Slice 'To Proxy OS
s (forall (i :: * -> *) c. i c -> c -> Slice 'To i c
SliceTo Proxy OS
i (Symbol
bforall p. p -> p -> Orientation p
:>Symbol
p)) (Symbol
aforall p. p -> p -> Orientation p
:>Symbol
b))

instance XStandardOrtSiteFrom (SliceFactor To Proxy OS)