License	BSD-style (see the file LICENSE)
Maintainer	sjoerd@w3future.com
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Category

Contents

Category
Opposite category
(->)/Hask

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 -> Type) :: Type where ...
newtype Op k a b = Op {
- unOp :: k b a
}
obj :: Obj (FUN m) a

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

Instances details

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 :: forall (a :: k) (b :: k). Boolean a b -> Obj Boolean a Source # tgt :: forall (a :: k) (b :: k). Boolean a b -> Obj Boolean b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Boolean b c -> Boolean a b -> Boolean a c Source #
Category Cube Source #
Instance details Defined in Data.Category.Cube Methods src :: forall (a :: k) (b :: k). Cube a b -> Obj Cube a Source # tgt :: forall (a :: k) (b :: k). Cube a b -> Obj Cube b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Cube b c -> Cube a b -> Cube 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 :: forall (a :: k) (b :: k). Simplex a b -> Obj Simplex a Source # tgt :: forall (a :: k) (b :: k). Simplex a b -> Obj Simplex b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Simplex b c -> Simplex a b -> Simplex a c Source #
Category Unit Source #	`Unit` is the category with one object.
Instance details Defined in Data.Category.Unit Methods src :: forall (a :: k) (b :: k). Unit a b -> Obj Unit a Source # tgt :: forall (a :: k) (b :: k). Unit a b -> Obj Unit b Source # (.) :: forall (b :: k) (c :: k) (a :: k). 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 :: forall (a :: k) (b :: k). Void a b -> Obj Void a Source # tgt :: forall (a :: k) (b :: k). Void a b -> Obj Void b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Void b c -> Void a b -> Void 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 :: forall (a :: k0) (b :: k0). Underlying k a b -> Obj (Underlying k) a Source # tgt :: forall (a :: k0) (b :: k0). Underlying k a b -> Obj (Underlying k) b Source # (.) :: forall (b :: k0) (c :: k0) (a :: k0). Underlying k b c -> Underlying k a b -> Underlying k 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 :: forall (a :: k) (b :: k). Fix f a b -> Obj (Fix f) a Source # tgt :: forall (a :: k) (b :: k). Fix f a b -> Obj (Fix f) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Fix f b c -> Fix f a b -> Fix 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 :: forall (a :: k) (b :: k). Kleisli m a b -> Obj (Kleisli m) a Source # tgt :: forall (a :: k) (b :: k). Kleisli m a b -> Obj (Kleisli m) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Kleisli m b c -> Kleisli m a b -> Kleisli m a c Source #
Eq a => Category (Preorder a :: Type -> Type -> Type) Source #
Instance details Defined in Data.Category.Preorder Methods src :: forall (a0 :: k) (b :: k). Preorder a a0 b -> Obj (Preorder a) a0 Source # tgt :: forall (a0 :: k) (b :: k). Preorder a a0 b -> Obj (Preorder a) b Source # (.) :: forall (b :: k) (c :: k) (a0 :: k). Preorder a b c -> Preorder a a0 b -> Preorder a a0 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 :: forall (a :: k) (b :: k). (t :/\: s) a b -> Obj (t :/\: s) a Source # tgt :: forall (a :: k) (b :: k). (t :/\: s) a b -> Obj (t :/\: s) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). (t :/\: s) b c -> (t :/\: s) a b -> (t :/\: s) 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 :: forall (a :: k) (b :: k). (c1 :++: c2) a b -> Obj (c1 :++: c2) a Source # tgt :: forall (a :: k) (b :: k). (c1 :++: c2) a b -> Obj (c1 :++: c2) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). (c1 :++: c2) b c -> (c1 :++: c2) a b -> (c1 :++: c2) a c Source #
(Category c1, Category c2) => Category (c1 :>>: c2 :: Type -> Type -> TYPE LiftedRep) Source #
Instance details Defined in Data.Category.Coproduct Methods src :: forall (a :: k) (b :: k). (c1 :>>: c2) a b -> Obj (c1 :>>: c2) a Source # tgt :: forall (a :: k) (b :: k). (c1 :>>: c2) a b -> Obj (c1 :>>: c2) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). (c1 :>>: c2) b c -> (c1 :>>: c2) a b -> (c1 :>>: c2) 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 :: forall (a :: k) (b :: k). Dialg f g a b -> Obj (Dialg f g) a Source # tgt :: forall (a :: k) (b :: k). Dialg f g a b -> Obj (Dialg f g) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Dialg f g b c -> Dialg f g a b -> Dialg f g 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 :: forall (a :: k) (b :: k). MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) a Source # tgt :: forall (a :: k) (b :: k). MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). MonoidAsCategory f m b c -> MonoidAsCategory f m a b -> MonoidAsCategory f m 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 :: forall (a :: k) (b :: k). Nat c d a b -> Obj (Nat c d) a Source # tgt :: forall (a :: k) (b :: k). Nat c d a b -> Obj (Nat c d) b Source # (.) :: forall (b :: k) (c0 :: k) (a :: k). 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 #	The product category of categories `c1` and `c2`.
Instance details Defined in Data.Category.Product Methods src :: forall (a :: k) (b :: k). (c1 :: c2) a b -> Obj (c1 :: c2) a Source # tgt :: forall (a :: k) (b :: k). (c1 :: c2) a b -> Obj (c1 :: c2) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). (c1 :: c2) b c -> (c1 :: c2) a b -> (c1 :**: c2) a c Source #
ProfunctorOf c d f => Category (Cograph c d f :: Type -> Type -> Type) Source #	The cograph of the profunctor `f`.
Instance details Defined in Data.Category.Coproduct Methods src :: forall (a :: k) (b :: k). Cograph c d f a b -> Obj (Cograph c d f) a Source # tgt :: forall (a :: k) (b :: k). Cograph c d f a b -> Obj (Cograph c d f) b Source # (.) :: forall (b :: k) (c0 :: k) (a :: k). Cograph c d f b c0 -> Cograph c d f a b -> Cograph c d f a c0 Source #
Category (FUN m :: Type -> Type -> Type) Source #	For `m ~ Many`: The category with Haskell types as objects and Haskell functions as arrows, i.e. `(->)`. For `m ~ One`: The category with Haskell types as objects and Haskell linear functions as arrows, i.e. `(%1->)`.
Instance details Defined in Data.Category Methods src :: forall (a :: k) (b :: k). FUN m a b -> Obj (FUN m) a Source # tgt :: forall (a :: k) (b :: k). FUN m a b -> Obj (FUN m) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). FUN m b c -> FUN m a b -> FUN m a c Source #
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 :: forall (a :: k) (b :: k). Op k2 a b -> Obj (Op k2) a Source # tgt :: forall (a :: k) (b :: k). Op k2 a b -> Obj (Op k2) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Op k2 b c -> Op k2 a b -> Op k2 a c Source #
Category (LTE n :: Fin n -> Fin n -> Type) Source #
Instance details Defined in Data.Category.Fin Methods src :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) a Source # tgt :: forall (a :: k) (b :: k). LTE n a b -> Obj (LTE n) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). LTE n b c -> LTE n a b -> LTE n 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 :: forall (a :: k) (b :: k). AdjArrow a b -> Obj AdjArrow a Source # tgt :: forall (a :: k) (b :: k). AdjArrow a b -> Obj AdjArrow b Source # (.) :: forall (b :: k) (c :: k) (a :: k). AdjArrow b c -> AdjArrow a b -> AdjArrow 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 :: forall (a :: k) (b :: k). Cat a b -> Obj Cat a Source # tgt :: forall (a :: k) (b :: k). Cat a b -> Obj Cat b Source # (.) :: forall (b :: k) (c :: k) (a :: k). Cat b c -> Cat a b -> Cat 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 -> Type) :: Type where ... Source #

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

