{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# 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, slSiteType
  , slMap, slMapCov, slMapCnt

    -- * Factor

  , SliceFactor(..), slfFactor, slfIndex
  , slfMap, slfMapCov, slfMapCnt
  
    -- * Duality

  , toDualOpOrtSld, toDualOpOrtSld'
  , toDualOpMltSld, toDualOpMltSld'
  
    -- * Hom

  , SliceFactorDrop(..)

    -- * Limes


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

    -- ** Projective

  , slfTerminalPoint
  , slfPullback

    -- ** Injective

  , slfLimitsInjective

    -- * X

  , xSliceTo, xSliceFrom
  , xosXOrtSiteToSliceFactorTo
  , xosXOrtSiteFromSliceFactorFrom
  , xosAdjTerminal

  ) where

import Control.Monad

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

import OAlg.Prelude

import OAlg.Category.SDuality

import OAlg.Data.Singleton
import OAlg.Data.Either

import OAlg.Structure.Exception
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative as M
import OAlg.Structure.Fibred
import OAlg.Structure.Additive
import OAlg.Structure.Distributive
import OAlg.Structure.Operational
import OAlg.Structure.Vectorial

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.Entity.Slice.Sliced

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

-- Slice -


-- | slice over __@x@__ by a given 'Site' and indexed by @__i__@.

data Slice s i x where
  SliceFrom :: i x -> x -> Slice From i x
  SliceTo :: i x -> x -> Slice To i x

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

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

-- slice -


-- | the underlying slice.

slice :: Slice s i x -> x
slice :: forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice (SliceFrom i x
_ x
p) = x
p
slice (SliceTo i x
_ x
p)   = x
p

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

-- slIndex -


-- | the underlying index.

slIndex :: Slice s i x -> i x
slIndex :: forall (s :: Site) (i :: * -> *) x. Slice s i x -> i x
slIndex (SliceFrom i x
i x
_) = i x
i
slIndex (SliceTo i x
i x
_)   = i x
i

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

-- slSiteType -


-- | the 'Site' type of a slice.

