Data.Category.Functor

Documentation

data family Funct c d a b :: *

Functor category Funct(C, D), or D^C. Arrows of Funct(C, D) are natural transformations. Each category C needs its own data instance.

data FunctO c d f

Objects of Funct(C, D) are functors from C to D.

Constructors

(Dom f ~ c, Cod f ~ d) => FunctO f

Instances

(Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA CoprodInHask (FunctO Pair (->) f) (FunctO Pair (->) g)

(Dom f ~ Pair, Cod f ~ (->), Dom g ~ Pair, Cod g ~ (->)) => FunctorA ProdInHask (FunctO Pair (->) f) (FunctO Pair (->) g)

CategoryO (Funct Void d) (FunctO Void d f)

(CategoryO (Cod f) (F f Fst), CategoryO (Cod f) (F f Snd)) => CategoryO (Funct Pair d) (FunctO Pair d f)

(CategoryO (Cod f) (F f Fls), CategoryO (Cod f) (F f Tru)) => CategoryO (Funct Boolean d) (FunctO Boolean d f)

(Dom f ~ Omega, Cod f ~ d, CategoryO (Cod f) (F f Z)) => CategoryO (Funct Omega d) (FunctO Omega d f)

type Component f g z = Cod f (F f z) (F g z)

type :~> f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Funct c d (FunctO c d f) (FunctO c d g)

data Diag j (~>)

The diagonal functor from (index-) category J to (~>).

Constructors

Diag

Instances

(CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag (->) ~>) a b

(CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag Void ~>) a b

(CategoryO ~> a, CategoryO ~> b) => FunctorA (Diag Pair ~>) a b

type InitMorF x u = (x :*-: Cod u) :.: u

type TermMorF x u = (Cod u :-*: x) :.: u

data InitialUniversal x u a

Constructors

InitialUniversal (F (InitMorF x u) a) (InitMorF x u :~> (a :*-: Dom u))

data TerminalUniversal x u a

Constructors

TerminalUniversal (F (TermMorF x u) a) (TermMorF x u :~> (Dom u :-*: a))

type Cone f n = Const (Dom f) (Cod f) n :~> f

A cone from N to F is a natural transformation from the constant functor to N to F.

type Cocone f n = f :~> Const (Dom f) (Cod f) n

A co-cone from F to N is a natural transformation from F to the constant functor to N.

type Limit f l = TerminalUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l

type Colimit f l = InitialUniversal (FunctO (Dom f) (Cod f) f) (Diag (Dom f) (Cod f)) l

data Adjunction f g

Constructors

Adjunction

Fields

unit :: Id (Dom f) :~> (g :.: f)

counit :: (f :.: g) :~> Id (Dom g)