data-category-0.3.1.1: Restricted categories

Portabilitynon-portable
Stabilityexperimental
Maintainersjoerd@w3future.com

Data.Category.Functor

Contents

Description

 

Synopsis

Cat

data Cat whereSource

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 Source

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

Functors

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

The domain, or source category, of the functor.

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

The codomain, or target category, of the functor.

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

Functors map objects and arrows.

Methods

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

% 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 :: *Source

:% maps objects.

Functor instances

data Id (~>) Source

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 whereSource

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 whereSource

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

data :*-: whereSource

The covariant functor Hom(X,--)

Constructors

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

Instances

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

data :-*: whereSource

The contravariant functor Hom(--,X)

Constructors

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

Instances

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

data Opposite f whereSource

The dual of a functor

Constructors

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

Instances

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

data EndoHask whereSource

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

Constructors

EndoHask :: Functor f => EndoHask f 

Instances

Universal properties

data InitialUniversal x u a Source

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 Source

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