open import Level
open import Categories.Category.Core
open import Categories.Object.Initial
open import Categories.Object.Terminal
open import Categories.Object.NaturalNumbers.Properties.F-Algebras
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Category.Distributive using (Distributive)
open import Categories.Object.NaturalNumbers.Parametrized
open import Categories.Category.Construction.EilenbergMoore using (Module)
open import Monad.Instance.Delay using (DelayM)

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

-- Lemma 6.3

module Algebra.Elgot.MoreProperties {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (DM : DelayM (Distributive.cocartesian distributive)) (PNNO : ParametrizedNNO C (Distributive.cartesian distributive)) where
  open Category C
  open import Category.Distributive.Helper distributive
  open Bundles
  open import Algebra.Elgot cocartesian
  open import Algebra.Search cocartesian DM
  open import Algebra.Search.Properties cocartesian DM
  open Equiv
  open HomReasoning
  open DelayM DM
  open D-Monad
  open D-Kleisli

  module _ (algebra : Elgot-Algebra) where
    open import Monad.Instance.Delay.Iota distributive DM PNNO
    open Search-Algebra (Elgot⇒Search algebra)
    open Module (Elgot⇒D-Algebra algebra) using (commute)
    open MR C
    open M C
    open ParametrizedNNO PNNO renaming (N to ℕ; unique to pnno-unique)
    open import Monad.Helper using (extend⇒F₁)

    α-coequalize : α ∘ extend ι ≈ α ∘ D.F.₁ (π₁ {A} {ℕ})
    α-coequalize = begin 
      α ∘ extend ι          ≈⟨ refl⟩∘⟨ extend⇒F₁ kleisli ι ⟩ 
      α ∘ D.μ.η _ ∘ D.F.₁ ι ≈˘⟨ extendʳ commute ⟩ 
      α ∘ D.F.₁ α ∘ D.F.₁ ι ≈˘⟨ refl⟩∘⟨ D.F.homomorphism ⟩ 
      α ∘ D.F.₁ (α ∘ ι)     ≈⟨ refl⟩∘⟨ (D.F.F-resp-≈ α∘ι) ⟩ 
      α ∘ D.F.₁ π₁          ∎
      where
      α∘ι : α ∘ ι ≈ π₁ {A} {ℕ}
      α∘ι = begin 
        α ∘ ι           ≈⟨ pnno-unique (sym IB₁) (sym IS₁) ⟩
        universal id id ≈˘⟨ pnno-unique (sym IB₂) (sym IS₂) ⟩
        π₁              ∎
        where
        IB₁ : (α ∘ ι) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈ id
        IB₁ = begin 
          (α ∘ ι) ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ ι-zero ⟩ 
          α ∘ now                                    ≈⟨ identity₁ ⟩ 
          id                                         ∎
        IS₁ : (α ∘ ι) ∘ (id ×₁ s) ≈ id ∘ α ∘ ι
        IS₁ = begin 
          (α ∘ ι) ∘ (id ×₁ s) ≈⟨ pullʳ ι-succ ⟩ 
          α ∘ later ∘ ι       ≈⟨ pullˡ identity₂ ⟩ 
          α ∘ ι               ≈˘⟨ identityˡ ⟩ 
          id ∘ α ∘ ι          ∎
        IB₂ : π₁ ∘ ⟨ id , z ∘ Terminal.! terminal ⟩ ≈ id
        IB₂ = project₁
        IS₂ : π₁ ∘ (id ×₁ s) ≈ id ∘ π₁
        IS₂ = project₁