{-# LANGUAGE
    TypeOperators
  , TypeFamilies
  , GADTs
  , PolyKinds
  , DataKinds
  , Rank2Types
  , ViewPatterns
  , TypeSynonymInstances
  , FlexibleContexts
  , FlexibleInstances
  , UndecidableInstances
  , NoImplicitPrelude
  #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Category.Monoidal
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  sjoerd@w3future.com
-- Stability   :  experimental
-- Portability :  non-portable
-----------------------------------------------------------------------------
module Data.Category.Monoidal where

import Data.Category
import Data.Category.Functor
import Data.Category.NaturalTransformation
import Data.Category.Adjunction
import Data.Category.Limit
import Data.Category.Product
import Data.Category.KanExtension

import GHC.Exts (FUN)
import GHC.Types (Multiplicity(One))


-- | A monoidal category is a category with some kind of tensor product.
--   A tensor product is a bifunctor, with a unit object.
class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where

  type Unit f :: Kind (Cod f)
  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))

class TensorProduct f => SymmetricTensorProduct f where
  swap :: Cod f ~ k => f -> Obj k a -> Obj k b -> k (f :% (a, b)) (f :% (b, a))

-- | If a category has all products, then the product functor makes it a monoidal category,
--   with the terminal object as unit.
instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) where

  type Unit (ProductFunctor k) = TerminalObject k
  unitObject :: ProductFunctor k
-> Obj (Cod (ProductFunctor k)) (Unit (ProductFunctor k))
unitObject ProductFunctor k
_ = forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod (ProductFunctor k) ~ k) =>
ProductFunctor k
-> Obj k a
-> k (ProductFunctor k :% (Unit (ProductFunctor k), a)) a
leftUnitor     ProductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj k a
a
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (ProductFunctor k) ~ k) =>
ProductFunctor k
-> Obj k a
-> k a (ProductFunctor k :% (Unit (ProductFunctor k), a))
leftUnitorInv  ProductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj k a
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj k a
a
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod (ProductFunctor k) ~ k) =>
ProductFunctor k
-> Obj k a
-> k (ProductFunctor k :% (a, Unit (ProductFunctor k))) a
rightUnitor    ProductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k a
a forall {k} (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (ProductFunctor k) ~ k) =>
ProductFunctor k
-> Obj k a
-> k a (ProductFunctor k :% (a, Unit (ProductFunctor k)))
rightUnitorInv ProductFunctor k
_ Obj k a
a = Obj k a
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj k a
a

  associator :: forall (k :: * -> * -> *) a b c.
(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)))
associator    ProductFunctor k
_ Obj k a
a Obj k b
b Obj k c
c = (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k a
a Obj k b
b forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 (Obj k a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj k b
b) Obj k c
c) forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k a
a Obj k b
b forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj k c
c)
  associatorInv :: forall (k :: * -> * -> *) a b c.
(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))
associatorInv ProductFunctor k
_ Obj k a
a Obj k b
b Obj k c
c = (Obj k a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k b
b Obj k c
c) forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k b
b Obj k c
c forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k a
a (Obj k b
b forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Obj k c
c))

instance (HasTerminalObject k, HasBinaryProducts k) => SymmetricTensorProduct (ProductFunctor k) where
  swap :: forall (k :: * -> * -> *) a b.
(Cod (ProductFunctor k) ~ k) =>
ProductFunctor k
-> Obj k a
-> Obj k b
-> k (ProductFunctor k :% (a, b)) (ProductFunctor k :% (b, a))
swap ProductFunctor k
_ Obj k a
a Obj k b
b = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) y
proj2 Obj k a
a Obj k b
b forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryProducts k =>
Obj k x -> Obj k y -> k (BinaryProduct k x y) x
proj1 Obj k a
a Obj k b
b

-- | If a category has all coproducts, then the coproduct functor makes it a monoidal category,
--   with the initial object as unit.
instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where

  type Unit (CoproductFunctor k) = InitialObject k
  unitObject :: CoproductFunctor k