slSiteType :: Slice s i x -> Either (s :~: From) (s :~: To)
slSiteType :: forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Either (s :~: 'From) (s :~: 'To)
slSiteType (SliceFrom i x
_ x
_ ) = (s :~: 'From) -> Either (s :~: 'From) (s :~: 'To)
forall a b. a -> Either a b
Left s :~: s
s :~: 'From
forall {k} (a :: k). a :~: a
Refl
slSiteType (SliceTo i x
_ x
_)    = (s :~: 'To) -> Either (s :~: 'From) (s :~: 'To)
forall a b. b -> Either a b
Right s :~: s
s :~: 'To
forall {k} (a :: k). a :~: a
Refl

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

-- slTypeRefl -


slTypeRefl :: Slice s i x -> s :~: Dual (Dual s)
slTypeRefl :: forall (s :: Site) (i :: * -> *) x.
Slice s i x -> s :~: Dual (Dual s)
slTypeRefl (SliceFrom i x
_ x
_) = s :~: s
s :~: Dual (Dual s)
forall {k} (a :: k). a :~: a
Refl
slTypeRefl (SliceTo i x
_ x
_)   = s :~: s
s :~: Dual (Dual s)
forall {k} (a :: k). a :~: a
Refl

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

-- slMapCov -


-- | mapping of slices under a covariant homomorphism.

--

-- __Note__ As @'OAlg.Hom.Definition.IsoO' 'Ort' 'Op'@ is generated by 'toDualOpOrt' and

-- its inverse, the 'slicePoint' is invariant under these mappings and as such

-- 'slMapCov' maps 'valid' slices to 'valid' slices.

slMapCov :: HomSlicedOriented i h
  => Variant2 Covariant h x y -> Slice s i x -> Slice s i y
slMapCov :: forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov (Covariant2 h x y
h) Slice s i x
s = case Slice s i x
s of
  SliceFrom i x
i x
x          -> i y -> y -> Slice 'From i y
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Homomorphous (Sld i) x y -> i y
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange (Homomorphous (Sld i) x y -> i y)
-> Homomorphous (Sld i) x y -> i y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Proxy i -> h x y -> Homomorphous (Sld i) x y
forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom (i x -> Proxy i
forall (i :: * -> *) x. i x -> Proxy i
q i x
i) h x y
h) (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x)
  SliceTo i x
i x
x            -> i y -> y -> Slice 'To i y
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo (Homomorphous (Sld i) x y -> i y
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange (Homomorphous (Sld i) x y -> i y)
-> Homomorphous (Sld i) x y -> i y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Proxy i -> h x y -> Homomorphous (Sld i) x y
forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom (i x -> Proxy i
forall (i :: * -> *) x. i x -> Proxy i
q i x
i) h x y
h) (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x)
  where q :: i x -> Proxy i
        q :: forall (i :: * -> *) x. i x -> Proxy i
q i x
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy

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

-- slMapCnt -


-- | mapping of slices under a contravariant homomorphism.

slMapCnt :: HomSlicedOriented i h
  => Variant2 Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt :: forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt (Contravariant2 h x y
h) Slice s i x
s = case Slice s i x
s of
  SliceFrom i x
i x
x              -> i y -> y -> Slice 'To i y
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo (Homomorphous (Sld i) x y -> i y
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange (Homomorphous (Sld i) x y -> i y)
-> Homomorphous (Sld i) x y -> i y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Proxy i -> h x y -> Homomorphous (Sld i) x y
forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom (i x -> Proxy i
forall (i :: * -> *) x. i x -> Proxy i
q i x
i) h x y
h) (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x)
  SliceTo i x
i x
x                -> i y -> y -> Slice 'From i y
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom (Homomorphous (Sld i) x y -> i y
forall (i :: * -> *) x y. Homomorphous (Sld i) x y -> i y
sliceIndexRange (Homomorphous (Sld i) x y -> i y)
-> Homomorphous (Sld i) x y -> i y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Proxy i -> h x y -> Homomorphous (Sld i) x y
forall (i :: * -> *) (h :: * -> * -> *) (q :: (* -> *) -> *) x y.
HomSlicedOriented i h =>
q i -> h x y -> Homomorphous (Sld i) x y
sldHom (i x -> Proxy i
forall (i :: * -> *) x. i x -> Proxy i
q i x
i) h x y
h) (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h x
x)
  where q :: i x -> Proxy i
        q :: forall (i :: * -> *) x. i x -> Proxy i
q i x
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy

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

-- slMap -


-- | mapping of slices.

slMap :: (HomSlicedOriented i h, s ~ Dual (Dual s))
  => h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y
slMap :: forall (i :: * -> *) (h :: * -> * -> *) (s :: Site) x y.
(HomSlicedOriented i h, s ~ Dual (Dual s)) =>
h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y
slMap = (Variant2 'Covariant h x y -> Slice s i x -> Slice s i y)
-> (Variant2 'Covariant h x y
    -> Dual1 (Slice s i) x -> Dual1 (Slice s i) y)
-> (Variant2 'Contravariant h x y
    -> Slice s i x -> Dual1 (Slice s i) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (Slice s i) x -> Slice s i y)
-> h x y
-> SDualBi (Slice s i) x
-> SDualBi (Slice s i) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Covariant h x y
-> Dual1 (Slice s i) x -> Dual1 (Slice s i) y
Variant2 'Covariant h x y
-> Slice (Dual s) i x -> Slice (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Contravariant h x y -> Slice s i x -> Dual1 (Slice s i) y
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt Variant2 'Contravariant h x y -> Dual1 (Slice s i) x -> Slice s i y
Variant2 'Contravariant h x y
-> Slice (Dual s) i x -> Slice (Dual (Dual s)) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt

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

-- Duality -


type instance Dual1 (Slice s i) = Slice (Dual s) i

instance
  ( HomSlicedOriented i h
  , s ~ Dual (Dual s)
  )
  => ApplicativeG (SDualBi (Slice s i)) h (->) where
  amapG :: forall x y. h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y
amapG = h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y
forall (i :: * -> *) (h :: * -> * -> *) (s :: Site) x y.
(HomSlicedOriented i h, s ~ Dual (Dual s)) =>
h x y -> SDualBi (Slice s i) x -> SDualBi (Slice s i) y
slMap

instance
  ( HomSlicedOriented i h
  , FunctorialOriented h
  , s ~ Dual (Dual s)
  )
  => FunctorialG (SDualBi (Slice s i)) h (->)

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

-- Slice - Validable -


-- | validity of a 'Slice'.

relValidSlice :: Sliced i x => Slice s i x -> Statement
relValidSlice :: forall (i :: * -> *) x (s :: Site).
Sliced i x =>
Slice s i x -> Statement
relValidSlice s :: Slice s i x
s@(SliceFrom i x
i x
f)
  = [Statement] -> Statement
And [ i x -> Statement
forall x. i x -> Statement
forall (p :: * -> *) x. Validable1 p => p x -> Statement
valid1 i x
i
        , x -> Statement
forall a. Validable a => a -> Statement
valid x
f
        , let p :: Point x
p = i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i in
            (x -> Point x
forall q. Oriented q => q -> Point q
start x
f Point x -> Point x -> Bool
forall a. Eq a => a -> a -> Bool
== Point x
p) Bool -> Message -> Statement
:?> [Parameter] -> Message
Params [String
"s"String -> String -> Parameter
:=Slice s i x -> String
forall a. Show a => a -> String
show Slice s i x
s]
        ]
    
relValidSlice Slice s i x
s = case Slice s i x -> s :~: Dual (Dual s)
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> s :~: Dual (Dual s)
slTypeRefl Slice s i x
s of
  s :~: Dual (Dual s)
Refl -> Slice (Dual s) i (Op x) -> Statement
forall (i :: * -> *) x (s :: Site).
Sliced i x =>
Slice s i x -> Statement
relValidSlice Dual1 (Slice s i) (Op x)
Slice (Dual s) i (Op x)
s' where
            Contravariant2 Inv2 (HomDisjEmpty (Ort, Sld i) Op) x (Op x)
i = Proxy i
-> Variant2
     'Contravariant (Inv2 (HomDisjEmpty (Ort, Sld i) Op)) x (Op x)
forall (i :: * -> *) x (q :: (* -> *) -> *).
Sliced i x =>
q i -> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
toDualOpOrtSld' (Slice s i x -> Proxy i
forall (s :: Site) (i :: * -> *) x. Slice s i x -> Proxy i
q Slice s i x
s)
            SDualBi (Left1 Dual1 (Slice s i) (Op x)
s') = Inv2 (HomDisjEmpty (Ort, Sld i) Op) x (Op x)
-> SDualBi (Slice s i) x -> SDualBi (Slice s i) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 (HomDisjEmpty (Ort, Sld i) Op) x (Op x)
i (Either1 (Dual1 (Slice s i)) (Slice s i) x -> SDualBi (Slice s i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (Slice s i x -> Either1 (Slice (Dual s) i) (Slice s i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 Slice s i x
s))
  where q :: Slice s i x -> Proxy i
        q :: forall (s :: Site) (i :: * -> *) x. Slice s i x -> Proxy i
q Slice s i x
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy

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

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

-- SliceFactor -


-- | factor between two slices.

--

--  __Property__ Let @SliceFactor a b f@ be in

-- @'SliceFactor' __s i x__@ for a 'Multiplicative' structure __@x@__

-- constrained by @'Sliced' __i x__@ 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 x = SliceFactor (Slice s i x) (Slice s i x) x
  deriving (Int -> SliceFactor s i x -> ShowS
[SliceFactor s i x] -> ShowS
SliceFactor s i x -> String
(Int -> SliceFactor s i x -> ShowS)
-> (SliceFactor s i x -> String)
-> ([SliceFactor s i x] -> ShowS)
-> Show (SliceFactor s i x)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
Int -> SliceFactor s i x -> ShowS
forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
[SliceFactor s i x] -> ShowS
forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
SliceFactor s i x -> String
$cshowsPrec :: forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
Int -> SliceFactor s i x -> ShowS
showsPrec :: Int -> SliceFactor s i x -> ShowS
$cshow :: forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
SliceFactor s i x -> String
show :: SliceFactor s i x -> String
$cshowList :: forall (s :: Site) (i :: * -> *) x.
(Show1 i, Show x) =>
[SliceFactor s i x] -> ShowS
showList :: [SliceFactor s i x] -> ShowS
Show,SliceFactor s i x -> SliceFactor s i x -> Bool
(SliceFactor s i x -> SliceFactor s i x -> Bool)
-> (SliceFactor s i x -> SliceFactor s i x -> Bool)
-> Eq (SliceFactor s i x)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (s :: Site) (i :: * -> *) x.
(Eq1 i, Eq x) =>
SliceFactor s i x -> SliceFactor s i x -> Bool
$c== :: forall (s :: Site) (i :: * -> *) x.
(Eq1 i, Eq x) =>
SliceFactor s i x -> SliceFactor s i x -> Bool
== :: SliceFactor s i x -> SliceFactor s i x -> Bool
$c/= :: forall (s :: Site) (i :: * -> *) x.
(Eq1 i, Eq x) =>
SliceFactor s i x -> SliceFactor s i x -> Bool
/= :: SliceFactor s i x -> SliceFactor s i x -> Bool
Eq)

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

-- slfFactor -


-- | the underlying factor.

slfFactor :: SliceFactor s i x -> x       
slfFactor :: forall (s :: Site) (i :: * -> *) x. SliceFactor s i x -> x
slfFactor (SliceFactor Slice s i x
_ Slice s i x
_ x
f) = x
f

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

-- slfIndex -


-- | the associated index.

slfIndex :: Sliced i x => f (SliceFactor To i x) -> i x
slfIndex :: forall (i :: * -> *) x (f :: * -> *).
Sliced i x =>
f (SliceFactor 'To i x) -> i x
slfIndex f (SliceFactor 'To i x)
_ = i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

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

-- slfTypeRefl -


-- | proof of being reflexive.

slfTypeRefl :: SliceFactor s i x -> s :~: Dual (Dual s)
slfTypeRefl :: forall (s :: Site) (i :: * -> *) x.
SliceFactor s i x -> s :~: Dual (Dual s)
slfTypeRefl (SliceFactor Slice s i x
a Slice s i x
_ x
_) = Slice s i x -> s :~: Dual (Dual s)
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> s :~: Dual (Dual s)
slTypeRefl Slice s i x
a

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

-- slfMapCov -


-- | mapping of slices factor under a covariant homomorphism.

slfMapCov :: HomSlicedMultiplicative i h
  => Variant2 Covariant h x y -> SliceFactor s i x -> SliceFactor s i y
slfMapCov :: forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Covariant h x y -> SliceFactor s i x -> SliceFactor s i y
slfMapCov Variant2 'Covariant h x y
h (SliceFactor Slice s i x
a Slice s i x
b x
f) = Slice s i y -> Slice s i y -> y -> SliceFactor s i y
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor Slice s i y
a' Slice s i y
b' (Variant2 'Covariant h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap Variant2 'Covariant h x y
h x
f) where
  a' :: Slice s i y
a' = Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Covariant h x y
h Slice s i x
a
  b' :: Slice s i y
b' = Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Covariant h x y -> Slice s i x -> Slice s i y
slMapCov Variant2 'Covariant h x y
h Slice s i x
b
  
--------------------------------------------------------------------------------

-- slfMapCnt -


-- | mapping of slices factor under a contravariant homomorphism.

slfMapCnt :: HomSlicedMultiplicative i h
  => Variant2 Contravariant h x y -> SliceFactor s i x -> SliceFactor (Dual s) i y
slfMapCnt :: forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Contravariant h x y
-> SliceFactor s i x -> SliceFactor (Dual s) i y
slfMapCnt h :: Variant2 'Contravariant h x y
h@(Contravariant2 h x y
h') (SliceFactor Slice s i x
a Slice s i x
b x
f) = Slice (Dual s) i y
-> Slice (Dual s) i y -> y -> SliceFactor (Dual s) i y
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor Slice (Dual s) i y
b' Slice (Dual s) i y
a' (h x y -> x -> y
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
amap h x y
h' x
f) where
  a' :: Slice (Dual s) i y
a' = Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt Variant2 'Contravariant h x y
h Slice s i x
a
  b' :: Slice (Dual s) i y
b' = Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedOriented i h =>
Variant2 'Contravariant h x y -> Slice s i x -> Slice (Dual s) i y
slMapCnt Variant2 'Contravariant h x y
h Slice s i x
b

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

-- slfMap -


-- | mapping of slices factor.

slfMap :: (HomSlicedMultiplicative i h, s ~ Dual (Dual s))
  => h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y
slfMap :: forall (i :: * -> *) (h :: * -> * -> *) (s :: Site) x y.
(HomSlicedMultiplicative i h, s ~ Dual (Dual s)) =>
h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y
slfMap = (Variant2 'Covariant h x y
 -> SliceFactor s i x -> SliceFactor s i y)
-> (Variant2 'Covariant h x y
    -> Dual1 (SliceFactor s i) x -> Dual1 (SliceFactor s i) y)
-> (Variant2 'Contravariant h x y
    -> SliceFactor s i x -> Dual1 (SliceFactor s i) y)
-> (Variant2 'Contravariant h x y
    -> Dual1 (SliceFactor s i) x -> SliceFactor s i y)
-> h x y
-> SDualBi (SliceFactor s i) x
-> SDualBi (SliceFactor s i) y
forall (h :: * -> * -> *) x y (d :: * -> *).
Disjunctive2 h =>
(Variant2 'Covariant h x y -> d x -> d y)
-> (Variant2 'Covariant h x y -> Dual1 d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> d x -> Dual1 d y)
-> (Variant2 'Contravariant h x y -> Dual1 d x -> d y)
-> h x y
-> SDualBi d x
-> SDualBi d y
vmapBi Variant2 'Covariant h x y -> SliceFactor s i x -> SliceFactor s i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Covariant h x y -> SliceFactor s i x -> SliceFactor s i y
slfMapCov Variant2 'Covariant h x y
-> Dual1 (SliceFactor s i) x -> Dual1 (SliceFactor s i) y
Variant2 'Covariant h x y
-> SliceFactor (Dual s) i x -> SliceFactor (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Covariant h x y -> SliceFactor s i x -> SliceFactor s i y
slfMapCov Variant2 'Contravariant h x y
-> SliceFactor s i x -> Dual1 (SliceFactor s i) y
Variant2 'Contravariant h x y
-> SliceFactor s i x -> SliceFactor (Dual s) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Contravariant h x y
-> SliceFactor s i x -> SliceFactor (Dual s) i y
slfMapCnt Variant2 'Contravariant h x y
-> Dual1 (SliceFactor s i) x -> SliceFactor s i y
Variant2 'Contravariant h x y
-> SliceFactor (Dual s) i x -> SliceFactor (Dual (Dual s)) i y
forall (i :: * -> *) (h :: * -> * -> *) x y (s :: Site).
HomSlicedMultiplicative i h =>
Variant2 'Contravariant h x y
-> SliceFactor s i x -> SliceFactor (Dual s) i y
slfMapCnt

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

-- SliceFactor - Duality -


type instance Dual1 (SliceFactor s i) = SliceFactor (Dual s) i

instance (HomSlicedMultiplicative i h, s ~ Dual (Dual s))
  => ApplicativeG (SDualBi (SliceFactor s i)) h (->) where
  amapG :: forall x y.
h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y
amapG = h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y
forall (i :: * -> *) (h :: * -> * -> *) (s :: Site) x y.
(HomSlicedMultiplicative i h, s ~ Dual (Dual s)) =>
h x y -> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) y
slfMap

instance (HomSlicedMultiplicative i h, FunctorialOriented h, s ~ Dual (Dual s))
  => FunctorialG (SDualBi (SliceFactor s i)) h (->)

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

-- SliceTransformatin - Entity -


-- | validity of a 'SliceFactor'.

relValidSliceFactor :: (Multiplicative x, Sliced i x) => SliceFactor s i x -> Statement
relValidSliceFactor :: forall x (i :: * -> *) (s :: Site).
(Multiplicative x, Sliced i x) =>
SliceFactor s i x -> Statement
relValidSliceFactor (SliceFactor a :: Slice s i x
a@(SliceFrom i x
_ x
a') b :: Slice s i x
b@(SliceFrom i x
_ x
b') x
t)
  = [Statement] -> Statement
And [ Slice s i x -> Statement
forall a. Validable a => a -> Statement
valid Slice s i x
a
        , Slice s i x -> Statement
forall a. Validable a => a -> Statement
valid Slice s i x
b
        , x -> Statement
forall a. Validable a => a -> Statement
valid x
t
        , String -> Label
Label String
"1.1" Label -> Statement -> Statement
:<=>: (x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation x
t Orientation (Point x) -> Orientation (Point x) -> Bool
forall a. Eq a => a -> a -> Bool
== x -> Point x
forall q. Oriented q => q -> Point q
end x
a' Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:> x -> Point x
forall q. Oriented q => q -> Point q
end x
b')
            Bool -> Message -> Statement
:?> Message
prm
        , String -> Label
Label String
"1.2" Label -> Statement -> Statement
:<=>: (x
b' x -> x -> Bool
forall a. Eq a => a -> a -> Bool
== x
tx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
a') Bool -> Message -> Statement
:?> Message
prm
        ] where prm :: Message
prm = [Parameter] -> Message
Params [String
"(a,b,t)"String -> String -> Parameter
:=(Slice s i x, Slice s i x, x) -> String
forall a. Show a => a -> String
show (Slice s i x
a,Slice s i x
b,x
t)]
relValidSliceFactor SliceFactor s i x
t = case SliceFactor s i x -> s :~: Dual (Dual s)
forall (s :: Site) (i :: * -> *) x.
SliceFactor s i x -> s :~: Dual (Dual s)
slfTypeRefl SliceFactor s i x
t of
  s :~: Dual (Dual s)
Refl -> SliceFactor (Dual s) i (Op x) -> Statement
forall x (i :: * -> *) (s :: Site).
(Multiplicative x, Sliced i x) =>
SliceFactor s i x -> Statement
relValidSliceFactor Dual1 (SliceFactor s i) (Op x)
SliceFactor (Dual s) i (Op x)
t' where
            Contravariant2 Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
i = Proxy i
-> Variant2
     'Contravariant (Inv2 (HomDisjEmpty (Mlt, Sld i) Op)) x (Op x)
forall (i :: * -> *) x (q :: (* -> *) -> *).
(Sliced i x, Multiplicative x) =>
q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
toDualOpMltSld' (SliceFactor s i x -> Proxy i
forall (s :: Site) (i :: * -> *) x. SliceFactor s i x -> Proxy i
q SliceFactor s i x
t)
            SDualBi (Left1 Dual1 (SliceFactor s i) (Op x)
t') = Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
-> SDualBi (SliceFactor s i) x -> SDualBi (SliceFactor s i) (Op x)
forall (t :: * -> *) (a :: * -> * -> *) (b :: * -> * -> *) x y.
FunctorialG t a b =>
a x y -> b (t x) (t y)
amapF Inv2 (HomDisjEmpty (Mlt, Sld i) Op) x (Op x)
i (Either1 (Dual1 (SliceFactor s i)) (SliceFactor s i) x
-> SDualBi (SliceFactor s i) x
forall (d :: * -> *) x. Either1 (Dual1 d) d x -> SDualBi d x
SDualBi (SliceFactor s i x
-> Either1 (SliceFactor (Dual s) i) (SliceFactor s i) x
forall (g :: * -> *) x (f :: * -> *). g x -> Either1 f g x
Right1 SliceFactor s i x
t))
  where
    q :: SliceFactor s i x -> Proxy i
    q :: forall (s :: Site) (i :: * -> *) x. SliceFactor s i x -> Proxy i
q SliceFactor s i x
_ = Proxy i
forall {k} (t :: k). Proxy t
Proxy


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


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

-- SliceFactor - Multiplicative -


type instance Point (SliceFactor s i x) = Slice s i x
instance (Show1 i, Show x) => ShowPoint (SliceFactor s i x)
instance (Eq1 i, Eq x) => EqPoint (SliceFactor s i x)
instance Sliced i x => ValidablePoint (SliceFactor s i x)
instance (Typeable i, Typeable x, Typeable s) => TypeablePoint (SliceFactor s i x)

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

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

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

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

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

-- SliceFactor - TerminalPoint -


-- | terminal point for factors sliced to a 'Point'.

slfTerminalPoint :: (Multiplicative x, Sliced i x) => TerminalPoint (SliceFactor To i x)
slfTerminalPoint :: forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
TerminalPoint (SliceFactor 'To i x)
slfTerminalPoint = Cone Mlt 'Projective Diagram 'Empty N0 N0 (SliceFactor 'To i x)
-> (Cone Mlt 'Projective Diagram 'Empty N0 N0 (SliceFactor 'To i x)
    -> SliceFactor 'To i x)
-> LimesG
     Cone Mlt 'Projective Diagram 'Empty N0 N0 (SliceFactor 'To i 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 Diagram 'Empty N0 N0 (SliceFactor 'To i x)
l Cone Mlt 'Projective Diagram 'Empty N0 N0 (SliceFactor 'To i x)
-> SliceFactor 'To i x
u where
  o  :: (Multiplicative x, Sliced i x) => i x -> Slice To i x
  o :: forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
i x -> Slice 'To i x
o i x
i = i x -> x -> Slice 'To i x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i x
i (Point x -> x
forall c. Multiplicative c => Point c -> c
one (i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i))

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

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

-- DiagramSlicedCenter -


-- | predicate for a @'Star' __t__@ diagram with center 'Point' given by the index type

-- @__i x__@.

--

-- __Property__ Let @'DiagramSlicedCenter' i d@ be in

-- @'DiagramSlicedCenter' __i t n m x__@ then holds:

-- @'slicePoint' i '==' 'dgCenter' d@.

data DiagramSlicedCenter i t n m x where
  DiagramSlicedCenter :: Sliced i x
    => i x
    -> Diagram (Star t) n m x
    -> DiagramSlicedCenter i t n m x

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

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

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

-- slfPullback -


-- | the induced pullback.

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

-- @'tip' ('universalCone' l) '==' 'slicePoint' i@.

data LimesSlicedTip i s p t n m x where
  LimesSlicedTip :: Sliced i x => i x -> Limes s p t n m x -> LimesSlicedTip i s p t n m x


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

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

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

-- lstLimes -


-- | the underlying limes.

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

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

-- SliceFactorProjection -


-- | dropping a slice factor.

data SliceFactorDrop s x y where
  SliceFactorFromDrop
    :: (Multiplicative x, Sliced i x)
    => SliceFactorDrop From (SliceFactor From i x) x 
  SliceFactorToDrop
    :: (Multiplicative x, Sliced i x)
    => SliceFactorDrop To (SliceFactor To i x) x

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

-- 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)

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

-- 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 = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct
  homomorphous SliceFactorDrop s x y
SliceFactorToDrop   = Struct Mlt x
forall s x. Structure s x => Struct s x
Struct Struct Mlt x -> Struct Mlt y -> Homomorphous Mlt x y
forall s x y. Struct s x -> Struct s y -> Homomorphous s x y
:>: Struct Mlt y
forall s x. Structure s x => Struct s x
Struct

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

-- SliceFactorDrop - HomMultiplicative -


instance ApplicativeG Id (SliceFactorDrop s) (->) where
  amapG :: forall x y. SliceFactorDrop s x y -> Id x -> Id y
amapG SliceFactorDrop s x y
SliceFactorFromDrop = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
SliceFactor 'From i y -> y
forall (s :: Site) (i :: * -> *) x. SliceFactor s i x -> x
slfFactor
  amapG SliceFactorDrop s x y
SliceFactorToDrop   = (x -> y) -> Id x -> Id y
forall x y. (x -> y) -> Id x -> Id y
toIdG x -> y
SliceFactor 'To i y -> y
forall (s :: Site) (i :: * -> *) x. SliceFactor s i x -> x
slfFactor

instance ApplicativeG Pnt (SliceFactorDrop s) (->) where
  amapG :: forall x y. SliceFactorDrop s x y -> Pnt x -> Pnt y
amapG SliceFactorDrop s x y
SliceFactorFromDrop (Pnt (SliceFrom i y
_ y
a)) = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (y -> Point y
forall q. Oriented q => q -> Point q
end y
a)
  amapG SliceFactorDrop s x y
SliceFactorToDrop (Pnt (SliceTo i y
_ y
a))     = Point y -> Pnt y
forall x. Point x -> Pnt x
Pnt (y -> Point y
forall q. Oriented q => q -> Point q
start y
a)


instance HomOriented (SliceFactorDrop s)
instance HomMultiplicative (SliceFactorDrop s)

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

-- slfSliceIndex -


-- | the given attest for the slice index @__i x__@ given by the diagram proxy.

slfSliceIndex :: Sliced i x => Diagram t n m (SliceFactor To i x) -> i x
slfSliceIndex :: forall (i :: * -> *) x (t :: DiagramType) (n :: N') (m :: N').
Sliced i x =>
Diagram t n m (SliceFactor 'To i x) -> i x
slfSliceIndex Diagram t n m (SliceFactor 'To i x)
_ = i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

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

-- dgSlfToSlicePoint -


-- | the diagram as a cone with its tip given by the 'slicePoint'.

dgSlfToSlicePoint :: (Multiplicative x, Sliced i x)
  => Diagram t n m (SliceFactor To i x) -> Cone Mlt Injective Diagram t n m x
dgSlfToSlicePoint :: forall x (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x, Sliced i x) =>
Diagram t n m (SliceFactor 'To i x)
-> Cone Mlt 'Injective Diagram t n m x
dgSlfToSlicePoint Diagram t n m (SliceFactor 'To i x)
d = Diagram t n m x
-> Point x -> FinList n x -> Cone Mlt 'Injective Diagram t n m x
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeInjective Diagram t n m x
d' Point x
t FinList n x
cs where
  d' :: Diagram t n m x
d' = SliceFactorDrop 'To (SliceFactor 'To i x) x
-> Diagram t n m (SliceFactor 'To i x) -> Diagram t n m x
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOriented h =>
h x y -> Diagram t n m x -> Diagram t n m y
dgMap SliceFactorDrop 'To (SliceFactor 'To i x) x
forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
SliceFactorDrop 'To (SliceFactor 'To i x) x
SliceFactorToDrop Diagram t n m (SliceFactor 'To i x)
d
  t :: Point x
t  = i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint (i x -> Point x) -> i x -> Point x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m (SliceFactor 'To i x) -> i x
forall (i :: * -> *) x (t :: DiagramType) (n :: N') (m :: N').
Sliced i x =>
Diagram t n m (SliceFactor 'To i x) -> i x
slfSliceIndex Diagram t n m (SliceFactor 'To i x)
d
  cs :: FinList n x
cs = (Slice 'To i x -> x) -> FinList n (Slice 'To i x) -> FinList n x
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 Slice 'To i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice (FinList n (Slice 'To i x) -> FinList n x)
-> FinList n (Slice 'To i x) -> FinList n x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Diagram t n m (SliceFactor 'To i x)
-> FinList n (Point (SliceFactor 'To i x))
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 x)
d

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

-- slfLimesInjective -


-- | the induced 'Injective' limes for 'SliceFactor'. 

slfLimesInjective :: (Multiplicative x, Sliced i x)
  => Limits Mlt Injective t n m x
  -> Diagram t n m (SliceFactor To i x)
  -> Limes Mlt Injective t n m (SliceFactor To i x)
slfLimesInjective :: forall x (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x, Sliced i x) =>
Limits Mlt 'Injective t n m x
-> Diagram t n m (SliceFactor 'To i x)
-> Limes Mlt 'Injective t n m (SliceFactor 'To i x)
slfLimesInjective Limits Mlt 'Injective t n m x
l Diagram t n m (SliceFactor 'To i x)
dgSlf = Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> (Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
    -> SliceFactor 'To i x)
-> LimesG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
forall (c :: *
             -> Perspective
             -> (DiagramType -> N' -> N' -> * -> *)
             -> DiagramType
             -> N'
             -> N'
             -> *
             -> *)
       s (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') x.
c s 'Injective d t n m x
-> (Cone s 'Injective d t n m x -> x)
-> LimesG c s 'Injective d t n m x
LimesInjective Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfLim Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> SliceFactor 'To i x
slfUniv where
  LimesInjective Cone Mlt 'Injective Diagram t n m x
lLim Cone Mlt 'Injective Diagram t n m x -> x
lUniv = Limits Mlt 'Injective t n m x
-> Diagram t n m x -> LimesG Cone Mlt 'Injective Diagram 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.
LimitsG c s p d t n m x -> d t n m x -> LimesG c s p d t n m x
limes Limits Mlt 'Injective t n m x
l (SliceFactorDrop 'To (SliceFactor 'To i x) x
-> Diagram t n m (SliceFactor 'To i x) -> Diagram t n m x
forall (h :: * -> * -> *) x y (t :: DiagramType) (n :: N')
       (m :: N').
HomOriented h =>
h x y -> Diagram t n m x -> Diagram t n m y
dgMap SliceFactorDrop 'To (SliceFactor 'To i x) x
forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
SliceFactorDrop 'To (SliceFactor 'To i x) x
SliceFactorToDrop Diagram t n m (SliceFactor 'To i x)
dgSlf)
  
  slfLim :: Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfLim = Diagram t n m (SliceFactor 'To i x)
-> Point (SliceFactor 'To i x)
-> FinList n (SliceFactor 'To i x)
-> Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
forall a (d :: DiagramType -> N' -> N' -> * -> *)
       (t :: DiagramType) (n :: N') (m :: N').
Multiplicative a =>
d t n m a
-> Point a -> FinList n a -> Cone Mlt 'Injective d t n m a
ConeInjective Diagram t n m (SliceFactor 'To i x)
dgSlf Point (SliceFactor 'To i x)
Slice 'To i x
tSlf FinList n (SliceFactor 'To i x)
csSlf where
    tSlf :: Slice 'To i x
tSlf = i x -> x -> Slice 'To i x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo (Diagram t n m (SliceFactor 'To i x) -> i x
forall (i :: * -> *) x (t :: DiagramType) (n :: N') (m :: N').
Sliced i x =>
Diagram t n m (SliceFactor 'To i x) -> i x
slfSliceIndex Diagram t n m (SliceFactor 'To i x)
dgSlf) (Cone Mlt 'Injective Diagram t n m x -> x
lUniv (Diagram t n m (SliceFactor 'To i x)
-> Cone Mlt 'Injective Diagram t n m x
forall x (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x, Sliced i x) =>
Diagram t n m (SliceFactor 'To i x)
-> Cone Mlt 'Injective Diagram t n m x
dgSlfToSlicePoint Diagram t n m (SliceFactor 'To i x)
dgSlf))
    csSlf :: FinList n (SliceFactor 'To i x)
csSlf = ((Slice 'To i x, x) -> SliceFactor 'To i x)
-> FinList n (Slice 'To i x, x) -> FinList n (SliceFactor 'To i x)
forall (h :: * -> * -> *) (f :: * -> *) x y.
Applicative1 h f =>
h x y -> f x -> f y
amap1 (\(Slice 'To i x
s,x
f) -> Slice 'To i x -> Slice 'To i x -> x -> SliceFactor 'To i x
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor Slice 'To i x
s Slice 'To i x
tSlf x
f) (Diagram t n m (SliceFactor 'To i x)
-> FinList n (Point (SliceFactor 'To i x))
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 x)
dgSlf FinList n (Slice 'To i x)
-> FinList n x -> FinList n (Slice 'To i x, x)
forall (n :: N') a b.
FinList n a -> FinList n b -> FinList n (a, b)
`zip` Cone Mlt 'Injective Diagram t n m x -> FinList n x
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> FinList n a
shell Cone Mlt 'Injective Diagram t n m x
lLim)

  slfUniv :: Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> SliceFactor 'To i x
slfUniv Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfCn = case Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> Dual (Dual t) :~: t
forall (d :: DiagramType -> N' -> N' -> * -> *) s
       (p :: Perspective) (t :: DiagramType) (n :: N') (m :: N') a.
Diagrammatic d =>
Cone s p d t n m a -> Dual (Dual t) :~: t
cnDiagramTypeRefl Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfCn of
    Dual (Dual t) :~: t
Refl -> Slice 'To i x -> Slice 'To i x -> x -> SliceFactor 'To i x
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor (Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> Point (SliceFactor 'To i x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfLim) (Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> Point (SliceFactor 'To i x)
forall s (p :: Perspective)
       (d :: DiagramType -> N' -> N' -> * -> *) (t :: DiagramType)
       (n :: N') (m :: N') a.
Cone s p d t n m a -> Point a
tip Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfCn) x
u where
              u :: x
u = Cone Mlt 'Injective Diagram t n m x -> x
lUniv (Cone Mlt 'Injective Diagram t n m x -> x)
-> Cone Mlt 'Injective Diagram t n m x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ SliceFactorDrop 'To (SliceFactor 'To i x) x
-> Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
-> Cone Mlt 'Injective Diagram t n m x
forall s (h :: * -> * -> *) (t :: DiagramType) x y
       (p :: Perspective) (n :: N') (m :: N').
(Hom s h, t ~ Dual (Dual t)) =>
h x y -> Cone s p Diagram t n m x -> Cone s p Diagram t n m y
cnMap SliceFactorDrop 'To (SliceFactor 'To i x) x
forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
SliceFactorDrop 'To (SliceFactor 'To i x) x
SliceFactorToDrop Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
slfCn

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

-- slfLimitsInjective -


-- | the induced 'Injective' 'Limits'.

slfLimitsInjective :: (Multiplicative x, Sliced i x)
  => Limits Mlt Injective t n m x -> Limits Mlt Injective t n m (SliceFactor To i x)
slfLimitsInjective :: forall x (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x, Sliced i x) =>
Limits Mlt 'Injective t n m x
-> Limits Mlt 'Injective t n m (SliceFactor 'To i x)
slfLimitsInjective Limits Mlt 'Injective t n m x
lms = (Diagram t n m (SliceFactor 'To i x)
 -> LimesG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x))
-> LimitsG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i 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 t n m (SliceFactor 'To i x)
  -> LimesG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x))
 -> LimitsG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x))
-> (Diagram t n m (SliceFactor 'To i x)
    -> LimesG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x))
-> LimitsG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Limits Mlt 'Injective t n m x
-> Diagram t n m (SliceFactor 'To i x)
-> LimesG Cone Mlt 'Injective Diagram t n m (SliceFactor 'To i x)
forall x (i :: * -> *) (t :: DiagramType) (n :: N') (m :: N').
(Multiplicative x, Sliced i x) =>
Limits Mlt 'Injective t n m x
-> Diagram t n m (SliceFactor 'To i x)
-> Limes Mlt 'Injective t n m (SliceFactor 'To i x)
slfLimesInjective Limits Mlt 'Injective t n m x
lms


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

-- xSliceTo -


-- | the induced random variable.

xSliceTo :: Sliced i x
  => XOrtSite To x -> i x -> X (Slice To i x)
xSliceTo :: forall (i :: * -> *) x.
Sliced i x =>
XOrtSite 'To x -> i x -> X (Slice 'To i x)
xSliceTo (XEnd X (Point x)
_ Point x -> X x
xTo) i x
i = Point x -> X x
xTo (i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i) X x -> (x -> X (Slice 'To i x)) -> X (Slice 'To i x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Slice 'To i x -> X (Slice 'To i x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Slice 'To i x -> X (Slice 'To i x))
-> (x -> Slice 'To i x) -> x -> X (Slice 'To i 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
. i x -> x -> Slice 'To i x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i x
i

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

-- xSlicFrom -


-- | the induced random variable.

xSliceFrom :: Sliced i x
  => XOrtSite From x -> i x -> X (Slice From i x)
xSliceFrom :: forall (i :: * -> *) x.
Sliced i x =>
XOrtSite 'From x -> i x -> X (Slice 'From i x)
xSliceFrom (XStart X (Point x)
_ Point x -> X x
xFrom) i x
i = Point x -> X x
xFrom (i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i) X x -> (x -> X (Slice 'From i x)) -> X (Slice 'From i x)
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Slice 'From i x -> X (Slice 'From i x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Slice 'From i x -> X (Slice 'From i x))
-> (x -> Slice 'From i x) -> x -> X (Slice 'From i 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
. i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i

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

-- xosXOrtSiteToSliceFactorTo -


-- | the induced random variable.

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

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

-- xosXOrtSiteFromSliceFactorFrom -


-- | the induced random variable.

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

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

-- SliceFactor - XStandardOrtStite From -


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

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

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

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

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

-- SliceFactor - XStandardOrtStite To -


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

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

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

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

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


instance XStandardOrtSite From (SliceFactor To Proxy OS) where
  xStandardOrtSite :: XOrtSite 'From (SliceFactor 'To Proxy OS)
xStandardOrtSite = X (Point (SliceFactor 'To Proxy OS))
-> (Point (SliceFactor 'To Proxy OS)
    -> X (SliceFactor 'To Proxy OS))
-> XOrtSite 'From (SliceFactor 'To Proxy OS)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'From q
XStart X (Point (SliceFactor 'To Proxy OS))
X (Slice 'To Proxy OS)
xp Point (SliceFactor 'To Proxy OS) -> X (SliceFactor 'To Proxy OS)
Slice 'To Proxy OS -> X (SliceFactor 'To Proxy OS)
xFrom where
    xp :: X (Slice 'To Proxy OS)
xp = X (Slice 'To Proxy OS)
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 <- X Symbol
forall x. XStandard x => X x
xStandard
      SliceFactor 'To Proxy OS -> X (SliceFactor 'To Proxy OS)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return (Slice 'To Proxy OS
-> Slice 'To Proxy OS -> OS -> SliceFactor 'To Proxy OS
forall (s :: Site) (i :: * -> *) x.
Slice s i x -> Slice s i x -> x -> SliceFactor s i x
SliceFactor Slice 'To Proxy OS
s (Proxy OS -> OS -> Slice 'To Proxy OS
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo Proxy OS
i (Symbol
bSymbol -> Symbol -> OS
forall p. p -> p -> Orientation p
:>Symbol
p)) (Symbol
aSymbol -> Symbol -> OS
forall p. p -> p -> Orientation p
:>Symbol
b))

instance XStandardOrtSiteFrom (SliceFactor To Proxy OS)

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

-- xosAdjTerminal -


-- | adjoins a terminal point with the given probability to the random variable of the points of

-- the given @'XOrtSite' 'To'@ of the @'SliceFactor' 'To' __i x__@. Such a terminal point is given

-- by @'one' s@ where @s@ is the slice point. 

xosAdjTerminal :: (Multiplicative x, Sliced i x)
  => Q -> XOrtSite To (SliceFactor To i x) -> XOrtSite To (SliceFactor To i x)
xosAdjTerminal :: forall x (i :: * -> *).
(Multiplicative x, Sliced i x) =>
Q
-> XOrtSite 'To (SliceFactor 'To i x)
-> XOrtSite 'To (SliceFactor 'To i x)
xosAdjTerminal Q
w xos :: XOrtSite 'To (SliceFactor 'To i x)
xos@(XEnd X (Point (SliceFactor 'To i x))
xp Point (SliceFactor 'To i x) -> X (SliceFactor 'To i x)
xf) = X (Point (SliceFactor 'To i x))
-> (Point (SliceFactor 'To i x) -> X (SliceFactor 'To i x))
-> XOrtSite 'To (SliceFactor 'To i x)
forall q. X (Point q) -> (Point q -> X q) -> XOrtSite 'To q
XEnd X (Point (SliceFactor 'To i x))
X (Slice 'To i x)
xp' Point (SliceFactor 'To i x) -> X (SliceFactor 'To i x)
xf where
  xp' :: X (Slice 'To i x)
xp' = [(Q, X (Slice 'To i x))] -> X (Slice 'To i x)
forall a. [(Q, X a)] -> X a
xOneOfXW [(Q
w0,X (Point (SliceFactor 'To i x))
X (Slice 'To i x)
xp),(Q
w,Slice 'To i x -> X (Slice 'To i x)
forall a. a -> X a
forall (m :: * -> *) a. Monad m => a -> m a
return Slice 'To i x
s)]
  w0 :: Q
w0  = Q
1 Q -> Q -> Q
forall a. Abelian a => a -> a -> a
- Q
w
  i :: i x
i   = XOrtSite 'To (SliceFactor 'To i x) -> i x
forall (i :: * -> *) x (f :: * -> *).
Sliced i x =>
f (SliceFactor 'To i x) -> i x
slfIndex XOrtSite 'To (SliceFactor 'To i x)
xos
  s :: Slice 'To i x
s   = i x -> x -> Slice 'To i x
forall (i :: * -> *) x. i x -> x -> Slice 'To i x
SliceTo i x
i (Point x -> x
forall c. Multiplicative c => Point c -> c
one (Point x -> x) -> Point x -> x
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i)


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

-- Slice - Structure -


type instance Point (Slice s i x) = Point x

instance ShowPoint x => ShowPoint (Slice s i x)
instance EqPoint x => EqPoint (Slice s i x)
instance ValidablePoint x => ValidablePoint (Slice s i x)
instance TypeablePoint x => TypeablePoint (Slice s i x)

instance (Oriented x, Sliced i x, Typeable s) => Oriented (Slice s i x) where
  orientation :: Slice s i x -> Orientation (Point (Slice s i x))
orientation Slice s i x
s = x -> Orientation (Point x)
forall q. Oriented q => q -> Orientation (Point q)
orientation (x -> Orientation (Point x)) -> x -> Orientation (Point x)
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Slice s i x -> x
forall (s :: Site) (i :: * -> *) x. Slice s i x -> x
slice Slice s i x
s

instance (Sliced i x, Ord x) => Ord (Slice s i x) where
  compare :: Slice s i x -> Slice s i x -> Ordering
compare (SliceFrom i x
_ x
a ) (SliceFrom i x
_ x
b) = x -> x -> Ordering
forall a. Ord a => a -> a -> Ordering
compare x
a x
b
  compare (SliceTo i x
_ x
a) (SliceTo i x
_ x
b)      = x -> x -> Ordering
forall a. Ord a => a -> a -> Ordering
compare x
a x
b
  
--------------------------------------------------------------------------------

-- Slice From - OrientedOpl -


instance Multiplicative x => Opl x (Slice From i x) where
  x
f *> :: x -> Slice 'From i x -> Slice 'From i x
*> (SliceFrom i x
i x
c) = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (x
fx -> x -> x
forall c. Multiplicative c => c -> c -> c
*x
c)

instance (Multiplicative x, Sliced i x) => OrientedOpl x (Slice From i x)

type instance Root (Slice s i x) = Point x

instance ShowPoint x => ShowRoot (Slice s i x)
instance EqPoint x => EqRoot (Slice s i x)
instance ValidablePoint x => ValidableRoot (Slice s i x)
instance TypeablePoint x => TypeableRoot (Slice s i x)

instance (Distributive x, Sliced i x, Typeable s) => Fibred (Slice s i x) where
 root :: Slice s i x -> Root (Slice s i x)
root (SliceFrom i x
_ x
s) = x -> Point x
forall q. Oriented q => q -> Point q
end x
s
 root (SliceTo i x
_ x
s)   = x -> Point x
forall q. Oriented q => q -> Point q
start x
s

instance (Distributive x, Sliced i x) => Additive (Slice From i x) where
  zero :: Root (Slice 'From i x) -> Slice 'From i x
zero Root (Slice 'From i x)
e = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (Root x -> x
forall a. Additive a => Root a -> a
zero (i x -> Point x
forall (i :: * -> *) c. Sliced i c => i c -> Point c
slicePoint i x
i Point x -> Point x -> Orientation (Point x)
forall p. p -> p -> Orientation p
:> Point x
Root (Slice 'From i x)
e))
    where i :: i x
i = Point x -> i x
forall (i :: * -> *) x. Sliced i x => Point x -> i x
i' Point x
Root (Slice 'From i x)
e
          i' :: Sliced i x => Point x -> i x
          i' :: forall (i :: * -> *) x. Sliced i x => Point x -> i x
i' Point x
_ = i x
forall x. i x
forall (s :: * -> *) x. Singleton1 s => s x
unit1

  SliceFrom i x
i x
a + :: Slice 'From i x -> Slice 'From i x -> Slice 'From i x
+ SliceFrom i x
_ x
b = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (x
ax -> x -> x
forall a. Additive a => a -> a -> a
+x
b)

  ntimes :: N -> Slice 'From i x -> Slice 'From i x
ntimes N
n (SliceFrom i x
i x
a) = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (N -> x -> x
forall a. Additive a => N -> a -> a
ntimes N
n x
a)
  
instance (Distributive x, Abelian x, Sliced i x) => Abelian (Slice From i x) where
  negate :: Slice 'From i x -> Slice 'From i x
negate (SliceFrom i x
i x
a) = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (x -> x
forall a. Abelian a => a -> a
negate x
a)

  SliceFrom i x
i x
a - :: Slice 'From i x -> Slice 'From i x -> Slice 'From i x
- SliceFrom i x
_ x
b = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (x
ax -> x -> x
forall a. Abelian a => a -> a -> a
-x
b)
  
  ztimes :: Z -> Slice 'From i x -> Slice 'From i x
ztimes Z
z (SliceFrom i x
i x
a) = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (Z -> x -> x
forall a. Abelian a => Z -> a -> a
ztimes Z
z x
a)

instance (Distributive x, Vectorial x, Sliced i x) => Vectorial (Slice From i x) where
  type Scalar (Slice From i x) = Scalar x
  Scalar (Slice 'From i x)
x ! :: Scalar (Slice 'From i x) -> Slice 'From i x -> Slice 'From i x
! SliceFrom i x
i x
a = i x -> x -> Slice 'From i x
forall (i :: * -> *) x. i x -> x -> Slice 'From i x
SliceFrom i x
i (Scalar x
Scalar (Slice 'From i x)
xScalar x -> x -> x
forall v. Vectorial v => Scalar v -> v -> v
!x
a)