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.

HasBinaryProducts Cat

HasInitialObject Cat

HasTerminalObject Cat

Unit is the terminal category.

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 Functor ftag where

Functors map objects and arrows. As objects are represented at both the type and value level, we need 3 maps in total.

Methods

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

%% maps objects at the value level.

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

% maps arrows.

Instances

Functor (EndoHask f)

Functor (Opposite f)

Functor (Id ~>)

Functor (YonedaEmbedding ~>)

Functor (VoidDiagram ~>)

Functor (DiagProd ~>)

Functor (Hom ~>)

Functor (NatF ~>)

Functor (:-*: ~> x)

Functor (:*-: x ~>)

Functor (:.: g h)

Functor (Postcompose f c)

Functor (Precompose f d)

Functor (:***: f1 f2)

Functor (Proj2 c1 c2)

Functor (Proj1 c1 c2)

Functor (Next n f)

Functor (ColimitFunctor j ~>)

Functor (LimitFunctor j ~>)

Functor (Diag j ~>)

Functor (KleisliAdjG ~> m)

Functor (KleisliAdjF ~> m)

Functor (Const c1 c2 x)

Functor (PairDiagram ~> x y)

Functor (DiscreteDiagram ~> n xs)

type family ftag :% a :: *

:% maps objects at the type level.

Functor instances

data Id (~>)

The identity functor on (~>)

Constructors

Id

Instances

Functor (Id ~>)

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

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

data g :.: h where

The composition of two functors.

Constructors

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

Instances

Functor (:.: g h)

data Const c1 c2 x where

The constant functor.

Constructors

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

Instances

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

Functor (:*-: x ~>)

data :-*: where

The contravariant functor Hom(--,X)

Constructors

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

Instances

Functor (:-*: ~> x)

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

data Opposite f where

The dual of a functor

Constructors

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

Instances

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 => HasInitialObject (Dialg (EndoHask f) (Id (->)))

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

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