-> Obj (Cod (CoproductFunctor k)) (Unit (CoproductFunctor k))
unitObject CoproductFunctor k
_ = forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod (CoproductFunctor k) ~ k) =>
CoproductFunctor k
-> Obj k a
-> k (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) a
leftUnitor     CoproductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj k a
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj k a
a
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (CoproductFunctor k) ~ k) =>
CoproductFunctor k
-> Obj k a
-> k a (CoproductFunctor k :% (Unit (CoproductFunctor k), a))
leftUnitorInv  CoproductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj k a
a
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod (CoproductFunctor k) ~ k) =>
CoproductFunctor k
-> Obj k a
-> k (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) a
rightUnitor    CoproductFunctor k
_ Obj k a
a = Obj k a
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj k a
a
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (CoproductFunctor k) ~ k) =>
CoproductFunctor k
-> Obj k a
-> k a (CoproductFunctor k :% (a, Unit (CoproductFunctor k)))
rightUnitorInv CoproductFunctor k
_ Obj k a
a = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k a
a forall {k} (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  associator :: forall (k :: * -> * -> *) a b c.
(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)))
associator    CoproductFunctor k
_ Obj k a
a Obj k b
b Obj k c
c = (Obj k a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k b
b Obj k c
c) forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k a
a (Obj k b
b forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ Obj k c
c) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k b
b Obj k c
c)
  associatorInv :: forall (k :: * -> * -> *) a b c.
(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))
associatorInv CoproductFunctor k
_ Obj k a
a Obj k b
b Obj k c
c = (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 (Obj k a
a forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ Obj k b
b) Obj k c
c forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k a
a Obj k b
b) forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| (forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k a
a Obj k b
b forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryCoproducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)
+++ Obj k c
c)

instance (HasInitialObject k, HasBinaryCoproducts k) => SymmetricTensorProduct (CoproductFunctor k) where
  swap :: forall (k :: * -> * -> *) a b.
(Cod (CoproductFunctor k) ~ k) =>
CoproductFunctor k
-> Obj k a
-> Obj k b
-> k (CoproductFunctor k :% (a, b)) (CoproductFunctor k :% (b, a))
swap CoproductFunctor k
_ Obj k a
a Obj k b
b = forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k y (BinaryCoproduct k x y)
inj2 Obj k b
b Obj k a
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| forall {k} (k :: k -> k -> *) (x :: k) (y :: k).
HasBinaryCoproducts k =>
Obj k x -> Obj k y -> k x (BinaryCoproduct k x y)
inj1 Obj k b
b Obj k a
a

-- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit.
instance Category k => TensorProduct (EndoFunctorCompose k) where

  type Unit (EndoFunctorCompose k) = Id k
  unitObject :: EndoFunctorCompose k
-> Obj (Cod (EndoFunctorCompose k)) (Unit (EndoFunctorCompose k))
unitObject EndoFunctorCompose k
_ = forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (k :: * -> * -> *). Id k
Id

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod (EndoFunctorCompose k) ~ k) =>
EndoFunctorCompose k
-> Obj k a
-> k (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a)) a
leftUnitor     EndoFunctorCompose k
_ (Nat a
g a
_ forall z. Obj k z -> Component a a z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (Id (Cod f) :.: f) f
idPostcomp a
g
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (EndoFunctorCompose k) ~ k) =>
EndoFunctorCompose k
-> Obj k a
-> k a (EndoFunctorCompose k :% (Unit (EndoFunctorCompose k), a))
leftUnitorInv  EndoFunctorCompose k
_ (Nat a
g a
_ forall z. Obj k z -> Component a a z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (Id (Cod f) :.: f)
idPostcompInv a
g
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod (EndoFunctorCompose k) ~ k) =>
EndoFunctorCompose k
-> Obj k a
-> k (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k))) a
rightUnitor    EndoFunctorCompose k
_ (Nat a
g a
_ forall z. Obj k z -> Component a a z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp a
g
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (EndoFunctorCompose k) ~ k) =>
EndoFunctorCompose k
-> Obj k a
-> k a (EndoFunctorCompose k :% (a, Unit (EndoFunctorCompose k)))
rightUnitorInv EndoFunctorCompose k
_ (Nat a
g a
_ forall z. Obj k z -> Component a a z
_) = forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv a
g

  associator :: forall (k :: * -> * -> *) a b c.
