data-category-0.10: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe
LanguageHaskell2010

Data.Category

Contents

Description

 
Synopsis
  • class Category k where
    • src :: k a b -> Obj k a
    • tgt :: k a b -> Obj k b
    • (.) :: k b c -> k a b -> k a c
  • type Obj k a = k a a
  • type family Kind (k :: o -> o -> *) :: * where ...
  • newtype Op k a b = Op {}

Category

class Category k where Source #

An instance of Category k declares the arrow k as a category.

Methods

src :: k a b -> Obj k a Source #

tgt :: k a b -> Obj k b Source #

(.) :: k b c -> k a b -> k a c infixr 8 Source #

Instances
Category k2 => Category (Op k2 :: k1 -> k1 -> Type) Source #

Op k is opposite category of the category k.

Instance details

Defined in Data.Category

Methods

src :: Op k2 a b -> Obj (Op k2) a Source #

tgt :: Op k2 a b -> Obj (Op k2) b Source #

(.) :: Op k2 b c -> Op k2 a b -> Op k2 a c Source #

Category Unit Source #

Unit is the category with one object.

Instance details

Defined in Data.Category.Unit

Methods

src :: Unit a b -> Obj Unit a Source #

tgt :: Unit a b -> Obj Unit b Source #

(.) :: Unit b c -> Unit a b -> Unit a c Source #

Category Void Source #

Void is the category with no objects.

Instance details

Defined in Data.Category.Void

Methods

src :: Void a b -> Obj Void a Source #

tgt :: Void a b -> Obj Void b Source #

(.) :: Void b c -> Void a b -> Void a c Source #

Category Simplex Source #

The (augmented) simplex category is the category of finite ordinals and order preserving maps.

Instance details

Defined in Data.Category.Simplex

Methods

src :: Simplex a b -> Obj Simplex a Source #

tgt :: Simplex a b -> Obj Simplex b Source #

(.) :: Simplex b c -> Simplex a b -> Simplex a c Source #

Category Cube Source # 
Instance details

Defined in Data.Category.Cube

Methods

src :: Cube a b -> Obj Cube a Source #

tgt :: Cube a b -> Obj Cube b Source #

(.) :: Cube b c -> Cube a b -> Cube a c Source #

Category Boolean Source #

Boolean is the category with true and false as objects, and an arrow from false to true.

Instance details

Defined in Data.Category.Boolean

Methods

src :: Boolean a b -> Obj Boolean a Source #

tgt :: Boolean a b -> Obj Boolean b Source #

(.) :: Boolean b c -> Boolean a b -> Boolean a c Source #

(Functor f, Dom f ~ (Op c :**: d), Cod f ~ ((->) :: Type -> Type -> Type), Category c, Category d) => Category (Cograph f :: Type -> Type -> Type) Source #

The cograph of the profunctor f.

Instance details

Defined in Data.Category.Coproduct

Methods

src :: Cograph f a b -> Obj (Cograph f) a Source #

tgt :: Cograph f a b -> Obj (Cograph f) b Source #

(.) :: Cograph f b c -> Cograph f a b -> Cograph f a c Source #

Category (Kleisli m :: Type -> Type -> Type) Source #

The category of Kleisli arrows.

Instance details

Defined in Data.Category.Kleisli

Methods

src :: Kleisli m a b -> Obj (Kleisli m) a Source #

tgt :: Kleisli m a b -> Obj (Kleisli m) b Source #

(.) :: Kleisli m b c -> Kleisli m a b -> Kleisli m a c Source #

Category (f (Fix f)) => Category (Fix f :: Type -> Type -> Type) Source #

Fix f is the fixed point category for a category combinator f.

Instance details

Defined in Data.Category.Fix

Methods

src :: Fix f a b -> Obj (Fix f) a Source #

tgt :: Fix f a b -> Obj (Fix f) b Source #

(.) :: Fix f b c -> Fix f a b -> Fix f a c Source #

ECategory k => Category (Underlying k :: Type -> Type -> Type) Source #

The underlying category of an enriched category

Instance details

Defined in Data.Category.Enriched

Methods

src :: Underlying k a b -> Obj (Underlying k) a Source #

tgt :: Underlying k a b -> Obj (Underlying k) b Source #

(.) :: Underlying k b c -> Underlying k a b -> Underlying k a c Source #

Category ((->) :: Type -> Type -> Type) Source #

The category with Haskell types as objects and Haskell functions as arrows.

Instance details

Defined in Data.Category

Methods

src :: (a -> b) -> Obj (->) a Source #

