open import Level

open import Data.Product using (_,_)
open import Categories.Category
open import Categories.Functor hiding (id)
open import Categories.Functor.Coalgebra
open import Monad.Instance.Delay
open import Categories.Monad.Strong
open import Categories.NaturalTransformation hiding (id)
open import Categories.Object.Terminal
open import Categories.Category.Distributive

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

-- The Delay Monad is Strong
module Monad.Instance.Delay.Strong {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (D : DelayM (Distributive.cocartesian distributive)) where
  open Category C
  open import Category.Distributive.Helper distributive
  open Bundles
  open HomReasoning
  open Equiv
  open MP C
  open MR C
  open M C
  open DelayM D
  open D-Kleisli
  open D-Monad
  open Coit
  module τ-mod where
    abstract
      τ : ∀ {X Y} → X × D₀ Y ⇒ D₀ (X × Y)
      τ {X} {Y} = coit (distributeˡ⁻¹ ∘ (id ×₁ out))
      
      τ-commutes : ∀ {X Y} → out ∘ τ {X} {Y} ≈ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
      τ-commutes = coit-commutes (distributeˡ⁻¹ ∘ (id ×₁ out))

      τ-out⁻¹ : ∀ {X Y} → τ {X} {Y} ∘ (id ×₁ out⁻¹) ≈ out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹
      τ-out⁻¹ = begin 
        τ ∘ (id ×₁ out⁻¹)                                                 ≈⟨ introˡ out⁻¹∘out ⟩ 
        (out⁻¹ ∘ out) ∘ τ ∘ (id ×₁ out⁻¹)                                 ≈⟨ pullʳ (pullˡ τ-commutes) ⟩
        out⁻¹ ∘ ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
        out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∘ (id ×₁ out⁻¹)   ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (×₁∘×₁ ○ (×₁-cong₂ identity² out∘out⁻¹) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ×₁-η)))) ⟩
        out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹                                 ∎

      τ-now : ∀ {X Y} → τ {X} {Y} ∘ (id ×₁ now) ≈ now
      τ-now = begin 
        τ ∘ (id ×₁ now)                                  ≈⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ (×₁-cong₂ identity² refl)) ⟩ 
        τ ∘ (id ×₁ out⁻¹) ∘ (id ×₁ i₁)                   ≈⟨ pullˡ τ-out⁻¹ ⟩
        (out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₁) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₁) ⟩
        out⁻¹ ∘ (id +₁ τ) ∘ i₁                           ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
        out⁻¹ ∘ i₁ ∘ id                                  ≈⟨ refl⟩∘⟨ identityʳ ⟩
        now                                              ∎
      
      τ-later : ∀ {X} {Y} → τ {X} {Y} ∘ (id ×₁ later) ≈ later ∘ τ
      τ-later = begin 
        τ ∘ (id ×₁ later)                                ≈⟨ refl⟩∘⟨ (sym (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ⟩ 
        τ ∘ (id ×₁ out⁻¹) ∘ (id ×₁ i₂)                   ≈⟨ pullˡ τ-out⁻¹ ⟩ 
        (out⁻¹ ∘ (id +₁ τ) ∘ distributeˡ⁻¹) ∘ (id ×₁ i₂) ≈⟨ pullʳ (pullʳ distributeˡ⁻¹-i₂) ⟩ 
        out⁻¹ ∘ (id +₁ τ) ∘ i₂                           ≈⟨ refl⟩∘⟨ +₁∘i₂ ⟩ 
        out⁻¹ ∘ i₂ ∘ τ                                   ≈⟨ sym-assoc ⟩ 
        later ∘ τ                                        ∎

      τ-identityˡ : ∀ {X} {Y} → D₁ (π₂ {X} {Y}) ∘ τ ≈ π₂
      τ-identityˡ {X} {Y} = by-coinduction {f = D₁ (π₂ {X} {Y}) ∘ τ} {g = π₂} ((π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) coind₁ coind₂
        where
        coind₁ : out ∘ D₁ (π₂ {X} {Y}) ∘ τ ≈ (id +₁ extend (now ∘ π₂) ∘ τ) ∘ (π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
        coind₁ = begin 
          out ∘ D₁ π₂ ∘ τ                                              ≈⟨ extendʳ (D₁-commutes π₂) ⟩ 
          (π₂ +₁ D₁ π₂) ∘ out ∘ τ                                      ≈⟨ refl⟩∘⟨ τ-commutes ⟩ 
          (π₂ +₁ D₁ π₂) ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)      ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl) ⟩ 
          (π₂ +₁ D₁ π₂ ∘ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)              ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
          (id +₁ D₁ π₂ ∘ τ) ∘ (π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
        coind₂ : out ∘ (π₂ {X} {D₀ Y}) ≈ (id +₁ π₂) ∘ (π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
        coind₂ = begin 
          out ∘ π₂                                              ≈˘⟨ π₂∘×₁ ⟩ 
          π₂ ∘ (id ×₁ out)                                      ≈˘⟨ pullˡ distributeˡ⁻¹-π₂ ⟩
          (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)              ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
          (id ∘ π₂ +₁ π₂ ∘ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)    ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
          (id +₁ π₂) ∘ (π₂ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎

      τ-unique : ∀ {X Y} → (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (id +₁ t) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) → τ ≈ t
      τ-unique {X} {Y} t t-commutes = coit-unique (distributeˡ⁻¹ ∘ (id ×₁ out)) t t-commutes

      τ-natural : ∀ {X Y} {A} {B} (f : X ⇒ A) (g : Y ⇒ B) → τ ∘ (f ×₁ D₁ g) ≈ D₁ (f ×₁ g) ∘ τ
      τ-natural f g = by-coinduction (((f ×₁ g +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)) coind₁ coind₂
        where
        coind₁ : out ∘ τ ∘ (f ×₁ extend (now ∘ g)) ≈ (id +₁ (τ ∘ (f ×₁ extend (now ∘ g)))) ∘ ((f ×₁ g +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)
        coind₁ = begin 
          out ∘ τ ∘ (f ×₁ extend (now ∘ g))                                                      ≈⟨ pullˡ τ-commutes ⟩ 
          ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (f ×₁ extend (now ∘ g))                    ≈⟨ pullʳ (pullʳ ×₁∘×₁) ⟩ 
          (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ∘ f ×₁ out ∘ extend (now ∘ g))                         ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (×₁-cong₂ identityˡ (extend-commutes (now ∘ g)))) ⟩ 
          (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (f ×₁ [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out)     ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (×₁-cong₂ refl (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl))) ⟩ 
          (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (f ×₁ [ i₁ ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out)            ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (×₁-cong₂ (sym identityʳ) refl)) ⟩ 
          (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (f ∘ id ×₁ (g +₁ extend (now ∘ g)) ∘ out)                  ≈⟨ sym (pullʳ (pullʳ ×₁∘×₁)) ⟩ 
          ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (f ×₁ (g +₁ extend (now ∘ g)))) ∘ (id ×₁ out)             ≈⟨ (refl⟩∘⟨ (sym (distributeˡ⁻¹-natural f g (extend (now ∘ g))))) ⟩∘⟨refl ⟩ 
          ((id +₁ τ) ∘ ((f ×₁ g) +₁ (f ×₁ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)      ≈⟨ (pullˡ +₁∘+₁) ⟩∘⟨refl ⟩ 
          ((id ∘ (f ×₁ g) +₁ τ ∘ (f ×₁ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)         ≈⟨ sym (((+₁-cong₂ refl identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
          ((id ∘ (f ×₁ g) +₁ (τ ∘ (f ×₁ extend (now ∘ g))) ∘ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)  ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩ 
          (id +₁ (τ ∘ (f ×₁ extend (now ∘ g)))) ∘ ((f ×₁ g +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out) ∎
        coind₂ : out ∘ extend (now ∘ (f ×₁ g)) ∘ τ ≈ (id +₁ (extend (now ∘ (f ×₁ g)) ∘ τ)) ∘ (((f ×₁ g) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)
        coind₂ = begin 
          out ∘ extend (now ∘ (f ×₁ g)) ∘ τ                                                         ≈⟨ pullˡ (extend-commutes (now ∘ (f ×₁ g))) ⟩ 
          ([ out ∘ now ∘ (f ×₁ g) , i₂ ∘ extend (now ∘ (f ×₁ g)) ] ∘ out) ∘ τ                       ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
          ([ i₁ ∘ (f ×₁ g) , i₂ ∘ extend (now ∘ (f ×₁ g)) ] ∘ out) ∘ τ                              ≈⟨ pullʳ τ-commutes ⟩
          ((f ×₁ g) +₁ (extend (now ∘ (f ×₁ g)))) ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)         ≈⟨ sym-assoc ○ sym-assoc ⟩
          ((((f ×₁ g) +₁ (extend (now ∘ (f ×₁ g)))) ∘ (id +₁ τ)) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)     ≈⟨ (+₁∘+₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩
          ((((f ×₁ g) ∘ id) +₁ (extend (now ∘ (f ×₁ g)) ∘ τ)) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)        ≈⟨ sym (((+₁-cong₂ id-comm-sym identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
          (((id ∘ (f ×₁ g)) +₁ ((extend (now ∘ (f ×₁ g)) ∘ τ) ∘ id)) ∘ distributeˡ⁻¹) ∘ (id ×₁ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
          (id +₁ (extend (now ∘ (f ×₁ g)) ∘ τ)) ∘ (((f ×₁ g) +₁ id) ∘ distributeˡ⁻¹) ∘ (id ×₁ out)  ∎
  open τ-mod

  module D-Strong where
    strength : Strength monoidal monad
    Strength.strengthen strength = ntHelper (record { η = λ (X , Y) → τ {X} {Y}; commute = λ (f , g) → τ-natural f g })

    Strength.identityˡ strength {X} = τ-identityˡ {Terminal.⊤ terminal} {X}

    Strength.η-comm strength {X} {Y} = τ-now {X} {Y}

    Strength.μ-η-comm strength {X} {Y} = by-coinduction ([ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) coind₁ coind₂
      where
      -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
      id*∘Dτ : extend id ∘ extend (now ∘ τ) ≈ extend τ
      id*∘Dτ = begin 
        extend id ∘ extend (now ∘ τ) ≈⟨ DK.sym-assoc ⟩ 
        extend (extend id ∘ now ∘ τ) ≈⟨ extend-≈ (pullˡ DK.identityʳ) ⟩
        extend (id ∘ τ)              ≈⟨ extend-≈ identityˡ ⟩ 
        extend τ                    ∎
      coind₁ : out ∘ extend id ∘ extend (now ∘ τ) ∘ τ {X} {D₀ Y} ≈ (id +₁ (extend id ∘ extend (now ∘ τ) ∘ τ)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
      coind₁ = begin 
        out ∘ extend id ∘ extend (now ∘ τ) ∘ τ                                                                                                ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
        out ∘ extend τ ∘ τ                                                                                                                    ≈⟨ square ⟩
        [ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)                                                                 ≈⟨ assoc²εβ ○ ∘-resp-≈ˡ tri ○ assoc²βε ⟩
        (id +₁ (extend τ ∘ τ)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)                     ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
        (id +₁ (extend id ∘ extend (now ∘ τ) ∘ τ)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
        where
        tri : [ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ≈ (id +₁ extend τ ∘ τ) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹
        tri = begin 
          [ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹                                                                  ≈⟨ pullˡ []∘+₁ ⟩ 
          [ (out ∘ τ) ∘ id , (i₂ ∘ extend τ) ∘ τ ] ∘ distributeˡ⁻¹                                                                 ≈⟨ ([]-cong₂ (identityʳ ○ τ-commutes) assoc) ⟩∘⟨refl ⟩ 
          [ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ τ ] ∘ distributeˡ⁻¹                                          ≈˘⟨ ([]-cong₂ ((+₁-cong₂ refl DK.identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ 
          [ (id +₁ extend τ ∘ now) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ τ ] ∘ distributeˡ⁻¹                             ≈˘⟨ ([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now))) ⟩∘⟨refl) refl) ⟩∘⟨refl ⟩ 
          [ (id ∘ id +₁ (extend τ ∘ τ) ∘ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ extend τ ∘ τ ] ∘ distributeˡ⁻¹          ≈˘⟨ ([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl ⟩ 
          [ (id +₁ extend τ ∘ τ) ∘ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , (id +₁ extend τ ∘ τ) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈˘⟨ pullˡ ∘[] ⟩ 
          (id +₁ extend τ ∘ τ) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹                        ∎
        square : out ∘ extend τ ∘ τ ≈ [ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
        square = begin 
          out ∘ extend τ ∘ τ                                                   ≈⟨ pullˡ (extend-commutes τ) ⟩ 
          ([ out ∘ τ , i₂ ∘ extend τ ] ∘ out) ∘ τ                              ≈⟨ pullʳ τ-commutes ⟩ 
          [ out ∘ τ , i₂ ∘ extend τ ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
      coind₂ : out ∘ τ {X} {Y} ∘ (id ×₁ extend id) ≈ (id +₁ τ ∘ (id ×₁ extend id)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
      coind₂ = begin 
        out ∘ τ ∘ (id ×₁ extend id)                                                                                              ≈⟨ pullˡ τ-commutes ⟩ 
        ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ extend id)                                                            ≈⟨ pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out ∘ extend id)                                                                      ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ refl (extend-commutes id) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ [ out ∘ id , i₂ ∘ extend id ] ∘ out)                                                  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ [ out , i₂ ∘ extend id ] ∘ out)                                                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (×₁∘×₁ ○ ×₁-cong₂ identity² refl) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ [ out , i₂ ∘ extend id ]) ∘ (id ×₁ out)                                               ≈⟨ sym-assoc ○ pullˡ (assoc ○ Iso⇒Epi (IsIso.iso isIsoˡ) _ _ (assoc²βε ○ epi-helper ○ assoc²εβ)) ○ assoc²βε ⟩
        (id +₁ τ ∘ (id ×₁ extend id)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
        where
          epi-helper : (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ [ out , i₂ ∘ extend id ]) ∘ [ (id ×₁ i₁) , (id ×₁ i₂) ] ≈ (id +₁ τ ∘ (id ×₁ extend id)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
          epi-helper = begin 
            (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ [ out , i₂ ∘ extend id ]) ∘ [ (id ×₁ i₁) , (id ×₁ i₂) ]                               ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (∘[] ○ []-cong₂ (×₁∘×₁ ○ ×₁-cong₂ identity² inject₁) (×₁∘×₁ ○ ×₁-cong₂ identity² inject₂)) ⟩ 
            (id +₁ τ) ∘ distributeˡ⁻¹ ∘ [ id ×₁ out , id ×₁ i₂ ∘ extend id ]                                                         ≈⟨ ∘-resp-≈ʳ ∘[] ○ ∘[] ⟩
            [ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂ ∘ extend id) ]                         ≈˘⟨ []-cong₂ refl (pullʳ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² refl))) ⟩
            [ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ i₂)) ∘ (id ×₁ extend id) ]               ≈⟨ []-cong₂ refl ((refl⟩∘⟨ distributeˡ⁻¹-i₂) ⟩∘⟨refl) ⟩
            [ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , ((id +₁ τ) ∘ i₂) ∘ (id ×₁ extend id) ]                                       ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
            [ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ τ ∘ (id ×₁ extend id) ]                                                 ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym DK.identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
            [ (id +₁ τ ∘ (id ×₁ extend id ∘ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ τ ∘ (id ×₁ extend id) ]                       ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (×₁∘×₁ ○ ×₁-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
            [ (id +₁ τ ∘ (id ×₁ extend id) ∘ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ∘ τ ∘ (id ×₁ extend id) ]               ≈˘⟨ ∘[] ○ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂ ⟩
            (id +₁ τ ∘ (id ×₁ extend id)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ]                               ≈˘⟨ refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ)) ⟩
            (id +₁ τ ∘ (id ×₁ extend id)) ∘ [ (id +₁ (id ×₁ now)) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎

    Strength.strength-assoc strength {X} {Y} {Z} = by-coinduction ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) coind₁ coind₂
      where
      coind₁ : out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ {X × Y} {Z} ≈ (id +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
      coind₁ = begin 
        out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ                                                                                       ≈⟨ pullˡ (extend-commutes (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩ 
        ([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ                               ≈⟨ pullʳ τ-commutes ⟩ 
        [ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ 
        (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)                   ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ id-comm (sym identityʳ)) ⟩ 
        (id ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ) ∘ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)               ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
        (id +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)              ∎
      coind₂ : out ∘ τ {X} {Y × Z} ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (id +₁ τ ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)
      coind₂ = begin 
        out ∘ τ ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                                                          ≈⟨ pullˡ τ-commutes ⟩ 
        ((id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                        ≈⟨ pullʳ (pullˡ (pullʳ (×₁∘×₁ ○ ×₁-cong₂ identity² τ-commutes))) ○ ∘-resp-≈ʳ assoc ⟩ 
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² assoc)) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ (id +₁ τ) ∘ distributeˡ⁻¹) ∘ (id ×₁ (id ×₁ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩          ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ helper₁ ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ (id +₁ τ) ∘ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id ×₁ out)                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (×₁∘×₁ ○ ×₁-cong₂ identity² refl)) ⟩
        (id +₁ τ) ∘ distributeˡ⁻¹ ∘ (id ×₁ (id +₁ τ)) ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id ×₁ out)          ≈⟨ refl⟩∘⟨ extendʳ (sym (distributeˡ⁻¹-natural id id τ) ○ ∘-resp-≈ˡ (+₁-cong₂ (⟨⟩-unique id-comm id-comm) refl)) ⟩ 
        (id +₁ τ) ∘ (id +₁ (id ×₁ τ)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id ×₁ out)          ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
        (id +₁ τ ∘ (id ×₁ τ)) ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id ×₁ out)                  ≈⟨ refl⟩∘⟨ (assoc²εβ ○ ∘-resp-≈ˡ helper₃ ○ assoc) ⟩ 
        (id +₁ τ ∘ (id ×₁ τ)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ∘ (id ×₁ out)      ≈˘⟨ extendʳ (+₁∘+₁ ○ +₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩ 
        (id +₁ τ ∘ (id ×₁ τ) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ×₁ out) ∎
        where
        helper₁ : (id ×₁ (id ×₁ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id {X × Y} ×₁ out {Z})
        helper₁ = begin 
          (id ×₁ (id ×₁ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩     ≈⟨ ×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) ⟩ 
          ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩                     ≈˘⟨ ⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ project₁ ○ ∘-resp-≈ʳ identityˡ) (⟨⟩∘ ○ ⟨⟩-cong₂ (pullʳ π₁∘×₁ ○ ∘-resp-≈ʳ identityˡ) π₂∘×₁) ⟩ 
          ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (id {X × Y} ×₁ out {Z}) ∎
        helper₃ : distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹
        helper₃ = Iso⇒Mono (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) (begin 
          distributeˡ ∘ distributeˡ⁻¹ ∘ (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩             ≈⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩ 
          (id ×₁ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                           ≈⟨ ×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ ⟩ 
          ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩                                                   ≈⟨ ⟨⟩-unique unique₁ unique₂ ⟩ 
          [ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹    ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ) (×₁∘⟨⟩ ○ ⟨⟩-congʳ identityˡ)) ⟩ 
          distributeˡ ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ∎)
          where
          unique₁ : π₁ ∘ [ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈ π₁ ∘ π₁
          unique₁ = begin 
            π₁ ∘ [ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ extendʳ (∘[] ○ []-cong₂ project₁ project₁ ○ sym ∘[]) ⟩ 
            π₁ ∘ [ π₁ , π₁ ] ∘ distributeˡ⁻¹                                                                   ≈⟨ refl⟩∘⟨ distributeˡ⁻¹-π₁ ⟩ 
            π₁ ∘ π₁                                                                                            ∎
          unique₂ : π₂ ∘ [ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩
          unique₂ = begin 
            π₂ ∘ [ ⟨ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ pullˡ (∘[] ○ []-cong₂ project₂ project₂) ⟩ 
            (⟨ π₂ ∘ π₁ , π₂ ⟩ +₁ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ distributeˡ⁻¹                                             ≈˘⟨ (+₁-cong₂ (⟨⟩-congˡ identityˡ) (⟨⟩-congˡ identityˡ)) ⟩∘⟨refl ⟩ 
            ((π₂ ×₁ id) +₁ (π₂ ×₁ id)) ∘ distributeˡ⁻¹                                                         ≈⟨ distributeˡ⁻¹-natural π₂ id id ⟩ 
            distributeˡ⁻¹ ∘ (π₂ ×₁ (id +₁ id))                                                                 ≈⟨ refl⟩∘⟨ (⟨⟩-congˡ (elimˡ ([]-unique id-comm-sym id-comm-sym))) ⟩ 
            distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩                                                                   ∎

    strongMonad : StrongMonad monoidal
    strongMonad = record { M = monad ; strength = strength }

    module strength = Strength strength