open import Level
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category

import Categories.Morphism.Reasoning as MR

module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Category C
  open MR C
  open HomReasoning
  open Equiv
  open Cocartesian cocartesian
  open import Algebra.Elgot cocartesian

  -- iteration preversing morphism between two elgot-algebras
  module _ (E₁ E₂ : Elgot-Algebra) where
    open Elgot-Algebra E₁ renaming (_# to _#₁)
    open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
    record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
      field
        h : A ⇒ B
        preserves : ∀ {X} {f : X ⇒ A + X} → h ∘ (f #₁) ≈ ((h +₁ id) ∘ f)#₂

  -- the category of elgot algebras for a given category
  Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
  Elgot-Algebras = record
    { Obj       = Elgot-Algebra
    ; _⇒_       = Elgot-Algebra-Morphism
    ; _≈_       = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
    ; id        = λ {EB} → let open Elgot-Algebra EB in 
    record { h = id; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
      id ∘ f #           ≈⟨ identityˡ ⟩ 
      f #                ≈⟨ #-resp-≈ (introˡ (+-unique id-comm-sym id-comm-sym)) ⟩
      ((id +₁ id) ∘ f) # ∎ }
    ; _∘_       = λ {EA} {EB} {EC} f g → let 
      open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
      open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
      open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ)
      open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B)
      open Elgot-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈)
      in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin 
        (hᶠ ∘ hᵍ) ∘ (f #ᵃ)                 ≈⟨ pullʳ preservesᵍ ⟩
        (hᶠ ∘ (((hᵍ +₁ id) ∘ f) #ᵇ))       ≈⟨ preservesᶠ ⟩ 
        (((hᶠ +₁ id) ∘ (hᵍ +₁ id) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩ 
        ((hᶠ ∘ hᵍ +₁ id) ∘ f) #ᶜ           ∎ }
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; equiv     = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    ; ∘-resp-≈  = ∘-resp-≈
    }
    where open Elgot-Algebra-Morphism