oalg-base-1.1.4.0: Algebraic structures on oriented entities and limits as a tool kit to solve algebraic problems.

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

OAlg.Category.Proposition

Contents

Category
Application
Functorial
Cayleyan2
X
- Categroy
- Functorial

Description

propositions on categories.

Synopsis

prpCategory :: (Category c, Eq2 c, Show2 c) => XCat c -> Statement
data XCat c = XCat {
- xcSomeMrph :: X (SomeMorphism c)
- xcSomeCmpb3 :: X (SomeCmpb3 c)
}
prpCategory1 :: (Category c, Show2 c, Eq2 c) => X (SomeMorphism c) -> Statement
prpCategory2 :: (Category c, Show2 c, Eq2 c) => X (SomeCmpb3 c) -> Statement
data SomeCmpb3 c where
- SomeCmpb3 :: c x w -> c y x -> c z y -> SomeCmpb3 c
type XAppl h = X (SomeApplication h)
prpFunctorial :: (Functorial c, Show2 c) => XFnct c -> Statement
data XFnct c where
- XFnct :: X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c
prpFunctorial1 :: (Functorial c, Show2 c) => X (SomeEntity c) -> Statement
prpFunctorial2 :: (Functorial c, Show2 c) => X (SomeCmpbAppl c) -> Statement
data SomeCmpbAppl c where
- SomeCmpbAppl :: (Entity x, Eq z) => c y z -> c x y -> x -> SomeCmpbAppl c
prpCayleyan2 :: (Cayleyan2 c, Show2 c) => X (SomeMorphism c) -> Statement
xCat :: Category c => XMrphSite s c -> XCat c
data XMrphSite (s :: Site) m where
- XDomain :: X (SomeObjectClass m) -> (forall x. Struct (ObjectClass m) x -> X (SomeMorphismSite From m x)) -> XMrphSite From m
- XRange :: X (SomeObjectClass m) -> (forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite To m y)) -> XMrphSite To m
xSomePathSiteMax :: Morphism m => XMrphSite s m -> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x)
xSomePathMax :: Morphism m => XMrphSite s m -> N -> X (SomePath m)
xSomePathSite :: Category c => XMrphSite s c -> N -> Struct (ObjectClass c) x -> X (SomePathSite s c x)
xSomePath :: Category c => XMrphSite s c -> N -> X (SomePath c)
xFnct :: (Category c, Transformable (ObjectClass c) Ent) => XFnctMrphSite s c -> XFnct c
xMrphSite :: XFnctMrphSite s m -> XMrphSite s m
data XFnctMrphSite s m where
- XFnctMrphSite :: XMrphSite s m -> (forall x. Struct (ObjectClass m) x -> X x) -> XFnctMrphSite s m

Category

prpCategory :: (Category c, Eq2 c, Show2 c) => XCat c -> Statement Source #

validity of a Category.

data XCat c Source #

random variable for validating Category.

Constructors

XCat
Fields xcSomeMrph :: X (SomeMorphism c) xcSomeCmpb3 :: X (SomeCmpb3 c)

prpCategory1 :: (Category c, Show2 c, Eq2 c) => X (SomeMorphism c) -> Statement Source #

validity according to OAlg.Category.Category.

prpCategory2 :: (Category c, Show2 c, Eq2 c) => X (SomeCmpb3 c) -> Statement Source #

validity according to OAlg.Category.Category.

data SomeCmpb3 c where Source #

some composable morphisms.

Constructors

SomeCmpb3 :: c x w -> c y x -> c z y -> SomeCmpb3 c

Application

type XAppl h = X (SomeApplication h) Source #

random variable for some application.

Functorial

prpFunctorial :: (Functorial c, Show2 c) => XFnct c -> Statement Source #

validity of a Functorial category.

data XFnct c where Source #

random variable for Functorial categories.

Constructors

XFnct :: X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c

prpFunctorial1 :: (Functorial c, Show2 c) => X (SomeEntity c) -> Statement Source #

validity according to OAlg.Category.Category.

prpFunctorial2 :: (Functorial c, Show2 c) => X (SomeCmpbAppl c) -> Statement Source #

validity according to OAlg.Category.Category.

data SomeCmpbAppl c where Source #

some composable morphisms with an applicable value.

Constructors

SomeCmpbAppl :: (Entity x, Eq z) => c y z -> c x y -> x -> SomeCmpbAppl c

Cayleyan2

prpCayleyan2 :: (Cayleyan2 c, Show2 c) => X (SomeMorphism c) -> Statement Source #

validity of Cayleyan2.

X

Categroy

xCat :: Category c => XMrphSite s c -> XCat c Source #

random variable for validating Category.

data XMrphSite (s :: Site) m where Source #

random variable of SomeObjectClass and SomeMorphismSite with:

Note

The random variable X (SomeObjectClass m) should have a bias towards non terminal respectively initial object classes. For an implementation see xIsoOpOrtFrom.
It is the analogue to XStart at the level of Categorys.

Constructors

XDomain :: X (SomeObjectClass m) -> (forall x. Struct (ObjectClass m) x -> X (SomeMorphismSite From m x)) -> XMrphSite From m
XRange :: X (SomeObjectClass m) -> (forall y. Struct (ObjectClass m) y -> X (SomeMorphismSite To m y)) -> XMrphSite To m

Instances

Instances details

Dualisable (XMrphSite 'To m) Source #
Instance details Defined in OAlg.Category.Proposition Methods toDual :: XMrphSite 'To m -> Dual (XMrphSite 'To m) Source # fromDual :: Dual (XMrphSite 'To m) -> XMrphSite 'To m Source #
type Dual (XMrphSite s m :: Type) Source #
Instance details Defined in OAlg.Category.Proposition type Dual (XMrphSite s m :: Type) = XMrphSite (Dual s) (Op2 m)

xSomePathSiteMax :: Morphism m => XMrphSite s m -> N -> Struct (ObjectClass m) x -> X (SomePathSite s m x) Source #

random variable of paths of Morphisms having maximal the given length. If during the randomly build path no terminal respectively initial object class has reached then the resulting path will have the given length.

It is the analogue to xStartPathOrt at the level of Categorys.

xSomePathMax :: Morphism m => XMrphSite s m -> N -> X (SomePath m) Source #

derived random variable for some paths.

xSomePathSite :: Category c => XMrphSite s c -> N -> Struct (ObjectClass c) x -> X (SomePathSite s c x) Source #

constructing random variable for some path site.

xSomePath :: Category c => XMrphSite s c -> N -> X (SomePath c) Source #

constructing random variable for some path.

Functorial

xFnct :: (Category c, Transformable (ObjectClass c) Ent) => XFnctMrphSite s c -> XFnct c Source #

random variable for Functorial Categorys.

xMrphSite :: XFnctMrphSite s m -> XMrphSite s m Source #

random variable for Morphisms for a given Site.

data XFnctMrphSite s m where Source #

random variable for Functorial Categorys.

Constructors

XFnctMrphSite :: XMrphSite s m -> (forall x. Struct (ObjectClass m) x -> X x) -> XFnctMrphSite s m