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 Distributive distributive
open import Categories.Category.Distributive.Properties distributive
open Cocartesian cocartesian
open Cartesian cartesian using (terminal; products)
open BinaryProducts products renaming (unique to ⟨⟩-unique)
open Terminal terminal
open CartesianMonoidal cartesian using (monoidal)
open import Monad.Instance.Maybe.Strong distributive
open Symmetric (symmetric C cartesian) using (braided)
open Commutative
First a general fact about the distributivity morphisms:
distribute₄ : ∀ {A B C D} → (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ {A + B} {C} {D} ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹
distribute₄ = Iso⇒Epi (IsIso.iso isIsoʳ) ((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) (begin
(((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeʳ) ≈⟨ ∘[] ⟩
[ (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₁ ⁂ id)) , (((distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ (i₂ ⁂ id)) ] ≈⟨ []-cong₂ (pullʳ ((refl⟩∘⟨ (⁂-cong₂ refl (sym (+-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₁ id id))) (pullʳ (((refl⟩∘⟨ (⁂-cong₂ refl (sym (+-unique id-comm-sym id-comm-sym)))) ○ sym (distributeˡ⁻¹-natural i₂ id id)))) ⟩
[ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₁ ⁂ id) +₁ (i₁ ⁂ id)) ∘ distributeˡ⁻¹ , (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ ((i₂ ⁂ id) +₁ (i₂ ⁂ id)) ∘ distributeˡ⁻¹ ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₁ distributeʳ⁻¹-i₁)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ distributeʳ⁻¹-i₂ distributeʳ⁻¹-i₂)) ⟩
[ (i₁ +₁ i₁) ∘ distributeˡ⁻¹ , (i₂ +₁ i₂) ∘ distributeˡ⁻¹ ] ≈˘⟨ []∘+₁ ⟩
([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹)) ≈˘⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoʳ)) ⟩
(([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeʳ) ∎)
The proof of commutative follows by some rewriting:
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 ∎