(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)))
associator    EndoFunctorCompose k
_ (Nat a
f a
_ forall z. Obj k z -> Component a a z
_) (Nat b
g b
_ forall z. Obj k z -> Component b b z
_) (Nat c
h c
_ forall z. Obj k z -> Component c c z
_) = forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) ((f :.: g) :.: h) (f :.: (g :.: h))
compAssoc a
f b
g c
h
  associatorInv :: forall (k :: * -> * -> *) a b c.
(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))
associatorInv EndoFunctorCompose k
_ (Nat a
f a
_ forall z. Obj k z -> Component a a z
_) (Nat b
g b
_ forall z. Obj k z -> Component b b z
_) (Nat c
h c
_ forall z. Obj k z -> Component c c z
_) = forall f g h.
(Functor f, Functor g, Functor h, Dom f ~ Cod g, Dom g ~ Cod h) =>
f
-> g
-> h
-> Nat (Dom h) (Cod f) (f :.: (g :.: h)) ((f :.: g) :.: h)
compAssocInv a
f b
g c
h

data LinearTensor = LinearTensor
instance Functor LinearTensor where
  type Dom LinearTensor = FUN 'One :**: FUN 'One
  type Cod LinearTensor = FUN 'One
  type LinearTensor :% (a, b) = (a, b)

  LinearTensor
LinearTensor % :: forall a b.
LinearTensor
-> Dom LinearTensor a b
-> Cod LinearTensor (LinearTensor :% a) (LinearTensor :% b)
% (a1 %1 -> b1
f :**: a2 %1 -> b2
g) = \(a1
a, a2
b) -> (a1 %1 -> b1
f a1
a, a2 %1 -> b2
g a2
b)

instance TensorProduct LinearTensor where
  type Unit LinearTensor = ()
  unitObject :: LinearTensor -> Obj (Cod LinearTensor) (Unit LinearTensor)
unitObject LinearTensor
_ = forall a. Obj (->) a
obj

  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a -> k (LinearTensor :% (Unit LinearTensor, a)) a
leftUnitor     LinearTensor
_ Obj k a
_ = \((), a
a) -> a
a
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a -> k a (LinearTensor :% (Unit LinearTensor, a))
leftUnitorInv  LinearTensor
_ Obj k a
_ = \a
a -> ((), a
a)
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a -> k (LinearTensor :% (a, Unit LinearTensor)) a
rightUnitor    LinearTensor
_ Obj k a
_ = \(a
a, ()) -> a
a
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a -> k a (LinearTensor :% (a, Unit LinearTensor))
rightUnitorInv LinearTensor
_ Obj k a
_ = \a
a -> (a
a, ())
  associator :: forall (k :: * -> * -> *) a b c.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a
-> Obj k b
-> Obj k c
-> k (LinearTensor :% (LinearTensor :% (a, b), c))
     (LinearTensor :% (a, LinearTensor :% (b, c)))
associator    LinearTensor
_ Obj k a
_ Obj k b
_ Obj k c
_ = \((a
a, b
b), c
c) -> (a
a, (b
b, c
c))
  associatorInv :: forall (k :: * -> * -> *) a b c.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a
-> Obj k b
-> Obj k c
-> k (LinearTensor :% (a, LinearTensor :% (b, c)))
     (LinearTensor :% (LinearTensor :% (a, b), c))
associatorInv LinearTensor
_ Obj k a
_ Obj k b
_ Obj k c
_ = \(a
a, (b
b, c
c)) -> ((a
a, b
b), c
c)

instance SymmetricTensorProduct LinearTensor where
  swap :: forall (k :: * -> * -> *) a b.
(Cod LinearTensor ~ k) =>
LinearTensor
-> Obj k a
-> Obj k b
-> k (LinearTensor :% (a, b)) (LinearTensor :% (b, a))
swap LinearTensor
_ Obj k a
_ Obj k b
_ = \(a
a, b
b) -> (b
b, a
a)


