bsc-leon-vatthauer/src/Monad/Instance/K/Commutative.lagda.md

module Monad.Instance.K.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (MK : MIK.MonadK ambient) where
  open Ambient ambient
  open MIK ambient
  open MonadK MK
  open import Monad.Instance.K.Strong ambient MK
  open import Category.Construction.UniformIterationAlgebras ambient
  open import Algebra.UniformIterationAlgebra ambient
  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)

  open Equiv
  open HomReasoning
  open MR C
  -- open M C

K is a commutative monad

The proof is analogous to the ones for strength, this is the relevant diagram is:

  KCommutative : CommutativeMonad {C = C} {V = monoidal} symmetric KStrong
  KCommutative = record { commutes = commutes' }
    where
      open monadK using (μ)
      open StrongMonad KStrong using (strengthen)
      open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
      open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
      
      -- some helper definitions to make our life easier
      η = λ Z → FreeObject.η (freealgebras Z)
      _♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
      _# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f

      σ : ∀ ((X , Y) : Obj ×f Obj) → K.₀ X × Y ⇒ K.₀ (X × Y)
      σ _ = K.₁ swap ∘ (τ _) ∘ swap

      σ-preserve : ∀ {X Y Z : Obj} (h : Z ⇒ K.₀ Y + Z) → σ (Y , X) ∘ (h # ⁂ idC) ≈ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))#
      {-
      K.₁ swap ∘ τ ∘ swap ∘ (h # ⁂ idC)
      ≈ K.₁ swap ∘ τ ∘ (idC ⁂ h #) ∘ swap
      ≈ K.₁ swap ∘ ()# ∘ swap
      ≈ ((K.₁ swap +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap
      -}
      σ-preserve {Z} h = {!   !}
      commutes' : ∀ {X Y : Obj} → μ.η _ ∘ K.₁ (σ _) ∘ τ (K.₀ X , Y) ≈ μ.η _ ∘ K.₁ (τ _) ∘ σ _
      commutes' {X} {Y} = begin 
        μ.η _ ∘ K.₁ (σ _) ∘ τ _ ≈⟨ ♯-unique (stable _) (σ _) (μ.η (X × Y) ∘ K.₁ (σ _) ∘ τ _) comm₁ comm₂ ⟩ 
        (σ _) ♯ ≈⟨ sym (♯-unique (stable _) (σ _) (μ.η _ ∘ K.₁ (τ _) ∘ σ _) comm₃ comm₄) ⟩ 
        μ.η _ ∘ K.₁ (τ _) ∘ σ _ ∎
        where
          comm₁ : σ _ ≈ (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _)
          comm₁ = sym (begin 
            (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩ 
            μ.η _ ∘ K.₁ (σ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η _) ⟩
            μ.η _ ∘ η _ ∘ σ _ ≈⟨ cancelˡ monadK.identityʳ ⟩
            σ _ ∎)
          comm₂ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
          comm₂ {Z} h = begin 
            (μ.η _ ∘ K.₁ (σ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (♯-preserving (stable _) (η _) h)) ⟩ 
            μ.η _ ∘ K.₁ (σ _) ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras _ FreeObject.*) (η _ ∘ σ _))) ⟩
            μ.η _ ∘ ((K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
            ((μ.η _ +₁ idC) ∘ (K.₁ (σ _) +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
            ((μ.η _ ∘ K.₁ (σ _) +₁ idC ∘ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
            (((μ.η _ ∘ K.₁ (σ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (elimˡ identity²)) ⟩∘⟨refl) ⟩
            ((μ.η _ ∘ K.₁ (σ _) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
          comm₃ : σ _ ≈ (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _)
          comm₃ = sym (begin 
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (pullʳ (pullʳ swap∘⁂))) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (sym K.identity) ⟩∘⟨refl ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (η _ ⁂ K.₁ idC) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (strengthen.commute (η _ , idC)) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ (K.₁ (η _ ⁂ idC) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym K.homomorphism)) ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (pullˡ (pullˡ (sym K.homomorphism))) ⟩ 
            μ.η _ ∘ (K.₁ (τ _ ∘ swap ∘ (η _ ⁂ idC)) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (((K.F-resp-≈ (refl⟩∘⟨ swap∘⁂)) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
            μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ η _) ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ (K.F-resp-≈ (pullˡ (τ-η _))) ⟩∘⟨refl ⟩∘⟨refl ⟩ 
            μ.η _ ∘ (K.₁ (η _ ∘ swap) ∘ τ _) ∘ swap ≈⟨ refl⟩∘⟨ ((K.homomorphism ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
            μ.η _ ∘ ((K.₁ (η _) ∘ K.₁ swap) ∘ τ _) ∘ swap ≈⟨ pullˡ (pullˡ (cancelˡ monadK.identityˡ)) ⟩ 
            (K.₁ swap ∘ τ _) ∘ swap ≈⟨ assoc ⟩ 
            σ _ ∎)
          comm₄ : ∀ {Z : Obj} (h : Z ⇒ K.₀ Y + Z) → (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
          comm₄ {Z} h = begin 
            (μ.η _ ∘ K.₁ (τ _) ∘ σ _) ∘ (idC ⁂ h #) ≈⟨ {!   !} ⟩ 
            μ.η (X × Y) ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (h # ⁂ idC) ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ τ _ ∘ (h # ⁂ K.₁ idC) ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ K.₁ (h # ⁂ idC) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ (swap ∘ (h # ⁂ idC)) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ ((idC ⁂ h #) ∘ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ (K.₁ (idC ⁂ h #) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ (K.₁ (τ _ ∘ (idC ⁂ h #)) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ (K.₁ (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ K.₁ swap) ∘ τ _ ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ σ _ ≈⟨ {!   !} ⟩ 
            {!   !} ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            {!   !} ≈⟨ {!   !} ⟩
            μ.η (X × Y) ∘ K.₁ (τ _) ∘ K.₁ swap ∘ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ K.₁ swap ∘ ((τ _ ∘ swap +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ K.₁ (τ _) ∘ ((σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
            μ.η _ ∘ ((K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ {!   !} ⟩ 
            ((μ.η _ ∘ K.₁ (τ _) ∘ σ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
            where
              test : ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ swap ≈ ((τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
              test = sym (#-Uniformity (algebras _) (sym (begin 
                ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ swap ≈⟨ pullʳ (pullʳ (sym swap∘⁂)) ⟩ 
                (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ swap ∘ (h ⁂ idC) ≈⟨ refl⟩∘⟨ (pullˡ distributeˡ⁻¹∘swap) ⟩
                (τ (X , Y) +₁ idC) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym)) ⟩
                ((idC ∘ τ (X , Y) ∘ swap +₁ swap ∘ idC) ∘ distributeʳ⁻¹) ∘ (h ⁂ idC) ≈⟨ assoc ○ (sym +₁∘+₁) ⟩∘⟨refl ⟩
                ((idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC)) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ≈⟨ assoc ⟩
                (idC +₁ swap) ∘ (τ (X , Y) ∘ swap +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC) ∎)))
              helper : τ _ ∘ (h # ⁂ idC) ∘ swap ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∘ swap
              helper = {!   !}
              τ∘swap-preserving : τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈ ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
              τ∘swap-preserving = begin 
                τ (K.₀ Y , X) ∘ (h # ⁂ idC) ≈⟨ {!   !} ⟩ 
                τ (K.₀ Y , X) ∘ (h # ⁂ K.₁ idC) ≈⟨ {!   !} ⟩ 
                K.₁ (h # ⁂ idC) ∘ τ _ ≈⟨ {!   !} ⟩ 
                {!   !} ≈⟨ {!   !} ⟩ 
                ((τ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) # ∎