tgt :: (a -> b) -> Obj (->) b Source #

(.) :: (b -> c) -> (a -> b) -> a -> c Source #

(Category c1, Category c2) => Category (c1 :**: c2 :: Type -> Type -> Type) Source #

The product category of categories c1 and c2.

Instance details

Defined in Data.Category.Product

Methods

src :: (c1 :**: c2) a b -> Obj (c1 :**: c2) a Source #

tgt :: (c1 :**: c2) a b -> Obj (c1 :**: c2) b Source #

(.) :: (c1 :**: c2) b c -> (c1 :**: c2) a b -> (c1 :**: c2) a c Source #

Category d => Category (Nat c d :: Type -> Type -> Type) Source #

Functor category D^C. Objects of D^C are functors from C to D. Arrows of D^C are natural transformations.

Instance details

Defined in Data.Category.NaturalTransformation

Methods

src :: Nat c d a b -> Obj (Nat c d) a Source #

tgt :: Nat c d a b -> Obj (Nat c d) b Source #

(.) :: Nat c d b c0 -> Nat c d a b -> Nat c d a c0 Source #

(Category c1, Category c2) => Category (c1 :>>: c2 :: Type -> Type -> Type) Source # 
Instance details

Defined in Data.Category.Coproduct

Methods

src :: (c1 :>>: c2) a b -> Obj (c1 :>>: c2) a Source #

tgt :: (c1 :>>: c2) a b -> Obj (c1 :>>: c2) b Source #

(.) :: (c1 :>>: c2) b c -> (c1 :>>: c2) a b -> (c1 :>>: c2) a c Source #

(Category c1, Category c2) => Category (c1 :++: c2 :: Type -> Type -> Type) Source #

The coproduct category of categories c1 and c2.

Instance details

Defined in Data.Category.Coproduct

Methods

src :: (c1 :++: c2) a b -> Obj (c1 :++: c2) a Source #

tgt :: (c1 :++: c2) a b -> Obj (c1 :++: c2) b Source #

(.) :: (c1 :++: c2) b c -> (c1 :++: c2) a b -> (c1 :++: c2) a c Source #

Category (MonoidAsCategory f m :: Type -> Type -> Type) Source #

A monoid as a category with one object.

Instance details

Defined in Data.Category.Monoidal

Methods

src :: MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) a Source #

tgt :: MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) b Source #

(.) :: MonoidAsCategory f m b c -> MonoidAsCategory f m a b -> MonoidAsCategory f m a c Source #

Category (Dialg f g :: Type -> Type -> Type) Source #

The category of (F,G)-dialgebras.

Instance details

Defined in Data.Category.Dialg

Methods

src :: Dialg f g a b -> Obj (Dialg f g) a Source #

tgt :: Dialg f g a b -> Obj (Dialg f g) b Source #

(.) :: Dialg f g b c -> Dialg f g a b -> Dialg f g a c Source #

(Category (Dom t), Category (Dom s)) => Category (t :/\: s :: Type -> Type -> Type) Source #

The comma category T \downarrow S

Instance details

Defined in Data.Category.Comma

Methods

src :: (t :/\: s) a b -> Obj (t :/\: s) a Source #

tgt :: (t :/\: s) a b -> Obj (t :/\: s) b Source #

(.) :: (t :/\: s) b c -> (t :/\: s) a b -> (t :/\: s) a c Source #

Category Cat Source #

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

Instance details

Defined in Data.Category.Functor

Methods

src :: Cat a b -> Obj Cat a Source #

tgt :: Cat a b -> Obj Cat b Source #

(.) :: Cat b c -> Cat a b -> Cat a c Source #

Category AdjArrow Source #

The category with categories as objects and adjunctions as arrows.

Instance details

Defined in Data.Category.Adjunction

Methods

src :: AdjArrow a b -> Obj AdjArrow a Source #

tgt :: AdjArrow a b -> Obj AdjArrow b Source #

(.) :: AdjArrow b c -> AdjArrow a b -> AdjArrow a c Source #

type Obj k a = k a a Source #

Whenever objects are required at value level, they are represented by their identity arrows.

type family Kind (k :: o -> o -> *) :: * where ... Source #

Kind k is the kind of the objects of the category k.

Equations

Kind (k :: o -> o -> *) = o 

Opposite category

newtype Op k a b Source #

Constructors

Op 

Fields

Instances
Category k2 => Category (Op k2 :: k1 -> k1 -> Type) Source #

Op k is opposite category of the category k.

Instance details

Defined in Data.Category

Methods

