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 .from 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 .from 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 _ _ $ ext Ξ» _ β†’ refl
    is .snd .linv _ = Left-strength-path  _ _ $ ext Ξ» _ β†’ refl

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.β†©οΈŽ