-- | Day convolution
data Day t = Day t
instance TensorProduct t => Functor (Day t) where
  type Dom (Day t) = Nat (Cod t) (->) :**: Nat (Cod t) (->)
  type Cod (Day t) = Nat (Cod t) (->)
  type Day t :% (f, g) = LanHaskF t (ProductFunctor (->) :.: (f :***: g))
  Day t
_ % :: forall a b.
Day t -> Dom (Day t) a b -> Cod (Day t) (Day t :% a) (Day t :% b)
% (Nat (Cod t) (->) a1 b1
nf :**: Nat (Cod t) (->) a2 b2
ng) =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall p f. LanHaskF p f
LanHaskF forall p f. LanHaskF p f
LanHaskF (\Obj (Cod t) z
_ (LanHask x :: Obj (Dom t) c
x@(Cod t a1 b1
x1 :**: Cod t a2 b2
x2) Cod t (t :% c) z
tx (ProductFunctor (->) :.: (a1 :***: a2)) :% c
fgx) -> forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask Obj (Dom t) c
x Cod t (t :% c) z
tx ((Nat (Cod t) (->) a1 b1
nf forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Cod t a1 b1
x1 forall {k} (k :: k -> k -> *) (a1 :: k) (b1 :: k) (a2 :: k)
       (b2 :: k).
HasBinaryProducts k =>
k a1 b1
-> k a2 b2 -> k (BinaryProduct k a1 a2) (BinaryProduct k b1 b2)
*** Nat (Cod t) (->) a2 b2
ng forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
! Cod t a2 b2
x2) (ProductFunctor (->) :.: (a1 :***: a2)) :% c
fgx))

instance TensorProduct t => TensorProduct (Day t) where
  type Unit (Day t) = Curry1 (Op (Cod t)) (Cod t) (Hom (Cod t)) :% Unit t
  unitObject :: Day t -> Obj (Cod (Day t)) (Unit (Day t))
unitObject (Day t
t) = forall f (c1 :: * -> * -> *) (c2 :: * -> * -> *).
(Functor f, Dom f ~ (c1 :**: c2), Category c1, Category c2) =>
f -> Curry1 c1 c2 f
Curry1 forall (k :: * -> * -> *). Hom k
Hom forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall {k} {k} (k :: k -> k -> *) (a :: k) (b :: k).
k b a -> Op k a b
Op (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t)
  leftUnitor :: forall (k :: * -> * -> *) a.
(Cod (Day t) ~ k) =>
Day t -> Obj k a -> k (Day t :% (Unit (Day t), a)) a
leftUnitor (Day t
t) (NatId a
a) =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall p f. LanHaskF p f
LanHaskF a
a (\Obj (Cod t) z
_ (LanHask (Dom a a1 b1
_ :**: Dom a a2 b2
c2) Cod t (t :% c) z
tcz (Dom a (Unit t) b1
uc1, a :% b2
ac2)) -> (a
a forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod t (t :% c) z
tcz forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Dom a (Unit t) b1
uc1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Dom a a2 b2
c2) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv t
t Dom a a2 b2
c2)) a :% b2
ac2)
  leftUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (Day t) ~ k) =>
Day t -> Obj k a -> k a (Day t :% (Unit (Day t), a))
leftUnitorInv (Day t
t) (NatId a
a) =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
a forall p f. LanHaskF p f
LanHaskF (\Obj (Dom a) z
z a :% z
az -> forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Obj (Dom a) z
z) (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitor t
t Obj (Dom a) z
z) (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t, a :% z
az))
  rightUnitor :: forall (k :: * -> * -> *) a.
(Cod (Day t) ~ k) =>
Day t -> Obj k a -> k (Day t :% (a, Unit (Day t))) a
rightUnitor (Day t
t) (NatId a
a) =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall p f. LanHaskF p f
LanHaskF a
a (\Obj (Cod t) z
_ (LanHask (Dom a a1 b1
c1 :**: Dom a a2 b2
_) Cod t (t :% c) z
tcz (a :% b1
ac1, Dom a (Unit t) b2
uc2)) -> (a
a forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod t (t :% c) z
tcz forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Dom a a1 b1
c1 forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Dom a (Unit t) b2
uc2) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (a, Unit f))
rightUnitorInv t
t Dom a a1 b1
c1)) a :% b1
ac1)
  rightUnitorInv :: forall (k :: * -> * -> *) a.
