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 (Hom ~>)

Category ~> => Functor (FunctorCompose ~>)

Functor (Cont1 r)

Functor (Cont2 r)

Category ~> => Functor (CodiagCoprod ~>)

Category (Discrete n) => Functor (Succ n)

HasBinaryProducts ~> => Functor (ProductFunctor ~>)

HasBinaryCoproducts ~> => Functor (CoproductFunctor ~>)

CartesianClosed ~> => Functor (ExpFunctor ~>)

Functor f => Functor (Yoneda f)

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

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

HasTerminalObject ~> => Functor (NatF ~>)

(Dom m ~ ~>, Cod m ~ ~>, Functor m) => Functor (EMAdjF m)

(Dom m ~ ~>, Cod m ~ ~>, Functor m) => Functor (EMAdjG m)

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

(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 ~>)

HasLimits j ~> => Functor (LimitFunctor j ~>)

HasColimits j ~> => 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)

(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 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 (->)))

Related to the product category

data Proj1 c1 c2

Proj1 is a bifunctor that projects out the first component of a product.

Constructors

Proj1

Instances

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

data Proj2 c1 c2

Proj2 is a bifunctor that projects out the second component of a product.

Constructors

Proj2

Instances

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

data f1 :***: f2

f1 :***: f2 is the product of the functors f1 and f2.

Constructors

f1 :***: f2

Instances

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

data DiagProd (~>)

DiagProd is the diagonal functor for products.

Constructors

DiagProd

Instances

Category ~> => Functor (DiagProd ~>)

HasInitialObject (Dialg (NatF (->)) (DiagProd (->)))

data Tuple1 c1 c2 a

Tuple1 tuples with a fixed object on the left.

Constructors

Tuple1 (Obj c1 a)

Instances

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

data Tuple2 c1 c2 a

Tuple2 tuples with a fixed object on the right.

Constructors

Tuple2 (Obj c2 a)

Instances

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

Hom functors

data Hom (~>)

The Hom functor, Hom(,), a bifunctor contravariant in its first argument and covariant in its second argument.

Constructors

Hom

Instances

Category ~> => Functor (Hom ~>)

type :*-: x (~>) = Hom ~> :.: Tuple1 (Op ~>) ~> x

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

The covariant functor Hom(X,)

type :-*: (~>) x = Hom ~> :.: Tuple2 (Op ~>) ~> x

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

The contravariant functor Hom(,X)