bsc-leon-vatthauer/Monad/ElgotMonad.agda

open import Level
open import Categories.Category.Core
open import Categories.Category.Extensive.Bundle
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
open import Categories.Category.Cartesian
open import Categories.Category.Extensive
open import ElgotAlgebra

import Categories.Morphism.Reasoning as MR

module Monad.ElgotMonad {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
  open HomReasoning
  open Cocartesian (Extensive.cocartesian extensive)
  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
  open BinaryProducts products hiding (η)
  open MR C
  open Equiv
  
  open import Categories.Monad
  open import Categories.Functor

  record IsPreElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
    open Monad T
    open Functor F renaming (F₀ to T₀; F₁ to T₁)

    -- every TX needs to be equipped with an elgot algebra structure
    field
      elgotalgebras : ∀ {X} → Elgot-Algebra-on ED (T₀ X)

    module elgotalgebras {X} = Elgot-Algebra-on (elgotalgebras {X})

    -- with the following associativity
    field
      assoc : ∀ {X Y Z} (f : Z ⇒ T₀ X + Z) (h : X ⇒ T₀ Y) 
        → elgotalgebras._# (((μ.η _ ∘ T₁ h) +₁ idC) ∘ f) ≈ (μ.η _ ∘ T₁ h) ∘ (elgotalgebras._# {X}) f
  
  record PreElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isPreElgot : IsPreElgot T

    open IsPreElgot isPreElgot public

  record IsElgot (T : Monad C) : Set (o ⊔ ℓ ⊔ e) where
    open Monad T
    open Functor F renaming (F₀ to T₀; F₁ to T₁)

    -- iteration operator
    field
      _† : ∀ {X Y} → X ⇒ T₀ (Y + X) → X ⇒ T₀ Y
      †-resp-≈ : ∀ {X Y} {f g : X ⇒ T₀ (Y + X)} → f ≈ g → f † ≈ g †

