Data.Category.Functor

Cat

data Cat where

Functors are arrows in the category Cat.

Constructors

CatA :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))

Instances

Category Cat

Cat is the category with categories as objects and funtors as arrows.

HasTerminalObject Cat

Unit is the terminal category.

HasInitialObject Cat

The empty category is the initial object in Cat.

HasBinaryProducts Cat

HasBinaryCoproducts Cat

CartesianClosed Cat

data CatW

We need a wrapper here because objects need to be of kind *, and categories are of kind * -> * -> *.

Functors

type family Dom ftag :: * -> * -> *

The domain, or source category, of the functor.

type family Cod ftag :: * -> * -> *

The codomain, or target category, of the functor.

class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where

Functors map objects and arrows.

Methods

(%) :: ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)

% maps arrows.

Instances

Functor ForgetMonoid

Functor FreeMonoid

Category ~> => Functor (Id ~>)

(Category (Dom f), Category (Cod f)) => Functor (Opposite f)

Functor (EndoHask f)

Category ~> => Functor (DiagProd ~>)

Category ~> => Functor (FunctorCompose ~>)

Category ~> => Functor (YonedaEmbedding ~>)

Functor f => Functor (Yoneda f)

Category ~> => Functor (CodiagCoprod ~>)

(Functor f, Category (PredDiscrete (Dom f))) => Functor (Next f)

HasBinaryProducts ~> => Functor (ProductFunctor ~>)

HasBinaryCoproducts ~> => Functor (CoproductFunctor ~>)

Functor (Cont1 r)

Functor (Cont2 r)

CartesianClosed ~> => Functor (ExpFunctor ~>)

HasTerminalObject ~> => Functor (NatF ~>)

(Category (Cod g), Category (Dom h)) => Functor (:.: g h)

Category ~> => Functor (:*-: x ~>)

Category ~> => Functor (:-*: ~> x)

(Category c1, Category c2) => Functor (Proj1 c1 c2)

(Category c1, Category c2) => Functor (Proj2 c1 c2)

(Functor f1, Functor f2) => Functor (:***: f1 f2)

(Functor f, Category d) => Functor (Precompose f d)

(Functor f, Category c) => Functor (Postcompose f c)

(Functor f, Functor h) => Functor (Wrap f h)

(Category c1, Category c2) => Functor (Inj1 c1 c2)

(Category c1, Category c2) => Functor (Inj2 c1 c2)

(Functor f1, Functor f2) => Functor (:+++: f1 f2)

(Category j, Category ~>) => Functor (Diag j ~>)

(Category j, Category ~>) => Functor (LimitFunctor j ~>)

(Category j, Category ~>) => Functor (ColimitFunctor j ~>)

(Category (Dom p), Category (Cod p)) => Functor (:*: p q)

(Category (Dom p), Category (Cod p)) => Functor (:+: p q)

(Category y, Category z) => Functor (CatApply y z)

(Category y, Category z) => Functor (CatTuple y z)

HasBinaryProducts ~> => Functor (ProductWith ~> y)

CartesianClosed ~> => Functor (ExponentialWith ~> y)

(Dom f ~ c, Cod f ~ d, Dom g ~ c, Cod g ~ d, Functor f, Functor g, Category c, Category d) => Functor (NatAsFunctor f g)

(Dom m ~ ~>, Cod m ~ ~>, Category ~>, Functor m) => Functor (KleisliAdjF ~> m)

(Dom m ~ ~>, Cod m ~ ~>, Category ~>, Functor m) => Functor (KleisliAdjG ~> m)

(Category c1, Category c2) => Functor (Const c1 c2 x)

(Category c1, Category c2) => Functor (Tuple1 c1 c2 a1)

(Category c1, Category c2) => Functor (Tuple2 c1 c2 a2)

(Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1)

(Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2)

(Category ~>, Category (Discrete n), Functor (DiscreteDiagram ~> n xs)) => Functor (DiscreteDiagram ~> (S n) (x, xs))

Category ~> => Functor (DiscreteDiagram ~> Z ())

(Dom p ~ Op ~>, Dom q ~ Op ~>, Cod p ~ (->), Cod q ~ (->), Category ~>, Functor p, Functor q) => Functor (PShExponential ~> p q)

type family ftag :% a :: *

:% maps objects.

Functor instances

data Id (~>)

The identity functor on (~>)

Constructors

Id

Instances

Category ~> => Functor (Id ~>)

Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))

Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->)))

data g :.: h where

The composition of two functors.

Constructors

:.: :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h

Instances

(Category (Cod g), Category (Dom h)) => Functor (:.: g h)

data Const c1 c2 x where

The constant functor.

Constructors

Const :: Category c2 => Obj c2 x -> Const c1 c2 x

Instances

(Category c1, Category c2) => Functor (Const c1 c2 x)

type ConstF f = Const (Dom f) (Cod f)

data :*-: where

The covariant functor Hom(X,--)

Constructors

HomX_ :: Category ~> => Obj ~> x -> x :*-: ~>

Instances

Category ~> => Functor (:*-: x ~>)

data :-*: where

The contravariant functor Hom(--,X)

Constructors

Hom_X :: Category ~> => Obj ~> x -> ~> :-*: x

Instances

Category ~> => Functor (:-*: ~> x)

Category ~> => Representable (:-*: ~> x)

data Opposite f where

The dual of a functor

Constructors

Opposite :: Functor f => f -> Opposite f

Instances

(Category (Dom f), Category (Cod f)) => Functor (Opposite f)

data EndoHask where

EndoHask is a wrapper to turn instances of the Functor class into categorical functors.

Constructors

EndoHask :: Functor f => EndoHask f

Instances

Functor (EndoHask f)

Functor f => HasTerminalObject (Dialg (Id (->)) (EndoHask f))

Functor f => HasInitialObject (Dialg (EndoHask f) (Id (->)))

Universal properties

data InitialUniversal x u a

An initial universal property, a universal morphism from x to u.

Constructors

InitialUniversal

Fields

iuObject :: Obj (Dom u) a

initialMorphism :: Cod u x (u :% a)

initialFactorizer :: forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y

data TerminalUniversal x u a

A terminal universal property, a universal morphism from u to x.

Constructors

TerminalUniversal

Fields

tuObject :: Obj (Dom u) a

terminalMorphism :: Cod u (u :% a) x

terminalFactorizer :: forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a