open import 1Lab.Reflection.Record

open import Cat.Monoidal.Instances.Cartesian
open import Cat.Functor.Naturality
open import Cat.Instances.Product
open import Cat.Monoidal.Braided
open import Cat.Monoidal.Reverse
open import Cat.Functor.Compose
open import Cat.Monoidal.Base
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open _=>_

module Cat.Monoidal.Strength where


# Strong functorsð

module _
{o â} {C : Precategory o â}
(Cáµ : Monoidal-category C)
(F : Functor C C)
where
open Cat.Reasoning C
open Monoidal-category Cáµ
open Functor F
private module F = Cat.Functor.Reasoning F


A left strength for a functor on a monoidal category is a natural transformation

interacting nicely with the left unitor and associator.

  record Left-strength : Type (o â â) where
field
left-strength : -â- Fâ (Id FÃ F) => F Fâ -â-

module Ï = _=>_ left-strength

Ï : â {A B} â Hom (A â Fâ B) (Fâ (A â B))
Ï = Ï.Î· _

field
left-strength-Î»â : â {A} â Fâ (Î»â {A}) â Ï â¡ Î»â
left-strength-Î±â : â {A B C}
â Fâ (Î±â A B C) â Ï â¡ Ï â (id ââ Ï) â Î±â A B (Fâ C)


Reversely1, a right strength is a natural transformation

interacting nicely with the right unitor and associator.

  record Right-strength : Type (o â â) where
field
right-strength : -â- Fâ (F FÃ Id) => F Fâ -â-

module Ï = _=>_ right-strength

Ï : â {A B} â Hom (Fâ A â B) (Fâ (A â B))
Ï = Ï.Î· _

field
right-strength-Ïâ : â {A} â Fâ (Ïâ {A}) â Ï â¡ Ïâ
right-strength-Î±â : â {A B C}
â Fâ (Î±â A B C) â Ï â¡ Ï â (Ï ââ id) â Î±â (Fâ A) B C

    right-strength-Î±â : â {A B C} â Ï â Î±â (Fâ A) B C â¡ Fâ (Î±â A B C) â Ï â (Ï ââ id)