(Cod (Day t) ~ k) =>
Day t -> Obj k a -> k a (Day t :% (a, Unit (Day t)))
rightUnitorInv (Day t
t) (NatId a
a) =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat a
a forall p f. LanHaskF p f
LanHaskF (\Obj (Dom a) z
z a :% z
az -> forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (Obj (Dom a) z
z forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t) (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (a, Unit f)) a
rightUnitor t
t Obj (Dom a) z
z) (a :% z
az, forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject t
t))
  associator :: forall (k :: * -> * -> *) a b c.
(Cod (Day t) ~ k) =>
Day t
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Day t :% (Day t :% (a, b), c))
     (Day t :% (a, Day t :% (b, c)))
associator (Day t
t) Obj k a
_ Obj k b
_ Obj k c
_ =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall p f. LanHaskF p f
LanHaskF forall p f. LanHaskF p f
LanHaskF (\Obj (Cod t) z
_ (LanHask (Cod t a1 b1
_e :**: Cod t a2 b2
d) Cod t (t :% c) z
eda (LanHask (Cod t a1 b1
b :**: Cod t a2 b2
c) Cod t (t :% c) b1
bce (a :% b1
fb, b :% b2
gc), c :% b2
hd)) ->
      let cd :: (:**:) (Cod t) (Cod t) (a2, a2) (b2, b2)
cd = Cod t a2 b2
c forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t a2 b2
d; tcd :: Cod t (t :% (b2, b2)) (t :% (b2, b2))
tcd = t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (:**:) (Cod t) (Cod t) (a2, a2) (b2, b2)
cd
      in forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (Cod t a1 b1
b forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t (t :% (b2, b2)) (t :% (b2, b2))
tcd) (Cod t (t :% c) z
eda forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod t (t :% c) b1
bce forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t a2 b2
d) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c))
associatorInv t
t Cod t a1 b1
b Cod t a2 b2
c Cod t a2 b2
d) (a :% b1
fb, forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (:**:) (Cod t) (Cod t) (a2, a2) (b2, b2)
cd Cod t (t :% (b2, b2)) (t :% (b2, b2))
tcd (b :% b2
gc, c :% b2
hd)))
  associatorInv :: forall (k :: * -> * -> *) a b c.
(Cod (Day t) ~ k) =>
Day t
-> Obj k a
-> Obj k b
-> Obj k c
-> k (Day t :% (a, Day t :% (b, c)))
     (Day t :% (Day t :% (a, b), c))
associatorInv (Day t
t) Obj k a
_ Obj k b
_ Obj k c
_ =
    forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall p f. LanHaskF p f
LanHaskF forall p f. LanHaskF p f
LanHaskF (\Obj (Cod t) z
_ (LanHask (Cod t a1 b1
b :**: Cod t a2 b2
_c) Cod t (t :% c) z
bca (a :% b1
fb, LanHask (Cod t a1 b1
d :**: Cod t a2 b2
e) Cod t (t :% c) b2
dec (b :% b1
gd, c :% b2
he))) ->
      let bd :: (:**:) (Cod t) (Cod t) (a1, a1) (b1, b1)
bd = Cod t a1 b1
b forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t a1 b1
d; tbd :: Cod t (t :% (b1, b1)) (t :% (b1, b1))
tbd = t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (:**:) (Cod t) (Cod t) (a1, a1) (b1, b1)
bd
      in forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (Cod t (t :% (b1, b1)) (t :% (b1, b1))
tbd forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t a2 b2
e) (Cod t (t :% c) z
bca forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. t
t forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod t a1 b1
b forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: Cod t (t :% c) b2
dec) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a b c.
(TensorProduct f, Cod f ~ k) =>
f
-> Obj k a
-> Obj k b
-> Obj k c
-> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c)))
associator t
t Cod t a1 b1
b Cod t a1 b1
d Cod t a2 b2
e) (forall p k a f.
Obj (Dom p) k -> Cod p (p :% k) a -> (f :% k) -> LanHask p f a
LanHask (:**:) (Cod t) (Cod t) (a1, a1) (b1, b1)
bd Cod t (t :% (b1, b1)) (t :% (b1, b1))
tbd (a :% b1
fb, b :% b1
gd), c :% b2
he))


-- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
data MonoidObject f a = MonoidObject
  { forall f a. MonoidObject f a -> Cod f (Unit f) a
unit     :: Cod f (Unit f)      a
  , forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply :: Cod f (f :% (a, a)) a
  }

trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f)
trivialMonoid :: forall f. TensorProduct f => f -> MonoidObject f (Unit f)
trivialMonoid f
f = forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f) (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitor f
f (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f))

coproductMonoid :: (HasInitialObject k, HasBinaryCoproducts k) => Obj k a -> MonoidObject (CoproductFunctor k) a
coproductMonoid :: forall (k :: * -> * -> *) a.
(HasInitialObject k, HasBinaryCoproducts k) =>
Obj k a -> MonoidObject (CoproductFunctor k) a
coproductMonoid Obj k a
a = forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (forall {k} (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj k a
a) (Obj k a
a forall {k} (k :: k -> k -> *) (x :: k) (a :: k) (y :: k).
HasBinaryCoproducts k =>
k x a -> k y a -> k (BinaryCoproduct k x y) a
||| Obj k a
a)


-- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@.
data ComonoidObject f a = ComonoidObject
  { forall f a. ComonoidObject f a -> Cod f a (Unit f)
counit     :: Cod f a (Unit f)
  , forall f a. ComonoidObject f a -> Cod f a (f :% (a, a))
comultiply :: Cod f a (f :% (a, a))
  }

trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f)
trivialComonoid :: forall f. TensorProduct f => f -> ComonoidObject f (Unit f)
trivialComonoid f
f = forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f) (forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f))

productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a
productComonoid :: forall (k :: * -> * -> *) a.
(HasTerminalObject k, HasBinaryProducts k) =>
Obj k a -> ComonoidObject (ProductFunctor k) a
productComonoid Obj k a
a = forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (forall {k} (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj k a
a) (Obj k a
a forall {k} (k :: k -> k -> *) (a :: k) (x :: k) (y :: k).
HasBinaryProducts k =>
k a x -> k a y -> k a (BinaryProduct k x y)
&&& Obj k a
a)


data MonoidAsCategory f m a b where
  MonoidValue :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k)
              => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m

-- | A monoid as a category with one object.
instance Category (MonoidAsCategory f m) where

  src :: forall a b.
MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) a
src (MonoidValue f
f MonoidObject f m
m k (Unit f) m
_) = forall f (k :: * -> * -> *) m.
(TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) =>
f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
MonoidValue f
f MonoidObject f m
m (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f m
m)
  tgt :: forall a b.
MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) b
tgt (MonoidValue f
f MonoidObject f m
m k (Unit f) m
_) = forall f (k :: * -> * -> *) m.
(TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) =>
f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
MonoidValue f
f MonoidObject f m
m (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f m
m)

  MonoidValue f
f MonoidObject f m
m k (Unit f) m
a . :: forall b c a.
MonoidAsCategory f m b c
-> MonoidAsCategory f m a b -> MonoidAsCategory f m a c
. MonoidValue f
_ MonoidObject f m
_ k (Unit f) m
b = forall f (k :: * -> * -> *) m.
(TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) =>
f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
MonoidValue f
f MonoidObject f m
m (forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject f m
m forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (k (Unit f) m
a forall (c1 :: * -> * -> *) k b1 (c2 :: * -> * -> *) a2 b2.
c1 k b1 -> c2 a2 b2 -> (:**:) c1 c2 (k, a2) (b1, b2)
:**: k (Unit f) m
b) forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f))


