Data.Category.Monoidal

Documentation

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

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

Minimal complete definition

unitObject, leftUnitor, leftUnitorInv, rightUnitor, rightUnitorInv, associator, associatorInv

Associated Types

type Unit f :: *

Methods

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

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

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

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

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

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

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

Instances

TensorProduct Add

Associated Types

type Unit Add :: *

Methods

unitObject :: Add -> Obj (Cod Add) (Unit Add)

leftUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (Unit Add, a))

rightUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a

rightUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (a, Unit Add))

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

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

TensorProduct Add

Ordinal addition makes the simplex category a monoidal category, with 0 as unit.

Associated Types

type Unit Add :: *

Methods

unitObject :: Add -> Obj (Cod Add) (Unit Add)

leftUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (Unit Add, a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (Unit Add, a))

rightUnitor :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k (Add :% (a, Unit Add)) a

rightUnitorInv :: ((* -> * -> *) ~ Cod Add) k => Add -> Obj k a -> k a (Add :% (a, Unit Add))

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

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

Category k => TensorProduct (EndoFunctorCompose k)

Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.

Associated Types

type Unit (EndoFunctorCompose k) :: *

Methods

unitObject :: EndoFunctorCompose k -> Obj (Cod (EndoFunctorCompose k)) (Unit (EndoFunctorCompose k))

leftUnitor :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> k (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> k a (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a))

rightUnitor :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> k (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) a

rightUnitorInv :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> k a (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k)))

associator :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> Obj k b -> Obj k c -> k (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c)) (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c)))

associatorInv :: ((* -> * -> *) ~ Cod (EndoFunctorCompose k)) k => EndoFunctorCompose k -> Obj k a -> Obj k b -> Obj k c -> k (EndoFunctorCompose k :% (a, EndoFunctorCompose k :% (b, c))) (EndoFunctorCompose k :% (EndoFunctorCompose k :% (a, b), c))

(HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k)

If a category has all coproducts, then the coproduct functor makes it a monoidal category, with the initial object as unit.

Associated Types

type Unit (CoproductFunctor k) :: *

Methods

unitObject :: CoproductFunctor k -> Obj (Cod (CoproductFunctor k)) (Unit (CoproductFunctor k))

leftUnitor :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> k (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> k a (CoproductFunctor k :% (Unit (CoproductFunctor k), a))

rightUnitor :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> k (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) a

rightUnitorInv :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> k a (CoproductFunctor k :% (a, Unit (CoproductFunctor k)))

associator :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> Obj k b -> Obj k c -> k (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c)) (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c)))

associatorInv :: ((* -> * -> *) ~ Cod (CoproductFunctor k)) k => CoproductFunctor k -> Obj k a -> Obj k b -> Obj k c -> k (CoproductFunctor k :% (a, CoproductFunctor k :% (b, c))) (CoproductFunctor k :% (CoproductFunctor k :% (a, b), c))

(HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k)

If a category has all products, then the product functor makes it a monoidal category, with the terminal object as unit.

Associated Types

type Unit (ProductFunctor k) :: *

Methods

unitObject :: ProductFunctor k -> Obj (Cod (ProductFunctor k)) (Unit (ProductFunctor k))

leftUnitor :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> k (ProductFunctor k :% (Unit (ProductFunctor k), a)) a

leftUnitorInv :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> k a (ProductFunctor k :% (Unit (ProductFunctor k), a))

rightUnitor :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> k (ProductFunctor k :% (a, Unit (ProductFunctor k))) a

rightUnitorInv :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> k a (ProductFunctor k :% (a, Unit (ProductFunctor k)))

associator :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> Obj k b -> Obj k c -> k (ProductFunctor k :% (ProductFunctor k :% (a, b), c)) (ProductFunctor k :% (a, ProductFunctor k :% (b, c)))

associatorInv :: ((* -> * -> *) ~ Cod (ProductFunctor k)) k => ProductFunctor k -> Obj k a -> Obj k b -> Obj k c -> k (ProductFunctor k :% (a, ProductFunctor k :% (b, c))) (ProductFunctor k :% (ProductFunctor k :% (a, b), c))

data MonoidObject f a

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

Constructors

MonoidObject

Fields

• unit :: Cod f (Unit f) a
• multiply :: Cod f (f :% (a, a)) a

trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)

coproductMonoid :: (HasInitialObject k, HasBinaryCoproducts k) => Obj k a -> MonoidObject (CoproductFunctor k) a

data ComonoidObject f a

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

Constructors

ComonoidObject

Fields

• counit :: Cod f a (Unit f)
• comultiply :: Cod f a (f :% (a, a))

trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)

productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a

data MonoidAsCategory f m a b where

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)

A monoid as a category with one object.

Methods

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

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

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

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

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

monadFunctor :: Monad f -> f

idMonad :: Category k => Monad (Id k)

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

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

idComonad :: Category k => Comonad (Id k)

adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)

Every adjunction gives rise to an associated monad.

adjunctionMonadT :: Dom m ~ c => Adjunction c d f g -> Monad m -> Monad ((g :.: m) :.: f)

Every adjunction gives rise to an associated monad transformer.

adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)

Every adjunction gives rise to an associated comonad.

adjunctionComonadT :: Dom w ~ d => Adjunction c d f g -> Comonad w -> Comonad ((f :.: w) :.: g)

Every adjunction gives rise to an associated comonad transformer.