Copyright | (c) Erich Gut |
---|---|
License | BSD3 |
Maintainer | zerich.gut@gmail.com |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
definition of slicing a Multiplicative
structures according a given indexed Point
.
Synopsis
- data Slice s i c where
- slice :: Slice s i c -> c
- data SliceFactor s i c = SliceFactor (Slice s i c) (Slice s i c) c
- slfDrop :: SliceFactor s i c -> c
- class (Entity1 i, Singleton1 i) => Sliced i c where
- slicePoint :: i c -> Point c
- 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
- 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
- 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
- lstLimes :: LimesSlicedTip i s p t n m c -> Limes s p t n m c
- slfTerminalPoint :: (Multiplicative c, Sliced i c) => TerminalPoint (SliceFactor To i c)
- slfPullback :: Multiplicative c => Products n (SliceFactor To i c) -> DiagramSlicedCenter i To (n + 1) n c -> Pullback n c
- slfLimitsInjective :: (Multiplicative c, Sliced i c) => Limits Mlt Injective t n m c -> Limits Mlt Injective t n m (SliceFactor To i c)
- xSliceTo :: Sliced i c => XOrtSite To c -> i c -> X (Slice To i c)
- xSliceFrom :: Sliced i c => XOrtSite From c -> i c -> X (Slice From i c)
- xosXOrtSiteToSliceFactorTo :: (Multiplicative c, Sliced i c) => XOrtSite To c -> i c -> XOrtSite To (SliceFactor To i c)
- xosXOrtSiteFromSliceFactorFrom :: (Multiplicative c, Sliced i c) => XOrtSite From c -> i c -> XOrtSite From (SliceFactor From i c)
Slice
data Slice s i c where Source #
slice over c
by a given Site
and indexed by i
.
Instances
(Show1 i, Show c) => Show (Slice s i c) Source # | |
(Eq1 i, Eq c) => Eq (Slice s i c) Source # | |
(Oriented c, Sliced i c) => Validable (Slice s i c) Source # | |
(Multiplicative c, Sliced i c, XStandardOrtSite 'From c) => XStandard (Slice 'From i c) Source # | |
(Multiplicative c, Sliced i c, XStandardOrtSite 'To c) => XStandard (Slice 'To i c) Source # | |
(Oriented c, Sliced i c, Typeable s) => Entity (Slice s i c) Source # | |
Defined in OAlg.Entity.Slice.Definition | |
type Dual (Slice s i c :: Type) Source # | |
Factor
data SliceFactor s i c Source #
factor between two slices.
Property Let SliceFactor a b f
be in
for a SliceFactor
s i cMultiplicative
structure c
constrained by
then holds:Sliced
i c
SliceFactor (Slice s i c) (Slice s i c) c |
Instances
slfDrop :: SliceFactor s i c -> c Source #
the underlying factor.
Sliced
class (Entity1 i, Singleton1 i) => Sliced i c where Source #
Slicing a Multiplicative
structures at the Point
given by the type of the index
i
.
Note The constraint
ensures that the distinguished point
depends only on the type Singleton1
ii c
.
slicePoint :: i c -> Point c Source #
the distingueished point of the given index type i
.
Hom
data SliceFactorDrop s x y where Source #
dropping a slice factor.
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 |
Instances
Limes
data DiagramSlicedCenter i t n m c where Source #
predicate for a
diagram with center Star
tPoint
given by the index type
i c
.
Property Let
be in
DiagramSlicedCenter
i d
then holds:
DiagramSlicedCenter
i t n m c
.slicePoint
i ==
dgCenter
d
DiagramSlicedCenter :: Sliced i c => i c -> Diagram (Star t) n m c -> DiagramSlicedCenter i t n m c |
Instances
Oriented c => Show (DiagramSlicedCenter i t n m c) Source # | |
Defined in OAlg.Entity.Slice.Definition showsPrec :: Int -> DiagramSlicedCenter i t n m c -> ShowS # show :: DiagramSlicedCenter i t n m c -> String # showList :: [DiagramSlicedCenter i t n m c] -> ShowS # | |
Oriented c => Validable (DiagramSlicedCenter i t n m c) Source # | |
Defined in OAlg.Entity.Slice.Definition valid :: DiagramSlicedCenter i t n m c -> Statement Source # |
data LimesSlicedTip i s p t n m c where Source #
predicate for a limes with a sliced tip of the universal cone.
Property Let
be in
LimesSlicedTip
i l
then holds:
LimesSlicedTip
i s p t n m c
.tip
(universalCone
l) ==
slicePoint
i
LimesSlicedTip :: Sliced i c => i c -> Limes s p t n m c -> LimesSlicedTip i s p t n m c |
Instances
Oriented c => Show (LimesSlicedTip i s p t n m c) Source # | |
Defined in OAlg.Entity.Slice.Definition showsPrec :: Int -> LimesSlicedTip i s p t n m c -> ShowS # show :: LimesSlicedTip i s p t n m c -> String # showList :: [LimesSlicedTip i s p t n m c] -> ShowS # | |
(Oriented c, Validable (Limes s p t n m c)) => Validable (LimesSlicedTip i s p t n m c) Source # | |
Defined in OAlg.Entity.Slice.Definition valid :: LimesSlicedTip i s p t n m c -> Statement Source # |
lstLimes :: LimesSlicedTip i s p t n m c -> Limes s p t n m c Source #
the underlying limes.
Projective
slfTerminalPoint :: (Multiplicative c, Sliced i c) => TerminalPoint (SliceFactor To i c) Source #
terminal point for factors sliced to a Point
.
slfPullback :: Multiplicative c => Products n (SliceFactor To i c) -> DiagramSlicedCenter i To (n + 1) n c -> Pullback n c Source #
the induced pullback.
Injective
slfLimitsInjective :: (Multiplicative c, Sliced i c) => Limits Mlt Injective t n m c -> Limits Mlt Injective t n m (SliceFactor To i c) Source #
X
xSliceTo :: Sliced i c => XOrtSite To c -> i c -> X (Slice To i c) Source #
the induced random variable.
xSliceFrom :: Sliced i c => XOrtSite From c -> i c -> X (Slice From i c) Source #
the induced random variable.
xosXOrtSiteToSliceFactorTo :: (Multiplicative c, Sliced i c) => XOrtSite To c -> i c -> XOrtSite To (SliceFactor To i c) Source #
the induced random variable.
xosXOrtSiteFromSliceFactorFrom :: (Multiplicative c, Sliced i c) => XOrtSite From c -> i c -> XOrtSite From (SliceFactor From i c) Source #
the induced random variable.