-- | A monad is a monoid in the category of endofunctors.
type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f

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
mkMonad :: forall f (k :: * -> * -> *).
(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
mkMonad f
f forall a. Obj k a -> Component (Id k) f a
ret forall a. Obj k a -> Component (f :.: f) f a
join = MonoidObject
  { unit :: Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) f
unit     = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat forall (k :: * -> * -> *). Id k
Id        f
f forall a. Obj k a -> Component (Id k) f a
ret
  , multiply :: Cod (EndoFunctorCompose k) (EndoFunctorCompose k :% (f, f)) f
multiply = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) f
f forall a. Obj k a -> Component (f :.: f) f a
join
  }

monadFunctor :: Monad f -> f
monadFunctor :: forall f. Monad f -> f
monadFunctor (forall f a. MonoidObject f a -> Cod f (Unit f) a
unit -> Nat Id (Dom f)
_ f
f forall z. Obj (Dom f) z -> Component (Id (Dom f)) f z
_) = f
f

idMonad :: Category k => Monad (Id k)
idMonad :: forall (k :: * -> * -> *). Category k => Monad (Id k)
idMonad = forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (k :: * -> * -> *). Id k
Id) (forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp forall (k :: * -> * -> *). Id k
Id)


-- | A comonad is a comonoid in the category of endofunctors.
type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f

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
mkComonad :: forall f (k :: * -> * -> *).
(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
mkComonad f
f forall a. Obj k a -> Component f (Id k) a
extr forall a. Obj k a -> Component f (f :.: f) a
dupl = ComonoidObject
  { counit :: Cod (EndoFunctorCompose k) f (Unit (EndoFunctorCompose k))
counit     = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f forall (k :: * -> * -> *). Id k
Id        forall a. Obj k a -> Component f (Id k) a
extr
  , comultiply :: Cod (EndoFunctorCompose k) f (EndoFunctorCompose k :% (f, f))
comultiply = forall f g (c :: * -> * -> *) (d :: * -> * -> *).
(Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f,
 d ~ Cod g) =>
f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
Nat f
f (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) forall a. Obj k a -> Component f (f :.: f) a
dupl
  }

idComonad :: Category k => Comonad (Id k)
idComonad :: forall (k :: * -> * -> *). Category k => Comonad (Id k)
idComonad = forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId forall (k :: * -> * -> *). Id k
Id) (forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv forall (k :: * -> * -> *). Id k
Id)


-- | Every adjunction gives rise to an associated monad.
adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) =
  let MonoidObject Cod
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f)))
  (Unit (EndoFunctorCompose (Dom ((g :.: Id c) :.: f))))
  ((g :.: Id c) :.: f)
ret Cod
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f)))
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f))
   :% ((g :.: Id c) :.: f, (g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
mult = forall m (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Dom m ~ c) =>
Adjunction c d f g -> Monad m -> Monad ((g :.: m) :.: f)
adjunctionMonadT Adjunction c d f g
adj forall (k :: * -> * -> *). Category k => Monad (Id k)
idMonad
  in forall f (k :: * -> * -> *).
(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
mkMonad (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (Cod
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f)))
  (Unit (EndoFunctorCompose (Dom ((g :.: Id c) :.: f))))
  ((g :.: Id c) :.: f)
ret forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!) (Cod
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f)))
  (EndoFunctorCompose (Dom ((g :.: Id c) :.: f))
   :% ((g :.: Id c) :.: f, (g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
mult forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)

-- | Every adjunction gives rise to an associated monad transformer.
adjunctionMonadT :: (Dom m ~ c) => Adjunction c d f g -> Monad m -> Monad (g :.: m :.: f)
adjunctionMonadT :: forall m (c :: * -> * -> *) (d :: * -> * -> *) f g.
(Dom m ~ c) =>
Adjunction c d f g -> Monad m -> Monad ((g :.: m) :.: f)
adjunctionMonadT adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (MonoidObject ret :: Cod
  (EndoFunctorCompose (Dom m)) (Unit (EndoFunctorCompose (Dom m))) m
ret@(Nat Id c
_ m
m forall z. Obj c z -> Component (Id c) m z
_) Cod
  (EndoFunctorCompose (Dom m))
  (EndoFunctorCompose (Dom m) :% (m, m))
  m
mult) = forall f (k :: * -> * -> *).
(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
mkMonad (g
g forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: m
m forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f)
  ((forall f h. f -> h -> Wrap f h
Wrap g
g f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cod
  (EndoFunctorCompose (Dom m)) (Unit (EndoFunctorCompose (Dom m))) m
ret forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv g
g forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId f
f forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  ((forall f h. f -> h -> Wrap f h
Wrap g
g f
f forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (Cod
  (EndoFunctorCompose (Dom m))
  (EndoFunctorCompose (Dom m) :% (m, m))
  m
mult forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp m
m forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId m
m forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f h. f -> h -> Wrap f h
Wrap m
m m
m forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)

-- | Every adjunction gives rise to an associated comonad.
adjunctionComonad :: Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad :: forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Comonad (f :.: g)
adjunctionComonad adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) =
  let ComonoidObject Cod
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g)))
  ((f :.: Id d) :.: g)
  (Unit (EndoFunctorCompose (Dom ((f :.: Id d) :.: g))))
extr Cod
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g)))
  ((f :.: Id d) :.: g)
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g))
   :% ((f :.: Id d) :.: g, (f :.: Id d) :.: g))
