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.

HasBinaryCoproducts Cat

The coproduct of categories :++: is the binary coproduct in Cat.

HasBinaryProducts Cat

The product of categories :**: is the binary product in Cat.

HasInitialObject Cat

The empty category is the initial object in Cat.

HasTerminalObject Cat

Unit is the terminal category.

CartesianClosed Cat

Exponentials in Cat are the functor categories.

HasNaturalNumberObject Cat

data CatW

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

Functors

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

Functors map objects and arrows.

Associated Types

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

The domain, or source category, of the functor.

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

The codomain, or target category, of the functor.

type ftag :% a :: *

:% maps objects.

Methods

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

% maps arrows.

Instances

Functor Add

Ordinal addition is a bifuntor, it concattenates the maps as it were.

Functor Forget

Turn Simplex x y arrows into Fin x -> Fin y functions.

Category k => Functor (Hom k)

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

Category k => Functor (DiagProd k)

DiagProd is the diagonal functor for products.

Category k => Functor (OpOpInv k)

The x = Op (Op x) functor.

Category k => Functor (OpOp k)

The Op (Op x) = x functor.

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

The dual of a functor

Category k => Functor (Id k)

The identity functor on k

Category k => Functor (Magic k)

Since there is nothing to map in Void, there's a functor from it to any other category.

Category k => Functor (CodiagCoprod k)

CodiagCoprod is the codiagonal functor for coproducts.

HasBinaryCoproducts k => Functor (CoproductFunctor k)

Binary coproduct as a bifunctor.

HasBinaryProducts k => Functor (ProductFunctor k)

Binary product as a bifunctor.

CartesianClosed k => Functor (ExpFunctor k)

The exponential as a bifunctor.

Category (f (Fix f)) => Functor (Wrap f)

The Wrap functor wraps Fix around f (Fix f).

(Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (KleisliAdjG m)

(Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (KleisliAdjF m)

(Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (ForgetAlg m)

ForgetAlg m is the forgetful functor for Alg m.

(Functor m, ~ (* -> * -> *) (Dom m) k, ~ (* -> * -> *) (Cod m) k) => Functor (FreeAlg m)

FreeAlg M takes x to the free algebra (M x, mu_x) of the monad M.

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

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

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

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

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

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

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

The composition of two functors.

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

Wrap f h is the functor such that Wrap f h :% g = f :.: g :.: h, for functors g that compose with f and h.

(Functor f, Functor g, ~ (* -> * -> *) (Dom f) (Dom g), ~ (* -> * -> *) (Cod f) (Cod g)) => Functor (NatAsFunctor f g)

A natural transformation Nat c d is isomorphic to a functor from c :**: 2 to d.

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

f1 :+++: f2 is the coproduct of the functors f1 and f2.

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

Inj2 is a functor which injects into the right category.

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

Inj1 is a functor which injects into the left category.

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

The coproduct of two functors, passing the same object to both functors and taking the coproduct of the results.

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

The product of two functors, passing the same object to both functors and taking the product of the results.

HasColimits j k => Functor (ColimitFunctor j k)

If every diagram of type j has a colimit in k there exists a colimit functor. It can be seen as a generalisation of (+++).

HasLimits j k => Functor (LimitFunctor j k)

If every diagram of type j has a limit in k there exists a limit functor. It can be seen as a generalisation of (***).

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

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

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

Tuple converts an object a to the functor Tuple1 a.

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

Apply is a bifunctor, Apply :% (f, a) applies f to a, i.e. f :% a.

(Category k, Functor f, ~ (* -> * -> *) (Dom f) (Op k), ~ (* -> * -> *) (Cod f) (->)) => Functor (Yoneda k f)

Yoneda converts a functor f into a natural transformation from the hom functor to f.

(Functor z, Functor s, ~ (* -> * -> *) (Dom z) Unit, ~ (* -> * -> *) (Cod z) (Dom s), ~ (* -> * -> *) (Dom s) (Cod s)) => Functor (PrimRec z s)

TensorProduct f => Functor (Replicate f a)

Replicate a monoid a number of times.

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

Tuple1 tuples with a fixed object on the left.

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

The constant functor.

(Category c, Category d, Category e) => Functor (FunctorCompose c d e)

Composition of functors is a functor.

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

Cotuple2 projects out to the right category, replacing a value from the left category with a fixed object.

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

Cotuple1 projects out to the left category, replacing a value from the right category with a fixed object.

Functor instances

data Id k

Constructors

Id

Instances

Category k => Functor (Id k)

The identity functor on k

data g :.: h where

Constructors

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

Instances

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

The composition of two functors.

data Const c1 c2 x where

Constructors

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

Instances

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

The constant functor.

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

The constant functor with the same domain and codomain as f.

data Opposite f where

Constructors

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

Instances

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

The dual of a functor

data OpOp k

Constructors

OpOp

Instances

Category k => Functor (OpOp k)

The Op (Op x) = x functor.

data OpOpInv k

Constructors

OpOpInv

Instances

Category k => Functor (OpOpInv k)

The x = Op (Op x) functor.

Related to the product category

data Proj1 c1 c2

Constructors

Proj1

Instances

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

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

data Proj2 c1 c2

Constructors

Proj2

Instances

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

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

data f1 :***: f2

Constructors

f1 :***: f2

Instances

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

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

data DiagProd k

Constructors

DiagProd

Instances

Category k => Functor (DiagProd k)

DiagProd is the diagonal functor for products.

HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

data Tuple1 c1 c2 a

Constructors

Tuple1 (Obj c1 a)

Instances

HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))

The category for defining the natural numbers and primitive recursion can be described as Dialg(F,G), with F(A)=<1,A> and G(A)=<A,A>.

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

Tuple1 tuples with a fixed object on the left.

type Swap c1 c2 = (Proj2 c1 c2 :***: Proj1 c1 c2) :.: DiagProd (c1 :**: c2)

swap :: (Category c1, Category c2) => Swap c1 c2

swap swaps the 2 categories of the product of categories.

type Tuple2 c1 c2 a = Swap c2 c1 :.: Tuple1 c2 c1 a

tuple2 :: (Category c1, Category c2) => Obj c2 a -> Tuple2 c1 c2 a

Tuple2 tuples with a fixed object on the right.

Hom functors

data Hom k

Constructors

Hom

Instances

Category k => Functor (Hom k)

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

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

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

The covariant functor Hom(X,--)

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

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

The contravariant functor Hom(--,X)