src :: Op k2 a b -> Obj (Op k2) a Source #

tgt :: Op k2 a b -> Obj (Op k2) b Source #

(.) :: Op k2 b c -> Op k2 a b -> Op k2 a c Source #

HasBinaryProducts k2 => HasBinaryCoproducts (Op k2 :: k1 -> k1 -> Type) Source #

Binary products are the dual of binary coproducts.

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryCoproduct (Op k2) x y :: Kind k Source #

Methods

inj1 :: Obj (Op k2) x -> Obj (Op k2) y -> Op k2 x (BinaryCoproduct (Op k2) x y) Source #

inj2 :: Obj (Op k2) x -> Obj (Op k2) y -> Op k2 y (BinaryCoproduct (Op k2) x y) Source #

(|||) :: Op k2 x a -> Op k2 y a -> Op k2 (BinaryCoproduct (Op k2) x y) a Source #

(+++) :: Op k2 a1 b1 -> Op k2 a2 b2 -> Op k2 (BinaryCoproduct (Op k2) a1 a2) (BinaryCoproduct (Op k2) b1 b2) Source #

HasBinaryCoproducts k2 => HasBinaryProducts (Op k2 :: k1 -> k1 -> Type) Source #

Binary products are the dual of binary coproducts.

Instance details

Defined in Data.Category.Limit

Associated Types

type BinaryProduct (Op k2) x y :: Kind k Source #

Methods

proj1 :: Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) x Source #

proj2 :: Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) y Source #

(&&&) :: Op k2 a x -> Op k2 a y -> Op k2 a (BinaryProduct (Op k2) x y) Source #

(***) :: Op k2 a1 b1 -> Op k2 a2 b2 -> Op k2 (BinaryProduct (Op k2) a1 a2) (BinaryProduct (Op k2) b1 b2) Source #

HasTerminalObject k2 => HasInitialObject (Op k2 :: k1 -> k1 -> Type) Source #

Terminal objects are the dual of initial objects.

Instance details

Defined in Data.Category.Limit

Associated Types

type InitialObject (Op k2) :: Kind k Source #

Methods

initialObject :: Obj (Op k2) (InitialObject (Op k2)) Source #

initialize :: Obj (Op k2) a -> Op k2 (InitialObject (Op k2)) a Source #

HasInitialObject k2 => HasTerminalObject (Op k2 :: k1 -> k1 -> Type) Source #

Terminal objects are the dual of initial objects.

Instance details

Defined in Data.Category.Limit

Associated Types

type TerminalObject (Op k2) :: Kind k Source #

Methods

terminalObject :: Obj (Op k2) (TerminalObject (Op k2)) Source #

terminate :: Obj (Op k2) a -> Op k2 a (TerminalObject (Op k2)) Source #

Category k => CartesianClosed (Presheaves k :: Type -> Type -> Type) Source #

The category of presheaves on a category C is cartesian closed for any C.

Instance details

Defined in Data.Category.CartesianClosed

Associated Types

type Exponential (Presheaves k) y z :: Kind k Source #

type InitialObject (Op k2 :: k1 -> k1 -> Type) Source # 
Instance details

Defined in Data.Category.Limit

type InitialObject (Op k2 :: k1 -> k1 -> Type) = TerminalObject k2
type TerminalObject (Op k2 :: k1 -> k1 -> Type) Source # 
Instance details

Defined in Data.Category.Limit

type TerminalObject (Op k2 :: k1 -> k1 -> Type) = InitialObject k2
type BinaryCoproduct (Op k2 :: k1 -> k1 -> Type) (x :: Kind (Op k2)) (y :: Kind (Op k2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryCoproduct (Op k2 :: k1 -> k1 -> Type) (x :: Kind (Op k2)) (y :: Kind (Op k2)) = BinaryProduct k2 x y
type BinaryProduct (Op k2 :: k1 -> k1 -> Type) (x :: Kind (Op k2)) (y :: Kind (Op k2)) Source # 
Instance details

Defined in Data.Category.Limit

type BinaryProduct (Op k2 :: k1 -> k1 -> Type) (x :: Kind (Op k2)) (y :: Kind (Op k2)) = BinaryCoproduct k2 x y
type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) ((->) :: Type -> Type -> Type))) (z :: Kind (Nat (Op k) ((->) :: Type -> Type -> Type))) Source # 
Instance details

Defined in Data.Category.CartesianClosed

type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) ((->) :: Type -> Type -> Type))) (z :: Kind (Nat (Op k) ((->) :: Type -> Type -> Type))) = PShExponential k y z