dupl = forall w (d :: * -> * -> *) (c :: * -> * -> *) f g.
(Dom w ~ d) =>
Adjunction c d f g -> Comonad w -> Comonad ((f :.: w) :.: g)
adjunctionComonadT Adjunction c d f g
adj forall (k :: * -> * -> *). Category k => Comonad (Id k)
idComonad
  in forall f (k :: * -> * -> *).
(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
mkComonad (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) (Cod
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g)))
  ((f :.: Id d) :.: g)
  (Unit (EndoFunctorCompose (Dom ((f :.: Id d) :.: g))))
extr forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!) (Cod
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g)))
  ((f :.: Id d) :.: g)
  (EndoFunctorCompose (Dom ((f :.: Id d) :.: g))
   :% ((f :.: Id d) :.: g, (f :.: Id d) :.: g))
dupl forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)

-- | Every adjunction gives rise to an associated comonad transformer.
adjunctionComonadT :: (Dom w ~ d) => Adjunction c d f g -> Comonad w -> Comonad (f :.: w :.: g)
adjunctionComonadT :: forall w (d :: * -> * -> *) (c :: * -> * -> *) f g.
(Dom w ~ d) =>
Adjunction c d f g -> Comonad w -> Comonad ((f :.: w) :.: g)
adjunctionComonadT adj :: Adjunction c d f g
adj@(Adjunction f
f g
g Profunctors c d (Costar f) (Star g)
_ Profunctors c d (Star g) (Costar f)
_) (ComonoidObject extr :: Cod
  (EndoFunctorCompose (Dom w)) w (Unit (EndoFunctorCompose (Dom w)))
extr@(Nat w
w Id d
_ forall z. Obj d z -> Component w (Id d) z
_) Cod
  (EndoFunctorCompose (Dom w))
  w
  (EndoFunctorCompose (Dom w) :% (w, w))
dupl) = forall f (k :: * -> * -> *).
(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
mkComonad (f
f forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: w
w forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g)
  ((forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp f
f forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId g
g forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f h. f -> h -> Wrap f h
Wrap f
f g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Cod
  (EndoFunctorCompose (Dom w)) w (Unit (EndoFunctorCompose (Dom w)))
extr) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  ((forall f h. f -> h -> Wrap f h
Wrap f
f g
g forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (forall f h. f -> h -> Wrap f h
Wrap w
w w
w forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv w
w forall (c :: * -> * -> *) (d :: * -> * -> *) (e :: * -> * -> *) j k
       f g.
(Category c, Category d, Category e) =>
Nat d e j k -> Nat c d f g -> Nat c e (j :.: f) (k :.: g)
`o` forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId w
w forall {k} (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Cod
  (EndoFunctorCompose (Dom w))
  w
  (EndoFunctorCompose (Dom w) :% (w, w))
dupl)) forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)