bsc-leon-vatthauer/src/Monad/Instance/Delay/Properties.lagda.md

module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
  open Ambient ambient
  open import Categories.Diagram.Coequalizer C 
  open import Monad.Instance.Delay ambient
  open import Algebra.Search ambient
  open import Algebra.ElgotAlgebra ambient
  open import Algebra.Properties ambient
  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
  open import Monad.Instance.Delay.Quotienting ambient

Properties of the quotiented delay monad

  module _ (D : DelayM) where
    open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)

    open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
    open Monad D-Monad using (μ; η) renaming (assoc to M-assoc; identityʳ to M-identityʳ)
    open HomReasoning
    open M C
    open MR C
    open Equiv

    module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
      open Quotiented D coeqs

      cond-1 : Set (o ⊔ ℓ ⊔ e)
      cond-1 = ∀ X → preserves D-Functor (coeqs X)

      -- cond-2' : Set (o ⊔ ℓ ⊔ e)
      -- cond-2' = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
      record cond-2' (X : Obj) : Set (o ⊔ ℓ ⊔ e) where
        field
          s-alg-on : Search-Algebra-on D (Ď₀ X)
          ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
      cond-2 = ∀ X → cond-2' X


      record cond-3' (X : Obj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
        -- Ď₀ X is stable free elgot algebra
        field
          elgot : Elgot-Algebra-on (Ď₀ X)
        elgot-alg = record { A = Ď₀ X ; algebra = elgot }

        open Elgot-Algebra-on elgot
        field
          isFO : IsFreeObject elgotForgetfulF X elgot-alg
        freeobject = IsFreeObject⇒FreeObject elgotForgetfulF X elgot-alg isFO
        field
          isStable : IsStableFreeElgotAlgebra freeobject

        -- ρ is D-algebra morphism
        field
          ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = out # }) (ρ {X})
          ρ-law : ρ ≈ ((ρ ∘ now +₁ idC) ∘ out) #
      cond-3 = ∀ X → cond-3' X

      record cond-4 : Set (o ⊔ ℓ ⊔ e) where

      2⇒3 : cond-2 → cond-3
      2⇒3 c-2 X = record
        { elgot = Elgot-Algebra.algebra (D-Algebra+Search⇒Elgot D (record 
          { A = Ď₀ X 
          ; action = α
          ; commute = epi-DDρ (α ∘ D₁ α) (α ∘ extend (idC)) (sym (begin 
            (α ∘ μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈⟨ pullʳ (μ.commute ρ) ⟩
            α ∘ D₁ ρ ∘ μ.η (D₀ X)        ≈⟨ pullˡ (sym ρ-algebra-morphism) ⟩
            (ρ ∘ μ.η X) ∘ μ.η (D₀ X)     ≈⟨ pullʳ μ∘Dμ ⟩
            ρ ∘ μ.η X ∘ D₁ (μ.η X)       ≈⟨ pullˡ ρ-algebra-morphism ⟩
            (α ∘ D₁ ρ) ∘ D₁ (μ.η X)      ≈⟨ pullʳ (sym D-homomorphism) ⟩
            α ∘ D₁ (ρ ∘ μ.η X)           ≈⟨ (refl⟩∘⟨ (D-resp-≈ ρ-algebra-morphism)) ⟩
            α ∘ D₁ (α ∘ D₁ ρ)            ≈⟨ (refl⟩∘⟨ D-homomorphism) ⟩
            α ∘ D₁ α ∘ D₁ (D₁ ρ)         ≈⟨ sym-assoc ⟩
            (α ∘ D₁ α) ∘ D₁ (D₁ ρ)       ∎))
          ; identity = identity₁ 
          }) (Search-Algebra-on⇒IsSearchAlgebra D s-alg-on))
        ; isFO = {!   !}
        ; isStable = {!   !}
        ; ρ-algebra-morphism = {!   !}
        ; ρ-law = {!   !}
        }
        where
          open cond-2' (c-2 X)
          open Search-Algebra-on s-alg-on
          epi-DDρ : Epi (D₁ (D₁ ρ))
          epi-DDρ = {!   !}
          μ∘Dμ : ∀ {X} → μ.η X ∘ μ.η (D₀ X) ≈ μ.η X ∘ D₁ (μ.η X)
          μ∘Dμ {X} = begin 
            μ.η X ∘ μ.η (D₀ X)                       ≈⟨ sym k-assoc ⟩ 
            extend (extend idC ∘ idC)                ≈⟨ extend-≈ identityʳ ⟩ 
            extend (extend idC)                      ≈⟨ extend-≈ (introˡ k-identityʳ) ⟩ 
            extend ((extend idC ∘ now) ∘ extend idC) ≈⟨ extend-≈ assoc ⟩ 
            extend (extend idC ∘ now ∘ extend idC)   ≈⟨ k-assoc ⟩ 
            μ.η X ∘ D₁ (μ.η X)                       ∎

      1⇒2 : cond-1 → cond-2
      1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = D-universal }
        where
          open Coequalizer (coeqs X) renaming (universal to coeq-universal)
          open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
          s-alg-on : Search-Algebra-on D (Ď₀ X)
          s-alg-on = record 
            { α = α'
            ; identity₁ = ρ-epi (α' ∘ now) idC (begin 
              (α' ∘ now) ∘ ρ    ≈⟨ pullʳ (η.commute ρ) ⟩ 
              α' ∘ D₁ ρ ∘ now   ≈⟨ pullˡ (sym D-universal) ⟩
              (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩
              ρ                 ≈⟨ sym identityˡ ⟩
              idC ∘ ρ           ∎) 
            ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
              (α' ∘ ▷) ∘ D₁ ρ    ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
              α' ∘ D₁ ρ ∘ ▷      ≈⟨ pullˡ (sym D-universal) ⟩
              (ρ ∘ μ.η X) ∘ ▷    ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩
              ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩
              ρ ∘ extend idC     ≈⟨ D-universal ⟩
              α' ∘ D₁ ρ          ∎) 
            }
            where
              μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι
              μ∘Dι = sym k-assoc ○ extend-≈ (cancelˡ k-identityʳ)
              eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι)
              eq₁ = sym (begin 
                D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ 
                D₁ (μ.η X ∘ D₁ ι)      ≈⟨ D-resp-≈ μ∘Dι ⟩
                D₁ (extend ι)          ∎)
              α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin 
                (ρ ∘ μ.η X) ∘ D₁ (extend ι)          ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
                (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩
                ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩
                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N)     ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
                ρ ∘ extend ι ∘ μ.η (X × N)           ≈⟨ pullˡ equality ⟩
                (ρ ∘ D₁ π₁) ∘ μ.η (X × N)            ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
                (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁)             ∎)