open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Cartesian.Monoidal
open import Categories.Category.Cartesian.SymmetricMonoidal
open import Categories.Category.Distributive using (Distributive)
open import Categories.Object.Terminal using (Terminal)
open import Categories.Monad.Commutative using (Commutative; CommutativeMonad)
open import Categories.Category.Monoidal.Symmetric using (Symmetric)

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

-- Maybe is a Commutative Monad

module Monad.Instance.Maybe.Commutative {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Category C
  open M C
  open MR C
  open MP C
  open HomReasoning
  open Equiv
  open import Category.Distributive.Helper distributive
  open Bundles
  open Terminal terminal

  open import Monad.Instance.Maybe.Strong distributive
  open Commutative

  maybeCommutative : Commutative braided maybeStrong
  maybeCommutative .commutes {X} {Y} = begin 
    [ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ id) ∘ (id +₁ !) ∘ distributeˡ⁻¹                                                                                                ≈⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ)) ⟩ 
    [ id , i₂ ] ∘ ((swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap +₁ !) ∘ distributeˡ⁻¹                                                                                                             ≈⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl) ⟩ 
    [ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹                                                                                                                     ≈⟨ ([]-cong₂ (refl⟩∘⟨ (pullʳ distributeˡ⁻¹∘swap)) (refl⟩∘⟨ !-unique (! ∘ distributeʳ⁻¹))) ⟩∘⟨refl ⟩ 
    [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ , i₂ ∘ ! ∘ distributeʳ⁻¹ ] ∘ distributeˡ⁻¹                                                                                             ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ assoc²βε assoc) ⟩ 
    [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹                                                                                          ≈⟨ refl⟩∘⟨ distribute₄ ⟩ 
    [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹                                                                ≈⟨ pullˡ ∘[] ⟩ 
    [ [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₁ +₁ i₁) , [ (swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap) , i₂ ∘ ! ] ∘ (i₂ +₁ i₂) ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹   ≈⟨ ([]-cong₂ []∘+₁ []∘+₁) ⟩∘⟨refl ⟩ 
    [ [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₁ , (i₂ ∘ !) ∘ i₁ ] , [ ((swap +₁ id) ∘ (id +₁ !) ∘ (swap +₁ swap)) ∘ i₂ , (i₂ ∘ !) ∘ i₂ ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ (pullʳ inject₁)) (pullʳ (sym (!-unique (! ∘ i₁))))) ([]-cong₂ (pullʳ (pullʳ inject₂)) (pullʳ (sym (!-unique (! ∘ i₂)))))) ⟩∘⟨refl ⟩ 
    [ [ (swap +₁ id) ∘ (id +₁ !) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (id +₁ !) ∘ i₂ ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹                                       ≈⟨ ([]-cong₂ ([]-cong₂ (refl⟩∘⟨ (pullˡ (inject₁ ○ identityʳ))) refl) ([]-cong₂ (refl⟩∘⟨ (pullˡ inject₂)) refl)) ⟩∘⟨refl ⟩ 
    [ [ (swap +₁ id) ∘ i₁ ∘ swap , i₂ ∘ ! ] , [ (swap +₁ id) ∘ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹                                                         ≈⟨ ([]-cong₂ ([]-cong₂ (pullˡ inject₁) refl) ([]-cong₂ (pullˡ (pullˡ (inject₂ ○ identityʳ))) refl)) ⟩∘⟨refl ⟩ 
    [ [ (i₁ ∘ swap) ∘ swap , i₂ ∘ ! ] , [ (i₂ ∘ !) ∘ swap , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹                                                                              ≈⟨ ([]-cong₂ ([]-cong₂ (pullʳ swap∘swap) refl) ([]-cong₂ (pullʳ (sym (!-unique (! ∘ swap)))) refl)) ⟩∘⟨refl ⟩ 
    [ id +₁ ! , [ i₂ ∘ ! , i₂ ∘ ! ] ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹                                                                                                               ≈⟨ pullˡ []∘+₁ ⟩ 
    [ (id +₁ !) ∘ distributeˡ⁻¹ , [ i₂ ∘ ! , i₂ ∘ ! ] ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹                                                                                                                ≈⟨ ([]-cong₂ refl ((sym ∘[]) ⟩∘⟨refl)) ⟩∘⟨refl ⟩ 
    [ (id +₁ !) ∘ distributeˡ⁻¹ , (i₂ ∘ [ ! , ! ]) ∘ distributeˡ⁻¹ ] ∘ distributeʳ⁻¹                                                                                                                   ≈⟨ ([]-cong₂ refl (pullʳ (sym (!-unique ([ ! , ! ] ∘ distributeˡ⁻¹))))) ⟩∘⟨refl ⟩ 
    [ (id +₁ !) ∘ distributeˡ⁻¹ , i₂ ∘ ! ] ∘ distributeʳ⁻¹                                                                                                                                             ≈˘⟨ ([]-cong₂ (cancelʳ swap∘swap) (pullʳ (sym (!-unique (! ∘ swap))))) ⟩∘⟨refl ⟩ 
    [ (((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) ∘ swap , (i₂ ∘ !) ∘ swap ] ∘ distributeʳ⁻¹                                                                                                                  ≈˘⟨ pullˡ []∘+₁ ⟩ 
    [ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ (swap +₁ swap) ∘ distributeʳ⁻¹                                                                                                                   ≈˘⟨ pullʳ distributeˡ⁻¹∘swap ⟩ 
    ([ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap , i₂ ∘ ! ] ∘ distributeˡ⁻¹) ∘ swap                                                                                                                           ≈˘⟨ pullˡ (pullˡ ([]∘+₁ ○ []-cong₂ identityˡ (refl⟩∘⟨ identityˡ))) ⟩ 
    [ id , i₂ ] ∘ (((((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap) +₁ id ∘ !) ∘ distributeˡ⁻¹) ∘ swap                                                                                                            ≈˘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²) ○ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ refl))) ⟩ 
    [ id , i₂ ] ∘ ((id +₁ !) ∘ distributeˡ⁻¹ +₁ id) ∘ (swap +₁ id) ∘ ((id +₁ !) ∘ distributeˡ⁻¹) ∘ swap                                                                                                ∎

  maybeCommutativeMonad : CommutativeMonad braided
  maybeCommutativeMonad = record { strongMonad = maybeStrong ; commutative = maybeCommutative }