open import Categories.Category.Core
open import Categories.Category.Distributive
open import Monad.Helper
open import Data.Product using (_,_)

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Monad.Instance.K as MIK


-- The monad K is copyable and weakly discardable.
module Monad.Instance.K.Copy {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (MK : MIK.MonadK distributive) where
  open import Category.Distributive.Helper distributive renaming (η to η-prod)
  open import Monad.Instance.K.OrderEnriched distributive MK
  open Bundles
  open MIK distributive
  open MonadK MK
  open Category C
  open HomReasoning
  open MR C
  open Equiv
  
  open kleisliK using (extend; extend-≈)
  open monadK using (μ)
  open import Monad.Instance.K.Strong distributive MK
  open import Monad.Instance.K.Commutative distributive MK
  open import Monad.Instance.K.EquationalLifting distributive MK
  open import Monad.Instance.K.Restriction distributive MK
  open strongK using (strengthen; strength-assoc)

  KCopyable : ∀ {X : Obj} → extend (σ (X , X)) ∘ τ (K.₀ X , X) ∘ Δ ≈ K.₁ Δ
  KCopyable = begin 
    extend (σ _) ∘ τ _ ∘ Δ           ≈⟨ refl⟩∘⟨ equationalLifting ⟩ 
    extend (σ _) ∘ K.₁ ⟨ η _ , id ⟩  ≈⟨ extend∘F₁ monadK (σ _) ⟨ η _ , id ⟩ ⟩ 
    extend (σ _ ∘ ⟨ η _ , id ⟩)      ≈˘⟨ extend-≈ (∘-resp-≈ʳ ×₁∘Δ) ⟩ 
    extend (σ _ ∘ ( η _ ×₁ id ) ∘ Δ) ≈⟨ extend-≈ (pullˡ σ-η) ⟩ 
    extend (η _ ∘ Δ)                 ≈⟨ F₁⇒extend monadK Δ ⟩ 
    K.₁ Δ                            ∎

  KDiscardable : ∀ {X Y Z : Obj} {f : X ⇒ K.₀ Y} {g : X ⇒ K.₀ Z} → (K.₁ π₁ ∘ extend (σ _) ∘ τ _ ∘ ⟨ f , g ⟩) ⊑ f
  KDiscardable {f = f} {g} = ⊑-cong₂ (sym helper) kleisliK.identityʳ (⊑∘ʳ {h = f} (f↓⊑η {f = g}))
    where
      helper : K.₁ π₁ ∘ extend (σ _) ∘ τ _ ∘ ⟨ f , g ⟩ ≈ extend f ∘ g ↓
      helper = begin 
        K.₁ π₁ ∘ extend (σ _) ∘ τ _ ∘ ⟨ f , g ⟩      ≈⟨ pullˡ (F₁∘extend monadK π₁ (σ _) ○ extend-≈ σ-π₁) ⟩ 
        extend π₁ ∘ τ _ ∘ ⟨ f , g ⟩                  ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ (×₁∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
        extend π₁ ∘ τ _ ∘ (f ×₁ id) ∘ ⟨ id , g ⟩     ≈⟨ refl⟩∘⟨ extendʳ (τ-comm-id f) ⟩ 
        extend π₁ ∘ K.₁ (f ×₁ id) ∘ τ _ ∘ ⟨ id , g ⟩ ≈⟨ pullˡ (extend∘F₁ monadK π₁ (f ×₁ id) ○ extend-≈ project₁) ⟩ 
        extend (f ∘ π₁) ∘ τ _ ∘ ⟨ id , g ⟩           ≈˘⟨ pullˡ (extend∘F₁ monadK f π₁) ⟩ 
        extend f ∘ g ↓                               ∎