right-strength-Î±â = sym $swizzle (sym (right-strength-Î±â â assoc _ _ _)) (Î±â .invr) (F.F-map-iso Î±â .invl)  A strength for is a pair of a left strength and a right strength inducing a single operation i.e.Â making the following diagram commute:  record Strength : Type (o â â) where field strength-left : Left-strength strength-right : Right-strength open Left-strength strength-left public open Right-strength strength-right public field strength-Î±â : â {A B C} â Fâ (Î±â A B C) â Ï â (Ï ââ id) â¡ Ï â (id ââ Ï) â Î±â A (Fâ B) C  A functor equipped with a strength is called a strong functor.  private unquoteDecl left-eqv = declare-record-iso left-eqv (quote Left-strength) Left-strength-path : â {a b} â a .Left-strength.left-strength â¡ b .Left-strength.left-strength â a â¡ b Left-strength-path p = Iso.injective left-eqv (Î£-prop-path (Î» _ â hlevel 1) p) private unquoteDecl right-eqv = declare-record-iso right-eqv (quote Right-strength) Right-strength-path : â {a b} â a .Right-strength.right-strength â¡ b .Right-strength.right-strength â a â¡ b Right-strength-path p = Iso.injective right-eqv (Î£-prop-path (Î» _ â hlevel 1) p)  ## Symmetryð  module _ (Cáµ : Braided-monoidal Cáµ) where open Braided Cáµ Cáµ open is-iso  In a symmetric monoidal category (or even just a braided monoidal category, if one is careful about directions), there is an equivalence between the notions of left and right strength: we can obtain one from the other by âconjugatingâ with the braiding, as illustrated by this diagram. Therefore, the literature usually speaks of âstrengthâ in a symmetric monoidal category to mean either a left or a right strength, but note that this is not quite the same as a Strength as defined above, which has left and right strengths not necessarily related by the braiding. If they are, we will say that the strength is symmetric; such a strength contains exactly the information of a left (or right) strength.  is-symmetric-strength : Strength â Type (o â â) is-symmetric-strength s = â {A B} â Ï {A} {B} â Î²â â¡ Fâ Î²â â Ï where open Strength s  The construction of the equivalence between left and right strengths is extremely tedious, so we leave the details to the curious reader.  leftâright : Iso Left-strength Right-strength   leftâright .fst l = r where open Left-strength l open Right-strength r : Right-strength r .right-strength .Î· _ = Fâ Î²â â Ï â Î²â r .right-strength .is-natural _ _ (f , g) = (Fâ Î²â â Ï â Î²â) â (Fâ f ââ g) â¡âš pullr (pullr (Î²â.is-natural _ _ _)) â©â¡ Fâ Î²â â Ï â (g ââ Fâ f) â Î²â â¡âš reflâ©ââš extendl (Ï.is-natural _ _ _) â©â¡ Fâ Î²â â Fâ (g ââ f) â Ï â Î²â â¡âš F.extendl (Î²â.is-natural _ _ _) â©â¡ Fâ (f ââ g) â Fâ Î²â â Ï â Î²â â r .right-strength-Ïâ = Fâ Ïâ â Fâ Î²â â Ï â Î²â â¡âš F.pulll Ïâ-Î²â â©â¡ Fâ Î»â â Ï â Î²â â¡âš pulll left-strength-Î»â â©â¡ Î»â â Î²â â¡âš Î»â-Î²â â©â¡ Ïâ â r .right-strength-Î±â = Fâ (Î±â _ _ _) â Fâ Î²â â Ï â Î²â â¡âš reflâ©ââš reflâ©ââš pushl3 (sym (lswizzle (Ï.is-natural _ _ _) (F.annihilate (â.annihilate (Î²â .invl))))) â©â¡ Fâ (Î±â _ _ _) â Fâ Î²â â Fâ (Î²â ââ id) â Ï â (Î²â ââ â Fâ id â) â Î²â â¡âš ap! F-id â©â¡ Fâ (Î±â _ _ _) â Fâ Î²â â Fâ (Î²â ââ id) â Ï â (Î²â ââ id) â Î²â â¡âš F.extendl3 (sym Î²â-idâÎ²â-Î±â) â©â¡ Fâ Î²â â Fâ (id ââ Î²â) â Fâ (Î±â _ _ _) â Ï â (Î²â ââ id) â Î²â â¡âš reflâ©ââš reflâ©ââš pulll left-strength-Î±â â©â¡ Fâ Î²â â Fâ (id ââ Î²â) â (Ï â (id ââ Ï) â Î±â _ _ _) â (Î²â ââ id) â Î²â â¡âš reflâ©ââš reflâ©ââš pullr (pullr refl) â©â¡ Fâ Î²â â Fâ (id ââ Î²â) â Ï â (id ââ Ï) â Î±â _ _ _ â (Î²â ââ id) â Î²â â¡âš reflâ©ââš pushr (pushr (reflâ©ââš sym Î²â-Î²ââid-Î±â)) â©â¡ Fâ Î²â â (Fâ (id ââ Î²â) â Ï â (id ââ Ï)) â Î²â â (Î²â ââ id) â Î±â _ _ _ â¡Ëâš reflâ©ââš pulll (â¶.shufflel (Ï.is-natural _ _ _)) â©â¡Ë Fâ Î²â â Ï â (id ââ (Fâ Î²â â Ï)) â Î²â â (Î²â ââ id) â Î±â _ _ _ â¡âš pushr (pushr (extendl (sym (Î²â.is-natural _ _ _)))) â©â¡ (Fâ Î²â â Ï â Î²â) â ((Fâ Î²â â Ï) ââ id) â (Î²â ââ id) â Î±â _ _ _ â¡âš reflâ©ââš â.pulll (sym (assoc _ _ _)) â©â¡ (Fâ Î²â â Ï â Î²â) â ((Fâ Î²â â Ï â Î²â) ââ id) â Î±â _ _ _ â leftâright .snd .inv r = l where open Right-strength r open Left-strength l : Left-strength l .left-strength .Î· _ = Fâ Î²â â Ï â Î²â l .left-strength .is-natural _ _ (f , g) = (Fâ Î²â â Ï â Î²â) â (f ââ Fâ g) â¡âš pullr (pullr (Î²â.is-natural _ _ _)) â©â¡ Fâ Î²â â Ï â (Fâ g ââ f) â Î²â â¡âš reflâ©ââš extendl (Ï.is-natural _ _ _) â©â¡ Fâ Î²â â Fâ (g ââ f) â Ï â Î²â â¡âš F.extendl (Î²â.is-natural _ _ _) â©â¡ Fâ (f ââ g) â Fâ Î²â â Ï â Î²â â l .left-strength-Î»â = Fâ Î»â â Fâ Î²â â Ï â Î²â â¡âš F.pulll Î»â-Î²â â©â¡ Fâ Ïâ â Ï â Î²â â¡âš pulll right-strength-Ïâ â©â¡ Ïâ â Î²â â¡âš Ïâ-Î²â â©â¡ Î»â â l .left-strength-Î±â = Fâ (Î±â _ _ _) â Fâ Î²â â Ï â Î²â â¡âš reflâ©ââš reflâ©ââš pushl3 (sym (lswizzle (Ï.is-natural _ _ _) (F.annihilate (â¶.annihilate (Î²â .invr))))) â©â¡ Fâ (Î±â _ _ _) â Fâ Î²â â Fâ (id ââ Î²â) â Ï â (â Fâ id â ââ Î²â) â Î²â â¡âš ap! F-id â©â¡ Fâ (Î±â _ _ _) â Fâ Î²â â Fâ (id ââ Î²â) â Ï â (id ââ Î²â) â Î²â â¡âš F.extendl3 ((reflâ©ââš Î²â.is-natural _ _ _) â sym Î²â-Î²ââid-Î±â) â©â¡ Fâ Î²â â Fâ (Î²â ââ id) â Fâ (Î±â _ _ _) â Ï â (id ââ Î²â) â Î²â â¡âš reflâ©ââš reflâ©ââš pulll right-strength-Î±â â©â¡ Fâ Î²â â Fâ (Î²â ââ id) â (Ï â (Ï ââ id) â Î±â _ _ _) â (id ââ Î²â) â Î²â â¡âš reflâ©ââš reflâ©ââš pullr (pullr refl) â©â¡ Fâ Î²â â Fâ (Î²â ââ id) â Ï â (Ï ââ id) â Î±â _ _ _ â (id ââ Î²â) â Î²â â¡âš reflâ©ââš pushr (pushr (reflâ©ââš ((reflâ©ââš sym (Î²â.is-natural _ _ _)) â sym Î²â-idâÎ²â-Î±â))) â©â¡ Fâ Î²â â (Fâ (Î²â ââ id) â Ï â (Ï ââ id)) â Î²â â (id ââ Î²â) â Î±â _ _ _ â¡Ëâš reflâ©ââš pulll (â.shufflel (Ï.is-natural _ _ _)) â©â¡Ë Fâ Î²â â Ï â ((Fâ Î²â â Ï) ââ id) â Î²â â (id ââ Î²â) â Î±â _ _ _ â¡âš pushr (pushr (extendl (sym (Î²â.is-natural _ _ _)))) â©â¡ (Fâ Î²â â Ï â Î²â) â (id ââ (Fâ Î²â â Ï)) â (id ââ Î²â) â Î±â _ _ _ â¡âš reflâ©ââš â¶.pulll (sym (assoc _ _ _)) â©â¡ (Fâ Î²â â Ï â Î²â) â (id ââ (Fâ Î²â â Ï â Î²â)) â Î±â _ _ _ â leftâright .snd .rinv r = Right-strength-path$ ext Î» (A , B) â
Fâ Î²â â (Fâ Î²â â Ï â Î²â) â Î²â â¡âš extendl (F.cancell (Î²â .invl)) â©â¡
Ï â Î²â â Î²â                   â¡âš elimr (Î²â .invl) â©â¡
Ï                             â
where open Right-strength r
leftâright .snd .linv l = Left-strength-path $ext Î» (A , B) â Fâ Î²â â (Fâ Î²â â Ï â Î²â) â Î²â â¡âš extendl (F.cancell (Î²â .invr)) â©â¡ Ï â Î²â â Î²â â¡âš elimr (Î²â .invr) â©â¡ Ï â where open Left-strength l  ## Dualityð As hinted to above, a right strength for on can equivalently be defined as a left strength on the reverse monoidal category It is entirely trivial to show that the two definitions are equivalent: module _ {o â} {C : Precategory o â} (M : Monoidal-category C) (F : Functor C C) where open is-iso   strength^rev : Left-strength (M ^rev) F â Right-strength M F strength^rev = IsoâEquiv is where is : Iso _ _ is .fst l = record { right-strength = NT (Î» _ â Ï) Î» _ _ _ â Ï.is-natural _ _ _ ; right-strength-Ïâ = left-strength-Î»â ; right-strength-Î±â = left-strength-Î±â } where open Left-strength l is .snd .inv r = record { left-strength = NT (Î» _ â Ï) Î» _ _ _ â Ï.is-natural _ _ _ ; left-strength-Î»â = right-strength-Ïâ ; left-strength-Î±â = right-strength-Î±â } where open Right-strength r is .snd .rinv _ = Right-strength-path _ _ trivial! is .snd .linv _ = Left-strength-path _ _ trivial!  ## Sets-endofunctors are strongð module _ {â} (F : Functor (Sets â) (Sets â)) where open Functor F open Left-strength  Every endofunctor on seen as a cartesian monoidal category, can be equipped with a canonical symmetric strength: the tensor product is the actual product of sets, so, given we can simply apply the functorial action of on the function yielding a function  Sets-strength : Left-strength Setsâ F Sets-strength .left-strength .Î· (A , B) (a , Fb) = Fâ (a ,_) Fb Sets-strength .left-strength .is-natural (A , B) (C , D) (ac , bd) = ext Î» a Fb â (sym (F-â _ _) â F-â _ _)$â Fb
Sets-strength .left-strength-Î»â =
ext Î» _ Fa â (sym (F-â _ _) â F-id) $â Fa Sets-strength .left-strength-Î±â = ext Î» a b Fc â (sym (F-â _ _) â F-â _ _)$â Fc


This is an instance of a more general fact: in a closed monoidal category (that is, one with an adjunction for example coming from a cartesian closed category), left strengths for endofunctors are equivalent to enrichments of F: that is, natural transformations

internalising the functorial action Then, what we have shown boils down to the fact that every endofunctor on is trivially

1. That is, on the other side of the reverse monoidal category duality.â©ïž