bsc-leon-vatthauer/src/Monad/Morphism.lagda.md

<!--
```agda
open import Level
open import Categories.Category.Core
open import Categories.Category.Monoidal
open import Categories.Monad
open import Categories.Monad.Morphism using (Monad⇒-id)
open import Categories.Monad.Strong
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Data.Product using (_,_; Σ; Σ-syntax)
```
-->

```agda
module Monad.Morphism {o ℓ e} (C : Category o ℓ e) where
  open Category C
```

# Monad morphisms
This file contains the definition of morphisms between (strong) monads on the same category

## Morphisms between monads
A morphism between monads is a natural transformation that preserves η and μ, 
this notion is already formalized in the categories library, 
but since we are only interested in monads on the same category we rename their definitions.

```agda
  Monad⇒ = Monad⇒-id
```

## Morphisms between strong monads
A morphism between strong monads is a morphism between the underlying monads that also preverses strength.

```agda
  record IsStrongMonad⇒ {monoidal : Monoidal C} (M N : StrongMonad monoidal) (α : NaturalTransformation (StrongMonad.M.F M) (StrongMonad.M.F N)) : Set (o ⊔ ℓ ⊔ e) where
    private
      module M = StrongMonad M
      module N = StrongMonad N
      module α = NaturalTransformation α
    open Monoidal monoidal
    
    field
      η-comm : ∀ {U} → α.η U ∘ M.M.η.η U ≈ N.M.η.η U
      μ-comm : ∀ {U} → α.η U ∘ (M.M.μ.η U) ≈ N.M.μ.η U ∘ α.η (N.M.F.₀ U) ∘ M.M.F.₁ (α.η U)
      τ-comm : ∀ {U V} → α.η (U ⊗₀ V) ∘ M.strengthen.η (U , V) ≈ N.strengthen.η (U , V) ∘ (id ⊗₁ α.η V)

  record StrongMonad⇒ {monoidal : Monoidal C} {M N : StrongMonad monoidal} : Set (o ⊔ ℓ ⊔ e) where
    field
      α : NaturalTransformation (StrongMonad.M.F M) (StrongMonad.M.F N)
      isStrongMonad⇒ : IsStrongMonad⇒ M N α

    open IsStrongMonad⇒ isStrongMonad⇒ public
```