Equations

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

Opposite category

newtype Op k a b Source #

Constructors

Op
Fields unOp :: k b a

Instances

Instances details

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 # Methods apply :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k (BinaryProduct (Presheaves k) (Exponential (Presheaves k) y z) y) z Source # tuple :: forall (y :: k0) (z :: k0). Obj (Presheaves k) y -> Obj (Presheaves k) z -> Presheaves k z (Exponential (Presheaves k) y (BinaryProduct (Presheaves k) z y)) Source # (^^^) :: forall (z1 :: k0) (z2 :: k0) (y2 :: k0) (y1 :: k0). Presheaves k z1 z2 -> Presheaves k y2 y1 -> Presheaves k (Exponential (Presheaves k) y1 z1) (Exponential (Presheaves k) y2 z2) Source #
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 :: forall (a :: k) (b :: k). Op k2 a b -> Obj (Op k2) a Source # tgt :: forall (a :: k) (b :: k). Op k2 a b -> Obj (Op k2) b Source # (.) :: forall (b :: k) (c :: k) (a :: k). 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 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 x (BinaryCoproduct (Op k2) x y) Source # inj2 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 y (BinaryCoproduct (Op k2) x y) Source # (\|\|\|) :: forall (x :: k) (a :: k) (y :: k). Op k2 x a -> Op k2 y a -> Op k2 (BinaryCoproduct (Op k2) x y) a Source # (+++) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) x Source # proj2 :: forall (x :: k) (y :: k). Obj (Op k2) x -> Obj (Op k2) y -> Op k2 (BinaryProduct (Op k2) x y) y Source # (&&&) :: forall (a :: k) (x :: k) (y :: k). Op k2 a x -> Op k2 a y -> Op k2 a (BinaryProduct (Op k2) x y) Source # (***) :: forall (a1 :: k) (b1 :: k) (a2 :: k) (b2 :: k). 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 :: forall (a :: k). 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 :: forall (a :: k). Obj (Op k2) a -> Op k2 a (TerminalObject (Op k2)) Source #
HasColimits j k => HasWColimits k (Const (Op j) (->) ()) Source #	Regular colimits as weigthed colimits, weighted by the constant functor to `()`.
Instance details Defined in Data.Category.WeightedLimit Associated Types type WeightedColimit k (Const (Op j) (->) ()) d Source # Methods colimitObj :: forall (j0 :: Type -> Type -> Type) d. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> Obj k (WColimit (Const (Op j) (->) ()) d) Source # colimit :: forall (j0 :: Type -> Type -> Type) d. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> WeightedCocone (Const (Op j) (->) ()) d (WColimit (Const (Op j) (->) ()) d) Source # colimitFactorizer :: forall (j0 :: Type -> Type -> Type) d e. (FunctorOf j0 k d, Op j0 ~ Dom (Const (Op j) (->) ())) => Const (Op j) (->) () -> d -> Obj k e -> WeightedCocone (Const (Op j) (->) ()) d e -> k (WColimit (Const (Op j) (->) ()) d) e Source #
type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) (->))) (z :: Kind (Nat (Op k) (->))) Source #
Instance details Defined in Data.Category.CartesianClosed type Exponential (Presheaves k :: Type -> Type -> Type) (y :: Kind (Nat (Op k) (->))) (z :: Kind (Nat (Op k) (->))) = PShExponential k y z
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 WeightedColimit k (Const (Op j) (->) ()) d Source #
Instance details Defined in Data.Category.WeightedLimit type WeightedColimit k (Const (Op j) (->) ()) d = Colimit d
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

`(->)`/Hask

obj :: Obj (FUN m) a Source #

Category

Instances

Opposite category

Instances

(->)/Hask

`(->)`/Hask