FunctorCategory.FunctorCategory

Given two categories C and D, the FunctorCategory D^C has as objects functors from C to D and as morphisms natural transformations between functors.

Documentation

data NaturalTransformation c1 m1 o1 c2 m2 o2

A NaturalTransformation between two heterogeneous functors from C to D is a mapping from objects of C to morphism of D such that naturality is respected.

Formally, let F and G be functors, and eta : Ob(C) -> Ar(D). The following property should be respected :

source F = source G

target F = target G

Forall f in arrows (source F) : eta(target f) @ F(f) = G(f) @ eta(source f)

Constructors

NaturalTransformation

Fields

• srcNT :: Diagram c1 m1 o1 c2 m2 o2
• tgtNT :: Diagram c1 m1 o1 c2 m2 o2
• component :: o1 -> m2

Instances

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Eq (NaturalTransformation c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

(==) :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool

(/=) :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> Bool

(FiniteCategory c1 m1 o1, Morphism m1 o1, Show c1, Show m1, Show o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Show c2, Show m2, Show o2) => Show (NaturalTransformation c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

showsPrec :: Int -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> ShowS

show :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> String

showList :: [NaturalTransformation c1 m1 o1 c2 m2 o2] -> ShowS

(FiniteCategory c1 m1 o1, Morphism m1 o1, PrettyPrintable c1, PrettyPrintable m1, PrettyPrintable o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, PrettyPrintable c2, PrettyPrintable m2, PrettyPrintable o2) => PrettyPrintable (NaturalTransformation c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

pprint :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> String

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq c1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq c2, Eq m2, Eq o2) => Morphism (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

(@) :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2

source :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2

target :: NaturalTransformation c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => GeneratedFiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

genAr :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

decompose :: FunctorCategory c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

genArrows :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => FiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

ob :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [Diagram c1 m1 o1 c2 m2 o2]

identity :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2

ar :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

arrows :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

preWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3) => NaturalTransformation c2 m2 o2 c3 m3 o3 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3

Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak

postWhiskering :: (FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2, FiniteCategory c3 m3 o3, Morphism m3 o3) => Diagram c2 m2 o2 c3 m3 o3 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c3 m3 o3

Pre-whiskering as defined in Category Theory for the Sciences (2014) by David I. Spivak

data FunctorCategory c1 m1 o1 c2 m2 o2

FunctorCategory D^C.

Constructors

FunctorCategory

Fields

• sourceCat :: c1

  C

• targetCat :: c2

  D

Instances

(Eq c1, Eq c2) => Eq (FunctorCategory c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

(==) :: FunctorCategory c1 m1 o1 c2 m2 o2 -> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool

(/=) :: FunctorCategory c1 m1 o1 c2 m2 o2 -> FunctorCategory c1 m1 o1 c2 m2 o2 -> Bool

(Show c1, Show c2) => Show (FunctorCategory c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

showsPrec :: Int -> FunctorCategory c1 m1 o1 c2 m2 o2 -> ShowS

show :: FunctorCategory c1 m1 o1 c2 m2 o2 -> String

showList :: [FunctorCategory c1 m1 o1 c2 m2 o2] -> ShowS

(PrettyPrintable c1, PrettyPrintable c2) => PrettyPrintable (FunctorCategory c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

pprint :: FunctorCategory c1 m1 o1 c2 m2 o2 -> String

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => GeneratedFiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

genAr :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

decompose :: FunctorCategory c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

genArrows :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

(FiniteCategory c1 m1 o1, Morphism m1 o1, Eq m1, Eq o1, FiniteCategory c2 m2 o2, Morphism m2 o2, Eq m2, Eq o2) => FiniteCategory (FunctorCategory c1 m1 o1 c2 m2 o2) (NaturalTransformation c1 m1 o1 c2 m2 o2) (Diagram c1 m1 o1 c2 m2 o2)

Defined in FunctorCategory.FunctorCategory

Methods

ob :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [Diagram c1 m1 o1 c2 m2 o2]

identity :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> NaturalTransformation c1 m1 o1 c2 m2 o2

ar :: FunctorCategory c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> Diagram c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]

arrows :: FunctorCategory c1 m1 o1 c2 m2 o2 -> [NaturalTransformation c1 m1 o1 c2 m2 o2]