Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

OAlg.Entity.Slice.Free

Contents

Free
Limes

Description

sliced structures with an assigned free Point of some given dimension.

Synopsis

newtype Free k c = Free (Any k)
freeN :: Free k c -> N
castFree :: Free k x -> Free k y
isFree :: (Eq (Point c), Sliced (Free k) c) => Free k c -> Point c -> Bool
data SomeFree c where
- SomeFree :: (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c
data SomeFreeSlice s c where
- SomeFreeSlice :: (Attestable k, Sliced (Free k) c) => Slice s (Free k) c -> SomeFreeSlice s c
data LimesFree s p t n m a where
- LimesFree :: (Attestable k, Sliced (Free k) a) => Free k a -> Limes s p t n m a -> LimesFree s p t n m a
limesFree :: LimesFree s p t n m a -> Limes s p t n m a
data DiagramFree t n m a = DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)
dgfDiagram :: DiagramFree t n m a -> Diagram t n m a
data KernelSliceFromSomeFreeTip n i c where
- KernelSliceFromSomeFreeTip :: (Attestable k', Sliced (Free k') c) => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c
ksfKernel :: KernelSliceFromSomeFreeTip n i c -> Kernel n c
type KernelFree = LimesFree Dst Projective (Parallel LeftToRight) N2
type KernelDiagramFree = DiagramFree (Parallel LeftToRight) N2
type CokernelDiagramFree = DiagramFree (Parallel RightToLeft) N2
type PullbackFree n c = LimesFree Mlt Projective (Star To) (n + 1) n c
type PullbackDiagramFree n c = DiagramFree (Star To) (n + 1) n c

Free

newtype Free k c Source #

index for free points within a Multiplicative structure c.

>>> lengthN (Free attest :: Free N3 c)
3

Constructors

Free (Any k)

Instances

Instances details

Eq1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods eq1 :: Free k x -> Free k x -> Bool Source #
Show1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods show1 :: Free k x -> String Source #
Attestable k => Singleton1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods unit1 :: Free k x Source #
Validable1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid1 :: Free k x -> Statement Source #
Typeable k => Entity1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Show (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> Free k c -> ShowS # show :: Free k c -> String # showList :: [Free k c] -> ShowS #
Eq (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods (==) :: Free k c -> Free k c -> Bool # (/=) :: Free k c -> Free k c -> Bool #
Validable (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: Free k c -> Statement Source #
(Typeable c, Typeable k) => Entity (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free

freeN :: Free k c -> N Source #

the underlying natural number.

castFree :: Free k x -> Free k y Source #

casting between Free types.

isFree :: (Eq (Point c), Sliced (Free k) c) => Free k c -> Point c -> Bool Source #

check for being a free point, i.e. if it is equal to slicePoint.

Definition Let n be in Free n c and p in Point c then we call p of order n if and only if slicePoint i == p.

data SomeFree c where Source #

some free attest.

Constructors

SomeFree :: (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c

Instances

Instances details

Show (SomeFree c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> SomeFree c -> ShowS # show :: SomeFree c -> String # showList :: [SomeFree c] -> ShowS #
Validable (SomeFree c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: SomeFree c -> Statement Source #

data SomeFreeSlice s c where Source #

some free point within a Multiplicative structure c.

Constructors

SomeFreeSlice :: (Attestable k, Sliced (Free k) c) => Slice s (Free k) c -> SomeFreeSlice s c

Instances

Instances details

Show c => Show (SomeFreeSlice s c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> SomeFreeSlice s c -> ShowS # show :: SomeFreeSlice s c -> String # showList :: [SomeFreeSlice s c] -> ShowS #
Oriented c => Validable (SomeFreeSlice s c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: SomeFreeSlice s c -> Statement Source #

Limes

data LimesFree s p t n m a where Source #

predicate for a limes with a free tip of its universal cone.

Property Let 'LimesFree k l be in LimesFree s p t n m a and then holds: slicePoint k == t where t = tip (universalCone l).

Constructors

LimesFree :: (Attestable k, Sliced (Free k) a) => Free k a -> Limes s p t n m a -> LimesFree s p t n m a

Instances

Instances details

Oriented a => Show (LimesFree s p t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> LimesFree s p t n m a -> ShowS # show :: LimesFree s p t n m a -> String # showList :: [LimesFree s p t n m a] -> ShowS #
(Distributive a, XStandardOrtPerspective p a, Typeable p, Typeable t, Typeable n, Typeable m) => Validable (LimesFree Dst p t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: LimesFree Dst p t n m a -> Statement Source #

limesFree :: LimesFree s p t n m a -> Limes s p t n m a Source #

the underlying free limes.

data DiagramFree t n m a Source #

predicate for diagrams with free points.

Constructors

DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)

Instances

Instances details

Oriented a => Show (DiagramFree t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> DiagramFree t n m a -> ShowS # show :: DiagramFree t n m a -> String # showList :: [DiagramFree t n m a] -> ShowS #
Oriented a => Validable (DiagramFree t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: DiagramFree t n m a -> Statement Source #

dgfDiagram :: DiagramFree t n m a -> Diagram t n m a Source #

the underlying diagram.

data KernelSliceFromSomeFreeTip n i c where Source #

predicate for a kernel with a start point of its diagram given by the slice index and a free universal tip.

Property Let KernelSliceFromSomeFreeTip k' i ker be in KernelSliceFromSomeFreeTip n c, then holds:

slicePoint i == s where DiagramParallelLR s _ _ = diagram ker.
slicePoint k' == tip (universalCone ker).

Constructors

KernelSliceFromSomeFreeTip :: (Attestable k', Sliced (Free k') c) => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c

Instances

Instances details

(Oriented c, Sliced i c) => Show (KernelSliceFromSomeFreeTip n i c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> KernelSliceFromSomeFreeTip n i c -> ShowS # show :: KernelSliceFromSomeFreeTip n i c -> String # showList :: [KernelSliceFromSomeFreeTip n i c] -> ShowS #
(Distributive c, Sliced i c, XStandardOrtSiteTo c, Typeable n) => Validable (KernelSliceFromSomeFreeTip n i c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: KernelSliceFromSomeFreeTip n i c -> Statement Source #

ksfKernel :: KernelSliceFromSomeFreeTip n i c -> Kernel n c Source #

the underlying kernel.

Kernel

type KernelFree = LimesFree Dst Projective (Parallel LeftToRight) N2 Source #

kernel of a diagram with free points.

type KernelDiagramFree = DiagramFree (Parallel LeftToRight) N2 Source #

kerne diagram with free points.

Cokernel

type CokernelDiagramFree = DiagramFree (Parallel RightToLeft) N2 Source #

cokernel diagrams with free points.

Pullback

type PullbackFree n c = LimesFree Mlt Projective (Star To) (n + 1) n c Source #

pullback of a diagram with free points.

type PullbackDiagramFree n c = DiagramFree (Star To) (n + 1) n c Source #

pullback diagram with free points.