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

OAlg.Category.Proposition

Contents

Category
Application
Functorial
Cayleyan2
X
- Categroy
- Functorial
Inv2

Description

propositions on categories.

Synopsis

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

Application

type XAppl (h :: Type -> Type -> Type) = X (SomeApplication h) Source #

random variable for some application.

Functorial

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

validity of a Functorial category.

data XFnct (c :: Type -> Type -> Type) where Source #

random variable for Functorial categories.

Constructors

XFnct :: forall (c :: Type -> Type -> Type). X (SomeEntity c) -> X (SomeCmpbAppl c) -> XFnct c

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

validity according to OAlg.Category.Category.

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

validity according to OAlg.Category.Category.

data SomeCmpbAppl (c :: Type -> Type -> Type) where Source #

some composable morphisms with an applicable value.

Constructors

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

prpFunctorialG :: forall (t :: Type -> Type) (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) q. (FunctorialG t a b, EqExt b) => q t a b -> X (SomeObjectClass a) -> X (SomeCmpb2 a) -> Statement Source #

validity according to FunctorialG.

prpFunctorialGType :: forall (t :: Type -> Type) (a :: Type -> Type -> Type). FunctorialG t a (->) => X (SomeEntityG t a) -> X (SomeCmpb2G t a) -> Statement Source #

validity acording to represatnable FunctorialGs.

data SomeEntityG (t :: Type -> Type) (c :: Type -> Type -> Type) where Source #

some object class for c with a applicable t-entity.

Constructors

SomeEntityG :: forall (t :: Type -> Type) x (c :: Type -> Type -> Type). Entity (t x) => Struct (ObjectClass c) x -> t x -> SomeEntityG t c

data SomeCmpb2G (t :: Type -> Type) (c :: Type -> Type -> Type) where Source #

some combosables for c with a applicable t-entity.

Constructors

SomeCmpb2G :: forall (t :: Type -> Type) x z (c :: Type -> Type -> Type) y. (Entity (t x), Entity (t z)) => c y z -> c x y -> t x -> SomeCmpb2G t c

Cayleyan2

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

validity of Cayleyan2.

X

Categroy

xCat :: forall (c :: Type -> Type -> Type) (s :: Site). Category c => XMrphSite s c -> XCat c Source #

random variable for validating Category.

data XMrphSite (s :: Site) (m :: Type -> Type -> Type) 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 :: forall (m :: Type -> Type -> Type). X (SomeObjectClass m) -> (forall x. Struct (ObjectClass m) x -> X (SomeMorphismSite 'From m x)) -> XMrphSite 'From m
XRange :: forall (m :: Type -> Type -> Type). 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 :: forall (m :: Type -> Type -> Type) (s :: Site) x. 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 :: forall (m :: Type -> Type -> Type) (s :: Site). Morphism m => XMrphSite s m -> N -> X (SomePath m) Source #

derived random variable for some paths.

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

constructing random variable for some path site.

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

constructing random variable for some path.

Functorial

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

random variable for Functorial Categorys.

xMrphSite :: forall (s :: Site) (m :: Type -> Type -> Type). XFnctMrphSite s m -> XMrphSite s m Source #

random variable for Morphisms for a given Site.

data XFnctMrphSite (s :: Site) (m :: Type -> Type -> Type) where Source #

random variable for Functorial Categorys.

Constructors

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

Inv2

relInvEq2 :: forall (c :: Type -> Type -> Type) x y. (Category c, Eq2 c, Show2 c) => Inv2 c x y -> Statement Source #

validity according to Inv2.

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