data-category-0.10: Category theory

Data.Category.Monoidal

Description

Synopsis

# Documentation

class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where Source #

A monoidal category is a category with some kind of tensor product. A tensor product is a bifunctor, with a unit object.

Associated Types

type Unit f :: * Source #

Methods

unitObject :: f -> Obj (Cod f) (Unit f) Source #

leftUnitor :: Cod f ~ k => f -> Obj k a -> k (f :% (Unit f, a)) a Source #

leftUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (Unit f, a)) Source #

rightUnitor :: Cod f ~ k => f -> Obj k a -> k (f :% (a, Unit f)) a Source #

rightUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (a, Unit f)) Source #

associator :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c))) Source #

associatorInv :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c)) Source #

Instances
 Source # Ordinal addition makes the simplex category a monoidal category, with 0 as unit. Instance detailsDefined in Data.Category.Simplex Associated Typestype Unit Add :: Type Source # MethodsunitObject :: Add -> Obj (Cod Add) (Unit Add) Source #leftUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a Source #leftUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (Unit Add, a)) Source #rightUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a Source #rightUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (a, Unit Add)) Source #associator :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c))) Source #associatorInv :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c)) Source # Source # Instance detailsDefined in Data.Category.Cube Associated Typestype Unit Add :: Type Source # MethodsunitObject :: Add -> Obj (Cod Add) (Unit Add) Source #leftUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a Source #leftUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (Unit Add, a)) Source #rightUnitor :: Cod Add ~ k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a Source #rightUnitorInv :: Cod Add ~ k => Add -> Obj k a -> k a (Add :% (a, Unit Add)) Source #associator :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (Add :% (a, b), c)) (Add :% (a, Add :% (b, c))) Source #associatorInv :: Cod Add ~ k => Add -> Obj k a -> Obj k b -> Obj k c -> k (Add :% (a, Add :% (b, c))) (Add :% (Add :% (a, b), c)) Source # Source # Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. Instance detailsDefined in Data.Category.Monoidal Associated Typestype Unit (EndoFunctorCompose k) :: Type Source # MethodsleftUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) a Source #leftUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) Source #rightUnitor :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) a Source #rightUnitorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> k0 a (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) Source #associator :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) Source #associatorInv :: Cod (EndoFunctorCompose k) ~ k0 => EndoFunctorCompose k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) Source # Source # If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit. Instance detailsDefined in Data.Category.Monoidal Associated Typestype Unit (CoproductFunctor k) :: Type Source # MethodsleftUnitor :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) a Source #leftUnitorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 a (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) Source #rightUnitor :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) a Source #rightUnitorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> k0 a (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) Source #associator :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c)) (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c))) Source #associatorInv :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c))) (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c)) Source # Source # If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit. Instance detailsDefined in Data.Category.Monoidal Associated Typestype Unit (ProductFunctor k) :: Type Source # MethodsleftUnitor :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 (ProductFunctor k :% (Unit (ProductFunctor k), a)) a Source #leftUnitorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 a (ProductFunctor k :% (Unit (ProductFunctor k), a)) Source #rightUnitor :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 (ProductFunctor k :% (a, Unit (ProductFunctor k))) a Source #rightUnitorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> k0 a (ProductFunctor k :% (a, Unit (ProductFunctor k))) Source #associator :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (ProductFunctor k :% (ProductFunctor k :% (a, b), c)) (ProductFunctor k :% (a, ProductFunctor k :% (b, c))) Source #associatorInv :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> Obj k0 c -> k0 (ProductFunctor k :% (a, ProductFunctor k :% (b, c))) (ProductFunctor k :% (ProductFunctor k :% (a, b), c)) Source # (TensorProduct t, Cod t ~ f (Fix f)) => TensorProduct (WrapTensor (Fix f) t) Source # Fix f inherits tensor products from f (Fix f). Instance detailsDefined in Data.Category.Fix Associated Typestype Unit (WrapTensor (Fix f) t) :: Type Source # MethodsunitObject :: WrapTensor (Fix f) t -> Obj (Cod (WrapTensor (Fix f) t)) (Unit (WrapTensor (Fix f) t)) Source #leftUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) a Source #leftUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (Unit (WrapTensor (Fix f) t), a)) Source #rightUnitor :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) a Source #rightUnitorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> k a (WrapTensor (Fix f) t :% (a, Unit (WrapTensor (Fix f) t))) Source #associator :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) Source #associatorInv :: Cod (WrapTensor (Fix f) t) ~ k => WrapTensor (Fix f) t -> Obj k a -> Obj k b -> Obj k c -> k (WrapTensor (Fix f) t :% (a, WrapTensor (Fix f) t :% (b, c))) (WrapTensor (Fix f) t :% (WrapTensor (Fix f) t :% (a, b), c)) Source #

class TensorProduct f => SymmetricTensorProduct f where Source #

Methods

swap :: Cod f ~ k => f -> Obj k a -> Obj k b -> k (f :% (a, b)) (f :% (b, a)) Source #

Instances
 Source # Instance detailsDefined in Data.Category.Monoidal Methodsswap :: Cod (CoproductFunctor k) ~ k0 => CoproductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (CoproductFunctor k :% (a, b)) (CoproductFunctor k :% (b, a)) Source # Source # Instance detailsDefined in Data.Category.Monoidal Methodsswap :: Cod (ProductFunctor k) ~ k0 => ProductFunctor k -> Obj k0 a -> Obj k0 b -> k0 (ProductFunctor k :% (a, b)) (ProductFunctor k :% (b, a)) Source #

data MonoidObject f a Source #

MonoidObject f a defines a monoid a in a monoidal category with tensor product f.

Constructors

 MonoidObject Fieldsunit :: Cod f (Unit f) a multiply :: Cod f (f :% (a, a)) a

data ComonoidObject f a Source #

ComonoidObject f a defines a comonoid a in a comonoidal category with tensor product f.

Constructors

 ComonoidObject Fieldscounit :: Cod f a (Unit f) comultiply :: Cod f a (f :% (a, a))

data MonoidAsCategory f m a b where Source #

Constructors

 MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
Instances
 Category (MonoidAsCategory f m :: Type -> Type -> Type) Source # A monoid as a category with one object. Instance detailsDefined in Data.Category.Monoidal Methodssrc :: 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 #

type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f Source #

A monad is a monoid in the category of endofunctors.

mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k) => f -> (forall a. Obj k a -> Component (Id k) f a) -> (forall a. Obj k a -> Component (f :.: f) f a) -> Monad f Source #

type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f Source #

A comonad is a comonoid in the category of endofunctors.

mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k) => f -> (forall a. Obj k a -> Component f (Id k) a) -> (forall a. Obj k a -> Component f (f :.: f) a) -> Comonad f Source #