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

OAlg.Category.NaturalTransformable

Contents

Transformable
Natural
Duality
Proposition

Description

Natural transformable applications.

Synopsis

class (Natural (ObjectClass a) b f g, FunctorialG f a b, FunctorialG g a b) => NaturalTransformable (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type)
data NaturalTransformation (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where
- NaturalTransformation :: forall (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type). NaturalTransformable a b f g => NaturalTransformation a b f g
roh' :: forall (a :: Type -> Type -> Type) b f g x. NaturalTransformation a b f g -> Struct (ObjectClass a) x -> b (f x) (g x)
type NaturalFunctorial (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) = (NaturalTransformable a b f g, FunctorialG f a b, FunctorialG g a b)
class Natural s (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where
- roh :: Struct s x -> b (f x) (g x)
class NaturalTransformable h b (Dual1 f) (Dual1 g) => NaturalTransformableDual1 (h :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type)
prpNaturalTransformable :: forall (a :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type). NaturalTransformation a (->) f g -> X (SomeNaturalApplication a f g) -> Statement
data SomeNaturalApplication (a :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where
- SomeNaturalApplication :: forall (a :: Type -> Type -> Type) (g :: Type -> Type) y (f :: Type -> Type) x. (Show2 a, Eq (g y), Show (f x)) => a x y -> f x -> SomeNaturalApplication a f g
relNaturalTransformable :: forall a (g :: Type -> Type) y f x. (Show2 a, Eq (g y), Show (f x)) => NaturalTransformation a (->) f g -> a x y -> f x -> Statement

Transformable

class (Natural (ObjectClass a) b f g, FunctorialG f a b, FunctorialG g a b) => NaturalTransformable (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) Source #

natural generalized associations.

Property Let NaturalTransformable s a b f g and n in 'NatrualTransormation s a b r f g, then holds:

For all x, y and a in a x y holds: amapG a . roh' n (domain a) .=. roh' n (range a) . amapG a.

Instances

Instances details

(HomOrientedDisjunctive h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG Diagram t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic
(CategoryDisjunctive h, HomSlicedOriented i h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG (SliceDiagram i) t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG DiagramFree t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG Cone Dst p d t n m)) (SDualBi (ConeG Cone Dst p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomMultiplicativeDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG Cone Mlt p d t n m)) (SDualBi (ConeG Cone Mlt p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Duality
(HomDistributiveDisjunctive h, FunctorialOriented h, NaturalDiagrammaticBi h d t n m, p ~ Dual (Dual p)) => NaturalTransformable h (->) (SDualBi (ConeG ConeZeroHead Mlt p d t n m)) (SDualBi (ConeG Cone Mlt p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.ZeroHead.Duality
(CategoryDisjunctive h, HomSlicedDistributive i h, FunctorialOriented h, p ~ Dual (Dual p), t ~ Dual (Dual t), s ~ Dst) => NaturalTransformable (Inv2 h) (->) (SDualBi (ConeG (LiftableCone i) s p Diagram t n m)) (SDualBi (ConeG Cone s p Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Liftable

data NaturalTransformation (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where Source #

witness for a NaturalTransformable.

Constructors

NaturalTransformation :: forall (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type). NaturalTransformable a b f g => NaturalTransformation a b f g

roh' :: forall (a :: Type -> Type -> Type) b f g x. NaturalTransformation a b f g -> Struct (ObjectClass a) x -> b (f x) (g x) Source #

the induced roh.

type NaturalFunctorial (a :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) = (NaturalTransformable a b f g, FunctorialG f a b, FunctorialG g a b) Source #

natural transformables admitting the functorial propperty.

Natural

class Natural s (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where Source #

natural associations on s-structured types between f and g within b.

Methods

roh :: Struct s x -> b (f x) (g x) Source #

Instances

Instances details

Conic c => Natural r (->) (SDualBi (ConeG c s p d t n m)) (SDualBi (ConeG Cone s p d t n m)) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Core Methods roh :: Struct r x -> SDualBi (ConeG c s p d t n m) x -> SDualBi (ConeG Cone s p d t n m) x Source #
Diagrammatic d => Natural s (->) (SDualBi (DiagramG d t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods roh :: Struct s x -> SDualBi (DiagramG d t n m) x -> SDualBi (DiagramG Diagram t n m) x Source #
Diagrammatic d => Natural s (->) (DiagramG d t n m) (DiagramG Diagram t n m) Source #
Instance details Defined in OAlg.Entity.Diagram.Diagrammatic Methods roh :: Struct s x -> DiagramG d t n m x -> DiagramG Diagram t n m x Source #
Natural r (->) (Cone s p d t n m) (DiagramG d t n m) Source #
Instance details Defined in OAlg.Limes.Cone.Core Methods roh :: Struct r x -> Cone s p d t n m x -> DiagramG d t n m x Source #
Conic c => Natural r (->) (ConeG c s p d t n m) (ConeG Cone s p d t n m) Source #
Instance details Defined in OAlg.Limes.Cone.Conic.Core Methods roh :: Struct r x -> ConeG c s p d t n m x -> ConeG Cone s p d t n m x Source #

Duality

class NaturalTransformable h b (Dual1 f) (Dual1 g) => NaturalTransformableDual1 (h :: Type -> Type -> Type) (b :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) Source #

helper class to avoid undecidable instances.

Proposition

prpNaturalTransformable :: forall (a :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type). NaturalTransformation a (->) f g -> X (SomeNaturalApplication a f g) -> Statement Source #

validity according to NaturalTransformable for some applications.

data SomeNaturalApplication (a :: Type -> Type -> Type) (f :: Type -> Type) (g :: Type -> Type) where Source #

some f-indexed application.

Constructors

SomeNaturalApplication :: forall (a :: Type -> Type -> Type) (g :: Type -> Type) y (f :: Type -> Type) x. (Show2 a, Eq (g y), Show (f x)) => a x y -> f x -> SomeNaturalApplication a f g

relNaturalTransformable :: forall a (g :: Type -> Type) y f x. (Show2 a, Eq (g y), Show (f x)) => NaturalTransformation a (->) f g -> a x y -> f x -> Statement Source #

validity according to NaturalTransformable for some applications.