    -- laws
    field
      Fixpoint : ∀ {X Y} {f : X ⇒ T₀ (Y + X)} 
        → f † ≈ (μ.η _ ∘ T₁ [ η.η _ , f † ]) ∘ f
      Naturality : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Y ⇒ T₀ Z} 
        → (μ.η _ ∘ T₁ g) ∘ f † ≈ ((μ.η _ ∘ T₁ [ (T₁ i₁) ∘ g , η.η _ ∘ i₂ ]) ∘ f)†
      Codiagonal : ∀ {X Y} {f : X ⇒ T₀ ((Y + X) + X)} 
        → (T₁ [ idC , i₂ ] ∘ f )† ≈ f † †
      Uniformity : ∀ {X Y Z} {f : X ⇒ T₀ (Y + X)} {g : Z ⇒ T₀ (Y + Z)} {h : Z ⇒ X} 
        → f ∘ h ≈ (T₁ (idC +₁ h)) ∘ g → f † ∘ h ≈ g †

  record ElgotMonad : Set (o ⊔ ℓ ⊔ e) where
    field
      T : Monad C
      isElgot : IsElgot T

    open IsElgot isElgot public

  -- elgot monads are pre-elgot
  Elgot⇒PreElgot : ElgotMonad → PreElgotMonad
  Elgot⇒PreElgot EM = record 
    { T = T 
    ; isPreElgot = record 
      { elgotalgebras = λ {X} → record
        { _# = λ f → ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †
        ; #-Fixpoint = λ {Y} {f} → begin 
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †                                                         ≈⟨ Fixpoint ⟩ 
          (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) ≈⟨ pullˡ ∘[] ⟩
          [ (μ.η _ ∘ T₁ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ T₁ i₁ 
          , (μ.η _ ∘ T₁ [ η.η _ 
                        , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ]) ∘ η.η _ ∘ i₂ ] ∘ f                   ≈˘⟨ []-cong₂ 
                                                                                                    (pushʳ (homomorphism)) 
                                                                                                    (pushˡ (pushʳ (η.commute _)))
                                                                                                  ⟩∘⟨refl ⟩
          [ μ.η _ ∘ T₁ ([ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘  i₁) 
          , (μ.η _ ∘ (η.η _ ∘ [ η.η _ , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ])) ∘ i₂ ] ∘ f            ≈⟨ []-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (pullʳ (pullʳ inject₂)) ⟩∘⟨refl ⟩
          [ μ.η _ ∘ (T₁ (η.η _))
          , μ.η _ ∘ η.η _ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f                                 ≈⟨ []-cong₂ (T.identityˡ) (cancelˡ T.identityʳ) ⟩∘⟨refl ⟩
          [ idC , ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † ] ∘ f                                           ∎
        ; #-Uniformity = λ {X} {Y} {f} {g} {h} H → sym (Uniformity (begin 
            ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ g) ∘ h                           ≈˘⟨ pushʳ H ⟩
            [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ h) ∘ f                    ≈⟨ pullˡ []∘+₁ ⟩
            [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ h ] ∘ f                     ≈⟨ []-cong₂ (trans identityʳ (F-resp-≈ (sym identityʳ))) assoc ⟩∘⟨refl ⟩
            [ T₁ (i₁ ∘ idC) , η.η _ ∘ i₂ ∘ h ] ∘ f                     ≈˘⟨ []-cong₂ (F-resp-≈ +₁∘i₁) (pullʳ +₁∘i₂) ⟩∘⟨refl ⟩
            [ T₁ ((idC +₁ h) ∘ i₁) , (η.η _ ∘ (idC +₁ h)) ∘ i₂ ] ∘ f   ≈⟨ []-cong₂ homomorphism ( pushˡ (η.commute _)) ⟩∘⟨refl ⟩
            [ T₁ (idC +₁ h) ∘ T₁ i₁ , T₁ (idC +₁ h) ∘ η.η _ ∘ i₂ ] ∘ f ≈˘⟨ pullˡ ∘[] ⟩
            T₁ (idC +₁ h) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f ∎))
        ; #-Folding = λ {X} {Y} {f} {h} → begin 
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ ((([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) †) +₁ h))† ≈⟨ †-resp-≈ []∘+₁ ⟩ 
          [ T₁ i₁ ∘ ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f) † , (η.η _ ∘ i₂) ∘ h ] † ≈⟨ {!   !} ⟩
          {!   !} ≈⟨ {!   !} ⟩
          [ [ T₁ i₁ ∘ idC , (η.η _ ∘ i₂) ∘ i₁ ] ∘ f , (η.η _ ∘ i₂) ∘ h ] † ≈˘⟨ †-resp-≈ ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩
          [ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (idC +₁ i₁) ∘ f , [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ i₂ ∘ h ] † ≈˘⟨ †-resp-≈ ∘[] ⟩
          ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])† ∎
        ; #-resp-≈ = λ fg → †-resp-≈ (∘-resp-≈ʳ fg)
        }
      ; assoc = λ {X} {Y} {Z} f h → begin 
        -- TODO tidy up by moving doing sym outside, apply Naturality and then do `†-resp-≈ pullˡ` once.
        ([ T₁ i₁ , η.η _ ∘ i₂ ] ∘ (μ.η Y ∘ T₁ h +₁ idC) ∘ f)†                                                             ≈⟨ †-resp-≈ (pullˡ []∘+₁) ⟩ 
        (([ T₁ i₁ ∘ μ.η _ ∘ T₁ h , (η.η _ ∘ i₂) ∘ idC ] ∘ f)†)                                                            ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ assoc (sym identityʳ))) ⟩
        ([ (T₁ i₁ ∘ μ.η _) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)†                                                                    ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-congʳ (pullˡ (μ.commute _)))) ⟩
        ([ μ.η _ ∘ T₁ (T₁ i₁) ∘ T₁ h , η.η _ ∘ i₂ ] ∘ f)†                                                                 ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ homomorphism) (cancelˡ T.identityʳ))) ⟩
        ([ μ.η _ ∘ T₁ (T₁ i₁ ∘ h) , μ.η _ ∘ η.η _ ∘ η.η _ ∘ i₂ ] ∘ f)†                                                    ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ʳ (F-resp-≈ inject₁)) (∘-resp-≈ʳ (pullʳ inject₂)))) ⟩
        ([ μ.η _ ∘ T₁ ([ T₁ i₁ ∘ h , η.η _ ∘ i₂ ] ∘ i₁) , μ.η _ ∘ (η.η _ ∘ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ i₂ ] ∘ f)†       ≈˘⟨ †-resp-≈ (∘-resp-≈ˡ ([]-cong₂ (pullʳ (sym homomorphism)) (pullʳ (pullˡ (η.sym-commute _))))) ⟩
        ([ (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ T₁ i₁ , (μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ η.η _ ∘ i₂ ] ∘ f)† ≈˘⟨ †-resp-≈ (pullˡ ∘[]) ⟩
        ((μ.η _ ∘ T₁ [ T₁ i₁ ∘ h , η.η _ ∘ i₂ ]) ∘ [ T₁ i₁ , η.η _ ∘ i₂ ] ∘ f)†                                           ≈˘⟨ Naturality ⟩
        (μ.η Y ∘ T₁ h) ∘ ([ T₁ i₁ ,  η.η _ ∘ i₂ ] ∘ f)†                                                                   ∎ 
      } 
    }
    where
      open ElgotMonad EM
      module T = Monad T
      open T using (F; η; μ)
      open Functor F renaming (F₀ to T₀; F₁ to T₁)