{-# LANGUAGE
    TypeOperators
  , TypeFamilies
  , GADTs
  , Rank2Types
  , ViewPatterns
  , TypeSynonymInstances
  , 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


-- | 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 :: *
  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
_ = Obj (Cod (ProductFunctor k)) (Unit (ProductFunctor k))
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject

  leftUnitor :: ProductFunctor k
-> Obj k a
-> k (ProductFunctor k :% (Unit (ProductFunctor k), a)) a
leftUnitor     ProductFunctor k
_ Obj k a
a = Obj k (TerminalObject k)
-> Obj k a -> k (BinaryProduct k (TerminalObject 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 Obj k (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject Obj k a
a
  leftUnitorInv :: ProductFunctor k
-> Obj k a
-> k a (ProductFunctor k :% (Unit (ProductFunctor k), a))
leftUnitorInv  ProductFunctor k
_ Obj k a
a = Obj k a -> k a (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj k a
a k a (TerminalObject k)
-> Obj k a -> k a (BinaryProduct k (TerminalObject k) 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 :: ProductFunctor k
-> Obj k a
-> k (ProductFunctor k :% (a, Unit (ProductFunctor k))) a
rightUnitor    ProductFunctor k
_ Obj k a
a = Obj k a
-> Obj k (TerminalObject k)
-> k (BinaryProduct k a (TerminalObject k)) 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 Obj k (TerminalObject k)
forall k (k :: k -> k -> *).
HasTerminalObject k =>
Obj k (TerminalObject k)
terminalObject
  rightUnitorInv :: ProductFunctor k
-> Obj k a
-> k a (ProductFunctor k :% (a, Unit (ProductFunctor k)))
rightUnitorInv ProductFunctor k
_ Obj k a
a = Obj k a
a Obj k a
-> k a (TerminalObject k)
-> k a (BinaryProduct k a (TerminalObject k))
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 -> k a (TerminalObject k)
forall k (k :: k -> k -> *) (a :: k).
HasTerminalObject k =>
Obj k a -> k a (TerminalObject k)
terminate Obj k a
a

  associator :: 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 = (Obj k a -> Obj k b -> k (BinaryProduct k a b) 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 Obj k b
b k (BinaryProduct k a b) a
-> k (BinaryProduct k (BinaryProduct k a b) c)
     (BinaryProduct k a b)
-> k (BinaryProduct k (BinaryProduct k a b) c) a
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k (BinaryProduct k a b)
-> Obj k c
-> k (BinaryProduct k (BinaryProduct k a b) c)
     (BinaryProduct k a b)
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 a -> Obj k b -> k (BinaryProduct k a b) (BinaryProduct k a 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 b
b) Obj k c
c) k (BinaryProduct k (BinaryProduct k a b) c) a
-> k (BinaryProduct k (BinaryProduct k a b) c)
     (BinaryProduct k b c)
-> k (BinaryProduct k (BinaryProduct k a b) c)
     (BinaryProduct k a (BinaryProduct k b 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)
&&& (Obj k a -> Obj k b -> k (BinaryProduct k a 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 k (BinaryProduct k a b) b
-> Obj k c
-> k (BinaryProduct k (BinaryProduct k a b) c)
     (BinaryProduct k b c)
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 :: 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 Obj k a
-> k (BinaryProduct k b c) b
-> k (BinaryProduct k a (BinaryProduct k b c))
     (BinaryProduct k a 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 b -> Obj k c -> k (BinaryProduct k b c) b
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) k (BinaryProduct k a (BinaryProduct k b c)) (BinaryProduct k a b)
-> k (BinaryProduct k a (BinaryProduct k b c)) c
-> k (BinaryProduct k a (BinaryProduct k b c))
     (BinaryProduct k (BinaryProduct k a b) 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)
&&& (Obj k b -> Obj k c -> k (BinaryProduct k b c) 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 b
b Obj k c
c k (BinaryProduct k b c) c
-> k (BinaryProduct k a (BinaryProduct k b c))
     (BinaryProduct k b c)
-> k (BinaryProduct k a (BinaryProduct k b c)) c
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a
-> Obj k (BinaryProduct k b c)
-> k (BinaryProduct k a (BinaryProduct k b c))
     (BinaryProduct k b 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 Obj k b -> Obj k c -> k (BinaryProduct k b c) (BinaryProduct k b c)
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 :: 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 = Obj k a -> Obj k b -> k (BinaryProduct k a 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 k (BinaryProduct k a b) b
-> k (BinaryProduct k a b) a
-> k (BinaryProduct k a b) (BinaryProduct k b 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 -> Obj k b -> k (BinaryProduct k a b) 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 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
_ = Obj (Cod (CoproductFunctor k)) (Unit (CoproductFunctor k))
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  leftUnitor :: CoproductFunctor k
-> Obj k a
-> k (CoproductFunctor k :% (Unit (CoproductFunctor k), a)) a
leftUnitor     CoproductFunctor k
_ Obj k a
a = Obj k a -> k (InitialObject k) a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj k a
a k (InitialObject k) a
-> Obj k a -> k (BinaryCoproduct k (InitialObject 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 :: CoproductFunctor k
-> Obj k a
-> k a (CoproductFunctor k :% (Unit (CoproductFunctor k), a))
leftUnitorInv  CoproductFunctor k
_ Obj k a
a = Obj k (InitialObject k)
-> Obj k a -> k a (BinaryCoproduct k (InitialObject k) 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 (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject Obj k a
a
  rightUnitor :: CoproductFunctor k
-> Obj k a
-> k (CoproductFunctor k :% (a, Unit (CoproductFunctor k))) a
rightUnitor    CoproductFunctor k
_ Obj k a
a = Obj k a
a Obj k a
-> k (InitialObject k) a
-> k (BinaryCoproduct k a (InitialObject k)) 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 -> k (InitialObject k) a
forall k (k :: k -> k -> *) (a :: k).
HasInitialObject k =>
Obj k a -> k (InitialObject k) a
initialize Obj k a
a
  rightUnitorInv :: CoproductFunctor k
-> Obj k a
-> k a (CoproductFunctor k :% (a, Unit (CoproductFunctor k)))
rightUnitorInv CoproductFunctor k
_ Obj k a
a = Obj k a
-> Obj k (InitialObject k)
-> k a (BinaryCoproduct k a (InitialObject k))
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 (InitialObject k)
forall k (k :: k -> k -> *).
HasInitialObject k =>
Obj k (InitialObject k)
initialObject

  associator :: 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 Obj k a
-> k b (BinaryCoproduct k b c)
-> k (BinaryCoproduct k a b)
     (BinaryCoproduct k a (BinaryCoproduct k b c))
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 -> Obj k c -> k b (BinaryCoproduct k b 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 b
b Obj k c
c) k (BinaryCoproduct k a b)
  (BinaryCoproduct k a (BinaryCoproduct k b c))
-> k c (BinaryCoproduct k a (BinaryCoproduct k b c))
-> k (BinaryCoproduct k (BinaryCoproduct k a b) c)
     (BinaryCoproduct k a (BinaryCoproduct k b 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
||| (Obj k a
-> Obj k (BinaryCoproduct k b c)
-> k (BinaryCoproduct k b c)
     (BinaryCoproduct k a (BinaryCoproduct k b 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 a
a (Obj k b
b Obj k b
-> Obj k c -> k (BinaryCoproduct k b c) (BinaryCoproduct k b c)
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) k (BinaryCoproduct k b c)
  (BinaryCoproduct k a (BinaryCoproduct k b c))
-> k c (BinaryCoproduct k b c)
-> k c (BinaryCoproduct k a (BinaryCoproduct k b c))
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k b -> Obj k c -> k c (BinaryCoproduct k b 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 :: 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 = (Obj k (BinaryCoproduct k a b)
-> Obj k c
-> k (BinaryCoproduct k a b)
     (BinaryCoproduct k (BinaryCoproduct k a b) 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 a
-> Obj k b -> k (BinaryCoproduct k a b) (BinaryCoproduct k a 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 b
b) Obj k c
c k (BinaryCoproduct k a b)
  (BinaryCoproduct k (BinaryCoproduct k a b) c)
-> k a (BinaryCoproduct k a b)
-> k a (BinaryCoproduct k (BinaryCoproduct k a b) c)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Obj k a -> Obj k b -> k a (BinaryCoproduct k a b)
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) k a (BinaryCoproduct k (BinaryCoproduct k a b) c)
-> k (BinaryCoproduct k b c)
     (BinaryCoproduct k (BinaryCoproduct k a b) c)
-> k (BinaryCoproduct k a (BinaryCoproduct k b c))
     (BinaryCoproduct k (BinaryCoproduct k a b) 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
||| (Obj k a -> Obj k b -> k b (BinaryCoproduct k a 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 a
a Obj k b
b k b (BinaryCoproduct k a b)
-> Obj k c
-> k (BinaryCoproduct k b c)
     (BinaryCoproduct k (BinaryCoproduct k a b) c)
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 :: 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 = Obj k b -> Obj k a -> k a (BinaryCoproduct k b 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 b
b Obj k a
a k a (BinaryCoproduct k b a)
-> k b (BinaryCoproduct k b a)
-> k (BinaryCoproduct k a b) (BinaryCoproduct k b 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 b -> Obj k a -> k b (BinaryCoproduct k b 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
_ = Id k -> Nat (Dom (Id k)) (Cod (Id k)) (Id k) (Id k)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Id k
forall (k :: * -> * -> *). Id k
Id

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

  associator :: 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 f _ _) (Nat g _ _) (Nat h _ _) = a
-> b
-> c
-> Nat (Dom c) (Cod a) ((a :.: b) :.: c) (a :.: (b :.: c))
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 :: 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 f _ _) (Nat g _ _) (Nat h _ _) = a
-> b
-> c
-> Nat (Dom c) (Cod a) (a :.: (b :.: c)) ((a :.: b) :.: c)
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


-- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@.
data MonoidObject f a = MonoidObject
  { MonoidObject f a -> Cod f (Unit f) a
unit     :: Cod f (Unit 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 :: f -> MonoidObject f (Unit f)
trivialMonoid f
f = Cod f (Unit f) (Unit f)
-> Cod f (f :% (Unit f, Unit f)) (Unit f)
-> MonoidObject f (Unit f)
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (f -> Cod f (Unit f) (Unit f)
forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f) (f
-> Cod f (Unit f) (Unit f)
-> Cod f (f :% (Unit f, Unit f)) (Unit f)
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k (f :% (Unit f, a)) a
leftUnitor f
f (f -> Cod f (Unit f) (Unit 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 :: Obj k a -> MonoidObject (CoproductFunctor k) a
coproductMonoid Obj k a
a = Cod (CoproductFunctor k) (Unit (CoproductFunctor k)) a
-> Cod (CoproductFunctor k) (CoproductFunctor k :% (a, a)) a
-> MonoidObject (CoproductFunctor k) a
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (Obj k a -> k (InitialObject k) a
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 Obj k a -> Obj k a -> k (BinaryCoproduct k a 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
  { ComonoidObject f a -> Cod f a (Unit f)
counit     :: Cod f a (Unit f)
  , 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 :: f -> ComonoidObject f (Unit f)
trivialComonoid f
f = Cod f (Unit f) (Unit f)
-> Cod f (Unit f) (f :% (Unit f, Unit f))
-> ComonoidObject f (Unit f)
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (f -> Cod f (Unit f) (Unit f)
forall f. TensorProduct f => f -> Obj (Cod f) (Unit f)
unitObject f
f) (f
-> Cod f (Unit f) (Unit f)
-> Cod f (Unit f) (f :% (Unit f, Unit f))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (f -> Cod f (Unit f) (Unit 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 :: Obj k a -> ComonoidObject (ProductFunctor k) a
productComonoid Obj k a
a = Cod (ProductFunctor k) a (Unit (ProductFunctor k))
-> Cod (ProductFunctor k) a (ProductFunctor k :% (a, a))
-> ComonoidObject (ProductFunctor k) a
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (Obj k a -> k a (TerminalObject k)
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 Obj k a -> Obj k a -> k a (BinaryProduct 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 :: MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) a
src (MonoidValue f
f MonoidObject f m
m k (Unit f) m
_) = f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m 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 (MonoidObject f m -> Cod f (Unit f) m
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit MonoidObject f m
m)
  tgt :: MonoidAsCategory f m a b -> Obj (MonoidAsCategory f m) b
tgt (MonoidValue f
f MonoidObject f m
m k (Unit f) m
_) = f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m 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 (MonoidObject f m -> Cod f (Unit f) 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 . :: 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 = f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m 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 (MonoidObject f m -> Cod f (f :% (m, m)) m
forall f a. MonoidObject f a -> Cod f (f :% (a, a)) a
multiply MonoidObject f m
m k (f :% (m, m)) m -> k (Unit f) (f :% (m, m)) -> k (Unit f) 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 f
-> Dom f (Unit f, Unit f) (m, m)
-> Cod f (f :% (Unit f, Unit f)) (f :% (m, m))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (k (Unit f) m
a k (Unit f) m -> k (Unit f) m -> (:**:) k k (Unit f, Unit f) (m, m)
forall (c1 :: * -> * -> *) a1 b1 (c2 :: * -> * -> *) a2 b2.
c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
:**: k (Unit f) m
b) k (f :% (Unit f, Unit f)) (f :% (m, m))
-> k (Unit f) (f :% (Unit f, Unit f)) -> k (Unit f) (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 -> Obj k (Unit f) -> k (Unit f) (f :% (Unit f, Unit f))
forall f (k :: * -> * -> *) a.
(TensorProduct f, Cod f ~ k) =>
f -> Obj k a -> k a (f :% (Unit f, a))
leftUnitorInv f
f (f -> Obj (Cod f) (Unit 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 :: 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 :: forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject
  { unit :: Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) f
unit     = Id k
-> f
-> (forall a. Obj k a -> Component (Id k) f a)
-> Nat k k (Id k) f
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 Id k
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 = (f :.: f)
-> f
-> (forall a. Obj k a -> Component (f :.: f) f a)
-> Nat k k (f :.: f) f
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 -> 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 :: Monad f -> f
monadFunctor (Monad f
-> Cod
     (EndoFunctorCompose (Dom f)) (Unit (EndoFunctorCompose (Dom f))) f
forall f a. MonoidObject f a -> Cod f (Unit f) a
unit -> Nat _ f _) = f
f

idMonad :: Category k => Monad (Id k)
idMonad :: Monad (Id k)
idMonad = Cod (EndoFunctorCompose k) (Unit (EndoFunctorCompose k)) (Id k)
-> Cod
     (EndoFunctorCompose k)
     (EndoFunctorCompose k :% (Id k, Id k))
     (Id k)
-> MonoidObject (EndoFunctorCompose k) (Id k)
forall f a.
Cod f (Unit f) a -> Cod f (f :% (a, a)) a -> MonoidObject f a
MonoidObject (Id k -> Nat (Dom (Id k)) (Cod (Id k)) (Id k) (Id k)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Id k
forall (k :: * -> * -> *). Id k
Id) (Id k
-> Nat (Dom (Id k)) (Cod (Id k)) (Id k :.: Id (Dom (Id k))) (Id k)
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp Id k
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 :: 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 :: forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject
  { counit :: Cod (EndoFunctorCompose k) f (Unit (EndoFunctorCompose k))
counit     = f
-> Id k
-> (forall a. Obj k a -> Component f (Id k) a)
-> Nat k k f (Id k)
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 Id k
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 = f
-> (f :.: f)
-> (forall a. Obj k a -> Component f (f :.: f) a)
-> Nat k k f (f :.: f)
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 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 :: Comonad (Id k)
idComonad = Cod (EndoFunctorCompose k) (Id k) (Unit (EndoFunctorCompose k))
-> Cod
     (EndoFunctorCompose k)
     (Id k)
     (EndoFunctorCompose k :% (Id k, Id k))
-> ComonoidObject (EndoFunctorCompose k) (Id k)
forall f a.
Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
ComonoidObject (Id k -> Nat (Dom (Id k)) (Cod (Id k)) (Id k) (Id k)
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId Id k
forall (k :: * -> * -> *). Id k
Id) (Id k
-> Nat (Dom (Id k)) (Cod (Id k)) (Id k) (Id k :.: Id (Dom (Id k)))
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv Id k
forall (k :: * -> * -> *). Id k
Id)


-- | Every adjunction gives rise to an associated monad.
adjunctionMonad :: Adjunction c d f g -> Monad (g :.: f)
adjunctionMonad :: 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 d)
  (Unit (EndoFunctorCompose d))
  ((g :.: Id c) :.: f)
ret Cod
  (EndoFunctorCompose d)
  (EndoFunctorCompose d :% ((g :.: Id c) :.: f, (g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
mult = Adjunction c d f g -> Monad (Id c) -> Monad ((g :.: Id c) :.: f)
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 Monad (Id c)
forall (k :: * -> * -> *). Category k => Monad (Id k)
idMonad
  in (g :.: f)
-> (forall a. Obj d a -> Component (Id d) (g :.: f) a)
-> (forall a.
    Obj d a -> Component ((g :.: f) :.: (g :.: f)) (g :.: f) a)
-> Monad (g :.: f)
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 g -> f -> g :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f) (Cod
  (EndoFunctorCompose d)
  (Unit (EndoFunctorCompose d))
  ((g :.: Id c) :.: f)
Nat d d (Id d) ((g :.: Id c) :.: f)
ret Nat d d (Id d) ((g :.: Id c) :.: f)
-> Obj d a -> d (Id d :% a) (((g :.: Id c) :.: f) :% a)
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 d)
  (EndoFunctorCompose d :% ((g :.: Id c) :.: f, (g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
Nat
  d
  d
  (((g :.: Id c) :.: f) :.: ((g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
mult Nat
  d
  d
  (((g :.: Id c) :.: f) :.: ((g :.: Id c) :.: f))
  ((g :.: Id c) :.: f)
-> Obj d a
-> d ((((g :.: Id c) :.: f) :.: ((g :.: Id c) :.: f)) :% a)
     (((g :.: Id c) :.: f) :% a)
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 :: 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 _ m _) Cod
  (EndoFunctorCompose (Dom m))
  (EndoFunctorCompose (Dom m) :% (m, m))
  m
mult) = ((g :.: m) :.: f)
-> (forall a. Obj d a -> Component (Id d) ((g :.: m) :.: f) a)
-> (forall a.
    Obj d a
    -> Component
         (((g :.: m) :.: f) :.: ((g :.: m) :.: f)) ((g :.: m) :.: f) a)
-> Monad ((g :.: m) :.: f)
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 g -> m -> g :.: m
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: m
m (g :.: m) -> f -> (g :.: m) :.: f
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: f
f)
  ((g -> f -> Wrap g f
forall f h. f -> h -> Wrap f h
Wrap g
g f
f Wrap g f
-> Dom (Wrap g f) (Id c) m
-> Cod (Wrap g f) (Wrap g f :% Id c) (Wrap g f :% m)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Wrap g f) (Id c) m
Cod
  (EndoFunctorCompose (Dom m)) (Unit (EndoFunctorCompose (Dom m))) m
ret Nat d d ((g :.: Id c) :.: f) ((g :.: m) :.: f)
-> Nat d d (Id d) ((g :.: Id c) :.: f)
-> Nat d d (Id d) ((g :.: m) :.: f)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. g -> Nat (Dom g) (Cod g) g (g :.: Id (Dom g))
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv g
g Nat c d g (g :.: Id c)
-> Nat d c f f -> Nat d d (g :.: f) ((g :.: Id c) :.: 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` f -> Nat (Dom f) (Cod f) f f
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId f
f Nat d d (g :.: f) ((g :.: Id c) :.: f)
-> Nat d d (Id d) (g :.: f) -> Nat d d (Id d) ((g :.: Id c) :.: f)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. Adjunction c d f g -> Nat d d (Id d) (g :.: f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj) Nat d d (Id d) ((g :.: m) :.: f)
-> Obj d a -> d (Id d :% a) (((g :.: m) :.: f) :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  ((g -> f -> Wrap g f
forall f h. f -> h -> Wrap f h
Wrap g
g f
f Wrap g f
-> Dom (Wrap g f) ((m :.: (f :.: g)) :.: m) m
-> Cod
     (Wrap g f) (Wrap g f :% ((m :.: (f :.: g)) :.: m)) (Wrap g f :% m)
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
Nat c c (m :.: m) m
mult Nat c c (m :.: m) m
-> Nat c c ((m :.: (f :.: g)) :.: m) (m :.: m)
-> Nat c c ((m :.: (f :.: g)) :.: m) m
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. m -> Nat (Dom m) (Cod m) (m :.: Id (Dom m)) m
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp m
m Nat c c (m :.: Id c) m
-> Nat c c m m -> Nat c c ((m :.: Id c) :.: m) (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` m -> Nat (Dom m) (Cod m) m m
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId m
m Nat c c ((m :.: Id c) :.: m) (m :.: m)
-> Nat c c ((m :.: (f :.: g)) :.: m) ((m :.: Id c) :.: m)
-> Nat c c ((m :.: (f :.: g)) :.: m) (m :.: m)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. m -> m -> Wrap m m
forall f h. f -> h -> Wrap f h
Wrap m
m m
m Wrap m m
-> Dom (Wrap m m) (f :.: g) (Id c)
-> Cod (Wrap m m) (Wrap m m :% (f :.: g)) (Wrap m m :% Id c)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Adjunction c d f g -> Nat c c (f :.: g) (Id c)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj)) Nat d d ((g :.: ((m :.: (f :.: g)) :.: m)) :.: f) ((g :.: m) :.: f)
-> Obj d a
-> d (((g :.: ((m :.: (f :.: g)) :.: m)) :.: f) :% a)
     (((g :.: m) :.: f) :% a)
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 :: 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 c)
  ((f :.: Id d) :.: g)
  (Unit (EndoFunctorCompose c))
extr Cod
  (EndoFunctorCompose c)
  ((f :.: Id d) :.: g)
  (EndoFunctorCompose c :% ((f :.: Id d) :.: g, (f :.: Id d) :.: g))
dupl = Adjunction c d f g
-> Comonad (Id d) -> Comonad ((f :.: Id d) :.: g)
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 Comonad (Id d)
forall (k :: * -> * -> *). Category k => Comonad (Id k)
idComonad
  in (f :.: g)
-> (forall a. Obj c a -> Component (f :.: g) (Id c) a)
-> (forall a.
    Obj c a -> Component (f :.: g) ((f :.: g) :.: (f :.: g)) a)
-> Comonad (f :.: g)
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 f -> g -> f :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g) (Cod
  (EndoFunctorCompose c)
  ((f :.: Id d) :.: g)
  (Unit (EndoFunctorCompose c))
Nat c c ((f :.: Id d) :.: g) (Id c)
extr Nat c c ((f :.: Id d) :.: g) (Id c)
-> Obj c a -> c (((f :.: Id d) :.: g) :% a) (Id c :% a)
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 c)
  ((f :.: Id d) :.: g)
  (EndoFunctorCompose c :% ((f :.: Id d) :.: g, (f :.: Id d) :.: g))
Nat
  c
  c
  ((f :.: Id d) :.: g)
  (((f :.: Id d) :.: g) :.: ((f :.: Id d) :.: g))
dupl Nat
  c
  c
  ((f :.: Id d) :.: g)
  (((f :.: Id d) :.: g) :.: ((f :.: Id d) :.: g))
-> Obj c a
-> c (((f :.: Id d) :.: g) :% a)
     ((((f :.: Id d) :.: g) :.: ((f :.: Id d) :.: g)) :% a)
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 :: 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 _ _) Cod
  (EndoFunctorCompose (Dom w))
  w
  (EndoFunctorCompose (Dom w) :% (w, w))
dupl) = ((f :.: w) :.: g)
-> (forall a. Obj c a -> Component ((f :.: w) :.: g) (Id c) a)
-> (forall a.
    Obj c a
    -> Component
         ((f :.: w) :.: g) (((f :.: w) :.: g) :.: ((f :.: w) :.: g)) a)
-> Comonad ((f :.: w) :.: g)
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 f -> w -> f :.: w
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: w
w (f :.: w) -> g -> (f :.: w) :.: g
forall g h.
(Functor g, Functor h, Cod h ~ Dom g) =>
g -> h -> g :.: h
:.: g
g)
  ((Adjunction c d f g -> Nat c c (f :.: g) (Id c)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat c c (f :.: g) (Id c)
adjunctionCounit Adjunction c d f g
adj Nat c c (f :.: g) (Id c)
-> Nat c c ((f :.: w) :.: g) (f :.: g)
-> Nat c c ((f :.: w) :.: g) (Id c)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) (f :.: Id (Dom f)) f
idPrecomp f
f Nat d c (f :.: Id d) f
-> Nat c d g g -> Nat c c ((f :.: Id d) :.: g) (f :.: 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` g -> Nat (Dom g) (Cod g) g g
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId g
g Nat c c ((f :.: Id d) :.: g) (f :.: g)
-> Nat c c ((f :.: w) :.: g) ((f :.: Id d) :.: g)
-> Nat c c ((f :.: w) :.: g) (f :.: g)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. f -> g -> Wrap f g
forall f h. f -> h -> Wrap f h
Wrap f
f g
g Wrap f g
-> Dom (Wrap f g) w (Id d)
-> Cod (Wrap f g) (Wrap f g :% w) (Wrap f g :% Id d)
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Dom (Wrap f g) w (Id d)
Cod
  (EndoFunctorCompose (Dom w)) w (Unit (EndoFunctorCompose (Dom w)))
extr) Nat c c ((f :.: w) :.: g) (Id c)
-> Obj c a -> c (((f :.: w) :.: g) :% a) (Id c :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)
  ((f -> g -> Wrap f g
forall f h. f -> h -> Wrap f h
Wrap f
f g
g Wrap f g
-> Dom (Wrap f g) w ((w :.: (g :.: f)) :.: w)
-> Cod
     (Wrap f g) (Wrap f g :% w) (Wrap f g :% ((w :.: (g :.: f)) :.: w))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% (w -> w -> Wrap w w
forall f h. f -> h -> Wrap f h
Wrap w
w w
w Wrap w w
-> Dom (Wrap w w) (Id d) (g :.: f)
-> Cod (Wrap w w) (Wrap w w :% Id d) (Wrap w w :% (g :.: f))
forall ftag a b.
Functor ftag =>
ftag -> Dom ftag a b -> Cod ftag (ftag :% a) (ftag :% b)
% Adjunction c d f g -> Nat d d (Id d) (g :.: f)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g.
Adjunction c d f g -> Nat d d (Id d) (g :.: f)
adjunctionUnit Adjunction c d f g
adj Nat d d ((w :.: Id d) :.: w) ((w :.: (g :.: f)) :.: w)
-> Nat d d w ((w :.: Id d) :.: w)
-> Nat d d w ((w :.: (g :.: f)) :.: w)
forall k (k :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category k =>
k b c -> k a b -> k a c
. w -> Nat (Dom w) (Cod w) w (w :.: Id (Dom w))
forall f.
Functor f =>
f -> Nat (Dom f) (Cod f) f (f :.: Id (Dom f))
idPrecompInv w
w Nat d d w (w :.: Id d)
-> Nat d d w w -> Nat d d (w :.: w) ((w :.: Id d) :.: 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` w -> Nat (Dom w) (Cod w) w w
forall f. Functor f => f -> Nat (Dom f) (Cod f) f f
natId w
w Nat d d (w :.: w) ((w :.: Id d) :.: w)
-> Nat d d w (w :.: w) -> Nat d d w ((w :.: Id d) :.: 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))
Nat d d w (w :.: w)
dupl)) Nat c c ((f :.: w) :.: g) ((f :.: ((w :.: (g :.: f)) :.: w)) :.: g)
-> Obj c a
-> c (((f :.: w) :.: g) :% a)
     (((f :.: ((w :.: (g :.: f)) :.: w)) :.: g) :% a)
forall (c :: * -> * -> *) (d :: * -> * -> *) f g a b.
(Category c, Category d) =>
Nat c d f g -> c a b -> d (f :% a) (g :% b)
!)