{-# LANGUAGE
TypeOperators
, TypeFamilies
, GADTs
, Rank2Types
, ViewPatterns
, TypeSynonymInstances
, FlexibleInstances
, UndecidableInstances
, NoImplicitPrelude
#-}
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
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))
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
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
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
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)
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
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))
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)
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)
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)
!)
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)
!)
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)
!)
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)
!)