open import Level
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Category.Core using (Category)
open import Categories.Category.Cocartesian

import Categories.Morphism.Reasoning as MR

module Algebra.Elgot {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Category C
  open Cocartesian cocartesian
  open MR C
  open import Algebra.UniformIteration cocartesian
  open HomReasoning
  open Equiv
  
  private
    -- identity algebra
    Id-Algebra : Obj → F-Algebra (idF {C = C})
    Id-Algebra A = record
      { A = A
      ; α = id
      }
     where open Functor (idF {C = C})

  record Guarded-Elgot-Algebra-on {F : Endofunctor C} (FA : F-Algebra F) : Set (o ⊔ ℓ ⊔ e) where
    open Functor F public
    open F-Algebra FA public
    -- iteration operator
    field
      _# : ∀ {X} → (X ⇒ A + F₀ X) → (X ⇒ A)

    -- _# properties
    field 
      #-Fixpoint : ∀ {X} {f : X ⇒ A + F₀ X }
        → f # ≈ [ id , α ∘ F₁ (f #) ] ∘ f
      #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} 
        → (id +₁ F₁ h) ∘ f ≈ g ∘ h
        → f # ≈ g # ∘ h
      #-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
        → (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
      #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} 
        → f ≈ g 
        → (f #) ≈ (g #)

  record Guarded-Elgot-Algebra (F : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
    field
      algebra : F-Algebra F
      guarded-elgot-algebra-on : Guarded-Elgot-Algebra-on algebra
    open Guarded-Elgot-Algebra-on guarded-elgot-algebra-on public

  record Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
    -- iteration operator
    field
      _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)

    -- _# properties
    field
      #-Fixpoint : ∀ {X} {f : X ⇒ A + X }
        → f # ≈ [ id , f # ] ∘ f
      #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} 
        → (id +₁ h) ∘ f ≈ g ∘ h
        → f # ≈ g # ∘ h
      #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
        → ((f #) +₁ h)# ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] #
      #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)

    -- Compositionality is derivable
    #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
      → (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
    #-Compositionality {X} {Y} {f} {h} = begin 
      (((f #) +₁ id) ∘ h)#                               ≈⟨ #-Uniformity {f = ((f #) +₁ id) ∘ h} 
                                                                          {g = (f #) +₁ h} 
                                                                          {h = h} 
                                                                          (trans (pullˡ +₁∘+₁) (+₁-cong₂ identityˡ identityʳ ⟩∘⟨refl))⟩ 
      ((f # +₁ h)# ∘ h)                                  ≈˘⟨ inject₂ ⟩
      (([ id ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂))          ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
      (([ id , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂)       ≈˘⟨ #-Fixpoint {f = (f # +₁ h) } ⟩∘⟨refl ⟩
      (f # +₁ h)# ∘ i₂                                   ≈⟨ #-Folding ⟩∘⟨refl ⟩
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂)               ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩
      ([ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] 
      ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂                ≈⟨ pullʳ inject₂ ⟩
      [ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h)  ≈⟨ pullˡ inject₂ ⟩ 
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h)                ≈˘⟨ refl⟩∘⟨ inject₂ {f = i₁} {g = h} ⟩ 
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ] ∘ i₂)  ≈˘⟨ pushˡ (#-Uniformity {f = [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} 
                                                                                  {g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]} 
                                                                                  {h = [ i₁ , h ]} 
                                                                                  (begin
        (id +₁ [ i₁ , h ]) 
        ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                  ≈⟨ refl⟩∘⟨ ∘[] ⟩
        (id +₁ [ i₁ , h ]) ∘ [ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ 
            , [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                     ≈⟨ refl⟩∘⟨ []-congʳ inject₁ ⟩
        (id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f 
            , [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                     ≈⟨ ∘[] ⟩
        [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f) 
        , (id +₁ [ i₁ , h ]) ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ]  ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ ∘[]) ⟩
        [ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
        , [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f) 
        , (id +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ]                     ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) 
                                                                            (∘-resp-≈ˡ ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ inject₂))) ⟩
        [ (id +₁ i₁) ∘ f , ([ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
        , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ]                            ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) 
                                                                                                (pullʳ inject₂))) ⟩
        [ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]         ≈˘⟨ []-congʳ inject₁ ⟩
        [ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ 
        , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                          ≈˘⟨ ∘[] ⟩
        [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                     ∎))
      ⟩
      ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂  ∎

    #-Stutter : ∀ {X Y} (f : X ⇒ (Y + Y) + X) (h : Y ⇒ A) → (([ h , h ] +₁ id) ∘ f)# ≈ [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂
    #-Stutter {X} {Y} f h = begin 
      (([ h , h ] +₁ id) ∘ f)#                                        ≈⟨ #-resp-≈ ((+₁-cong₂ (sym help) refl) ⟩∘⟨refl) ⟩ 
      (((h +₁ i₁) # +₁ id) ∘ f) #                                     ≈⟨ #-Compositionality ⟩
      ([ (id +₁ i₁) ∘ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂      ≈⟨ ((#-resp-≈ (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) refl) ⟩∘⟨refl)) ⟩∘⟨refl) ⟩
      ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ i₂              ≈˘⟨ (refl⟩∘⟨ (+₁∘i₂ ○ identityʳ)) ⟩
      ([ (h +₁ i₁ ∘ i₁) , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) # ∘ (i₁ +₁ id) ∘ i₂ ≈⟨ pullˡ (sym (#-Uniformity (sym by-uni))) ⟩
      [ i₁ ∘ h , [ h +₁ i₁ , i₂ ∘ i₂ ] ∘ f ] # ∘ i₂                   ∎
      where
        help : (h +₁ i₁) # ≈ [ h , h ]
        help = begin 
          ((h +₁ i₁) #)                                   ≈⟨ #-Fixpoint ⟩ 
          [ id , (h +₁ i₁) # ] ∘ (h +₁ i₁)                ≈⟨ []∘+₁ ○ []-cong₂ identityˡ refl ⟩ 
          [ h , (h +₁ i₁) # ∘ i₁ ]                        ≈⟨ []-cong₂ refl (#-Fixpoint ⟩∘⟨refl) ⟩ 
          [ h , ([ id , (h +₁ i₁) # ] ∘ (h +₁ i₁)) ∘ i₁ ] ≈⟨ []-cong₂ refl (pullʳ +₁∘i₁) ⟩ 
          [ h , [ id , (h +₁ i₁) # ] ∘ i₁ ∘ h ]           ≈⟨ []-cong₂ refl (cancelˡ inject₁) ⟩ 
          [ h , h ]                                       ∎
        by-uni : ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ id) ≈ (id +₁ (i₁ +₁ id)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]
        by-uni = begin 
          ([ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ [ i₁ , f ]) ∘ (i₁ +₁ id)                                                  ≈⟨ ((∘[] ○ []-cong₂ inject₁ refl) ⟩∘⟨refl) ⟩ 
          [ h +₁ i₁ ∘ i₁ , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ∘ (i₁ +₁ id)                                          ≈⟨ ([]∘+₁ ○ []-cong₂ +₁∘i₁ identityʳ) ⟩ 
          [ i₁ ∘ h , [ h +₁ i₁ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ]                                                             ≈˘⟨ []-cong₂ (pullˡ (+₁∘i₁ ○ identityʳ)) (([]-cong₂ (+₁∘+₁ ○ +₁-cong₂ identityˡ +₁∘i₁) (pullˡ +₁∘i₂ ○ pullʳ (+₁∘i₂ ○ identityʳ))) ⟩∘⟨refl) ⟩ 
          [ (id +₁ (i₁ +₁ id)) ∘ i₁ ∘ h , [ (id +₁ (i₁ +₁ id)) ∘ (h +₁ i₁) , (id +₁ (i₁ +₁ id)) ∘ i₂ ∘ i₂ ] ∘ f ] ≈˘⟨ []-cong₂ refl (pullˡ ∘[]) ⟩
          [ (id +₁ (i₁ +₁ id)) ∘ i₁ ∘ h , (id +₁ (i₁ +₁ id)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                      ≈˘⟨ ∘[] ⟩
          (id +₁ (i₁ +₁ id)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                                           ∎

    #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((id +₁ ∇) ∘ f)# ≈ ([ i₁ , ((id +₁ ∇) ∘ f) # +₁ id ] ∘ f) #
    #-Diamond {X} f = begin 
      g #                                                                                                          ≈⟨ introʳ inject₂ ⟩ 
      g # ∘ ∇ ∘ i₂                                                                                                 ≈⟨ pullˡ (sym (#-Uniformity by-uni₁)) ⟩ 
      [ (id +₁ i₁) ∘ g , f ] # ∘ i₂                                                                                ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (elimˡ (+-unique id-comm-sym id-comm-sym)))) ⟩∘⟨refl) ⟩ 
      [ (id +₁ i₁) ∘ g , (id +₁ id) ∘ f ] # ∘ i₂                                                                   ≈˘⟨ ((#-resp-≈ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₁ identityˡ)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identityˡ)))) ⟩∘⟨refl) ⟩
      [ (∇ +₁ id) ∘ ((i₁ +₁ i₁) ∘ g) , (∇ +₁ id) ∘ ((i₂ +₁ id) ∘ f) ] # ∘ i₂                                       ≈˘⟨ ((#-resp-≈ ∘[]) ⟩∘⟨refl) ⟩
      ((∇ +₁ id) ∘ [ ((i₁ +₁ i₁) ∘ g) , ((i₂ +₁ id) ∘ f) ]) # ∘ i₂                                                 ≈⟨ ((#-Stutter [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ] id) ⟩∘⟨refl) ⟩ 
      ([ i₁ ∘ id , [ id +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ] ] # ∘ i₂) ∘ i₂                     ≈⟨ (assoc ○ ((#-resp-≈ ([]-cong₂ identityʳ refl)) ⟩∘⟨refl)) ⟩
      [ i₁ , ([ id +₁ i₁ , i₂ ∘ i₂ ] ∘ [ (i₁ +₁ i₁) ∘ g , (i₂ +₁ id) ∘ f ]) ] # ∘ i₂ ∘ i₂                          ≈⟨ ((#-resp-≈ ([]-cong₂ refl (∘[] ○ []-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁)))) ⟩∘⟨refl) ⟩ 
      [ i₁ , [ [ (id +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (id +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ id ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
      [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂                               ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
      [ i₁ , [ [ i₁ , i₂ ] ∘ (id +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂                          ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
      [ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂                                                        ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩
      [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ i₂ ∘ i₂                               ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
      [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X}                                         ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ 
      [ (id +₁ i₁) ∘ [ i₁ , (id +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂                                                     ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
      ([ i₁ , (id +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂                                                                       ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ 
      ([ id , g # ] +₁ h ) # ∘ i₂                                                                                  ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ((sym ∘[] ○ elimʳ +-η) ⟩∘⟨refl))) ⟩∘⟨refl) ⟩ 
      [ i₁ ∘ [ id , g # ] , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ h ] # ∘ i₂                                                     ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl (pullˡ ([]∘+₁ ○ []-cong₂ inject₂ identityʳ)))) ⟩∘⟨refl) ⟩ 
      [ i₁ ∘ [ id , g # ] , [ [ id , g # ] +₁ i₁ , i₂ ∘ i₂ ] ∘ (i₂ +₁ id) ∘ h ] # ∘ i₂                             ≈⟨ sym (#-Stutter ((i₂ +₁ id) ∘ h) [ id , g # ]) ⟩ 
      (([ [ id , g # ] , [ id , g # ] ] +₁ id) ∘ (i₂ +₁ id) ∘ h) #                                                 ≈⟨ #-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ inject₂ identity²)) ⟩ 
      ((([ id , g # ] +₁ id)) ∘ h) #                                                                               ≈⟨ #-resp-≈ (pullˡ (∘[] ○ []-cong₂ (pullˡ +₁∘i₁) +₁∘+₁)) ⟩ 
      ([ (i₁ ∘ [ id , g # ]) ∘ i₁ , [ id , g # ] ∘ i₂ +₁ id ∘ id ] ∘ f) #                                          ≈⟨ #-resp-≈ (([]-cong₂ (cancelʳ inject₁) (+₁-cong₂ inject₂ identity²)) ⟩∘⟨refl) ⟩ 
      ([ i₁ , g # +₁ id ] ∘ f) #                                                                                   ∎
      where
        g = (id +₁ ∇) ∘ f
        h = [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ f
        by-uni₂ : (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ id ]
        by-uni₂ = begin 
          (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ i₁ , [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]                                       ≈⟨ ∘[] ⟩ 
          [ (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ i₁ , (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ [ (id +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]      ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩ 
          [ i₁ , [ (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ (id +₁ i₂ ∘ i₁) ∘ g , (id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ i₂ ∘ f ] ]      ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩ 
          [ i₁ , [ (id ∘ id +₁ [ i₁ ∘ i₁ , i₂ +₁ id ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ id ]) ∘ f ] ]               ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩ 
          [ i₁ , [ (id +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ id) ] ∘ f ] ]                                        ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩ 
          [ i₁ , [ (id +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ]                                                                        ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩ 
          [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ id ] ]                    ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩ 
          [ [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ id) ] ≈˘⟨ ∘[] ⟩ 
          [ [ i₁ , (id +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ id ]                                               ∎
        by-uni₁ : (id +₁ ∇) ∘ [ (id +₁ i₁) ∘ g , f ] ≈ g ∘ ∇
        by-uni₁ = begin 
          (id +₁ ∇) ∘ [ (id +₁ i₁) ∘ g , f ]             ≈⟨ ∘[] ⟩ 
          [ (id +₁ ∇) ∘ (id +₁ i₁) ∘ g , (id +₁ ∇) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩ 
          [ (id +₁ id) ∘ g , (id +₁ ∇) ∘ f ]             ≈⟨ []-cong₂ (elimˡ (+-unique id-comm-sym id-comm-sym)) refl ⟩ 
          [ g , g ]                                      ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
          g ∘ ∇                                          ∎
        by-fix : [ i₁ , (id +₁ i₂) ∘ g ] # ≈ [ id , g # ]
        by-fix = sym (begin 
          [ id , g # ]                                                 ≈⟨ []-cong₂ refl #-Fixpoint ⟩ 
          [ id , [ id , g # ] ∘ g ]                                    ≈⟨ []-cong₂ refl (([]-cong₂ refl (#-Uniformity (sym inject₂))) ⟩∘⟨refl) ⟩ 
          [ id , [ id , [ i₁ , (id +₁ i₂) ∘ g ] # ∘ i₂ ] ∘ g ]         ≈˘⟨ ∘[] ○ []-cong₂ inject₁ (pullˡ ([]∘+₁ ○ []-cong₂ identity² refl)) ⟩ 
          [ id , [ i₁ , (id +₁ i₂) ∘ g ] # ] ∘ [ i₁ , (id +₁ i₂) ∘ g ] ≈˘⟨ #-Fixpoint ⟩ 
          ([ i₁ , (id +₁ i₂) ∘ g ] #)                                  ∎)


  -- An alternative definition of Elgot Algebras using the Diamond law
  record Diamond-Elgot-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
    -- iteration operator
    field
      _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)

    -- _# properties
    field
      #-Fixpoint : ∀ {X} {f : X ⇒ A + X }
        → f # ≈ [ id , f # ] ∘ f
      #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} 
        → (id +₁ h) ∘ f ≈ g ∘ h
        → f # ≈ g # ∘ h
      #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) 
        → ((id +₁ ∇) ∘ f)# ≈ ([ i₁ , ((id +₁ ∇) ∘ f) # +₁ id ] ∘ f) #
      #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)

    #-Compositionality : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y}
      → (((f #) +₁ id) ∘ h)# ≈ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂
    #-Compositionality {X} {Y} {f} {h} = begin 
      (((f #) +₁ id) ∘ h) #                             ≈⟨ helper₂ ⟩ 
      ([ i₁ , ((id +₁ ∇) ∘ w) # +₁ id ] ∘ w) # ∘ i₂     ≈˘⟨ #-Diamond w ⟩∘⟨refl ⟩ 
      ((id +₁ ∇) ∘ w) # ∘ i₂                            ≈⟨ #-resp-≈ helper₁ ⟩∘⟨refl ⟩ 
      ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂ ∎
      where
      Z = X + Y
      w : Z ⇒ A + (Z + Z)
      w = [ (id +₁ i₁ ∘ i₁) ∘ f , i₂ ∘ i₂ ∘ i₂ ] ∘ [ i₁ , h ]
      helper₁ : (id +₁ ∇) ∘ w ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]
      helper₁ = begin 
        (id +₁ ∇) ∘ [ (id +₁ i₁ ∘ i₁) ∘ f , i₂ ∘ i₂ ∘ i₂ ] ∘ [ i₁ , h ]                  ≈⟨ ∘-resp-≈ʳ (∘[] ○ []-cong₂ inject₁ refl) ⟩
        (id +₁ ∇) ∘ [ (id +₁ i₁ ∘ i₁) ∘ f , [ (id +₁ i₁ ∘ i₁) ∘ f , i₂ ∘ i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘[] ○ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² (cancelˡ inject₁))) (pullˡ (∘[] ○ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² (cancelˡ inject₁))) (pullˡ inject₂ ○ pullʳ (cancelˡ inject₂)))) ⟩
        [ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                            ≈˘⟨ ∘[] ○ []-cong₂ inject₁ refl ⟩
        [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                                        ∎
      helper₂ : ((f # +₁ id) ∘ h) # ≈ ([ i₁ , ((id +₁ ∇) ∘ w) # +₁ id ] ∘ w) # ∘ i₂
      helper₂ = #-Uniformity (begin 
        (id +₁ i₂) ∘ (f # +₁ id) ∘ h                                                  ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
        (f # +₁ i₂) ∘ h                                                               ≈⟨ (+₁-cong₂ #-Fixpoint refl) ⟩∘⟨refl ⟩ 
        ([ id , f # ] ∘ f +₁ i₂) ∘ h                                                  ≈⟨ (+₁-cong₂ (∘-resp-≈ˡ ([]-cong₂ refl sub-helper)) refl) ⟩∘⟨refl ⟩ 
        ([ id , ((id +₁ ∇) ∘ w) # ∘ i₁ ] ∘ f +₁ i₂) ∘ h                               ≈⟨ ([]-cong₂ (pullˡ (∘[] ○ []-cong₂ identityʳ refl)) refl) ⟩∘⟨refl ⟩ 
        [ [ i₁ , i₁ ∘ ((id +₁ ∇) ∘ w) # ∘ i₁ ] ∘ f , i₂ ∘ i₂ ] ∘ h                    ≈˘⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ (extendʳ inject₁))) (pullˡ inject₂ ○ pullˡ (inject₂ ○ identityʳ))) ⟩ 
        [ i₁ , ((id +₁ ∇) ∘ w) # +₁ id ] ∘ [ (id +₁ i₁ ∘ i₁) ∘ f , i₂ ∘ i₂ ∘ i₂ ] ∘ h ≈˘⟨ pullʳ (pullʳ inject₂) ⟩ 
        ([ i₁ , ((id +₁ ∇) ∘ w) # +₁ id ] ∘ w) ∘ i₂                                   ∎)
        where
        sub-helper : f # ≈ ((id +₁ ∇) ∘ w) # ∘ i₁
        sub-helper = #-Uniformity (begin 
          (id +₁ i₁) ∘ f                                          ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² (cancelˡ inject₁)) ⟩ 
          (id +₁ ∇) ∘ (id +₁ i₁ ∘ i₁) ∘ f                         ≈˘⟨ refl⟩∘⟨ inject₁ ⟩ 
          (id +₁ ∇) ∘ [ (id +₁ i₁ ∘ i₁) ∘ f , i₂ ∘ i₂ ∘ i₂ ] ∘ i₁ ≈˘⟨ pullʳ (pullʳ inject₁) ⟩ 
          ((id +₁ ∇) ∘ w) ∘ i₁                                    ∎)

  Diamond-on⇒Guarded-on : ∀ A → Diamond-Elgot-Algebra-on A → Guarded-Elgot-Algebra-on {idF} (Id-Algebra A)
  Diamond-on⇒Guarded-on A DA = record
    { _# = _#
    ; #-Fixpoint = λ {X} {f} → #-Fixpoint ○ ∘-resp-≈ˡ ([]-cong₂ refl (sym identityˡ))
    ; #-Uniformity = #-Uniformity
    ; #-Compositionality = #-Compositionality
    ; #-resp-≈ = #-resp-≈
    }
    where open Diamond-Elgot-Algebra-on DA

  record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
    field
      A : Obj
      algebra : Elgot-Algebra-on A
    open Elgot-Algebra-on algebra public

  -- constructing an Id-Guarded Elgot-Algebra from an unguarded one
  Unguarded⇒Id-Guarded : (EA : Elgot-Algebra) → Guarded-Elgot-Algebra-on (Id-Algebra (Elgot-Algebra.A EA))
  Unguarded⇒Id-Guarded ea = record
      { _# = _#
      ; #-Fixpoint = λ {X} {f} → #-Fixpoint ○ ∘-resp-≈ˡ ([]-cong₂ refl (sym identityˡ))
      ; #-Uniformity = #-Uniformity
      ; #-Compositionality = #-Compositionality
      ; #-resp-≈ = #-resp-≈
      }
    where 
    open Elgot-Algebra ea

  -- constructing an unguarded Elgot-Algebra from an Id-Guarded one 
  Id-Guarded⇒Unguarded : ∀ {A} → Guarded-Elgot-Algebra-on (Id-Algebra A) → Elgot-Algebra
  Id-Guarded⇒Unguarded gea = record 
    { A = A 
    ; algebra = record
      { _# = _#
      ; #-Fixpoint = λ {X} {f} → trans #-Fixpoint (∘-resp-≈ˡ ([]-congˡ identityˡ))
      ; #-Uniformity = #-Uniformity
      ; #-Folding = λ {X} {Y} {f} {h} → begin 
      ((f #) +₁ h) #                                                              ≈˘⟨ +-g-η ⟩ 
      [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ]                                     ≈⟨ []-cong₂ left right ⟩ 
      [ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ 
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] #)                                             ∎
      ; #-resp-≈ = #-resp-≈
      }
    }
    where 
    open Guarded-Elgot-Algebra-on gea
    left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (f # +₁ h)# ∘ i₁ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
    left {X} {Y} {f} {h} = begin  
      (f # +₁ h)# ∘ i₁                                     ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩ 
      ([ id , id ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩ 
      [ id , id ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #)          ≈⟨ cancelˡ inject₁ ⟩
      (f #)                                                ≈⟨ #-Uniformity {f = f} 
                                                                             {g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]} 
                                                                             {h = i₁} 
                                                                             (sym inject₁)⟩
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁)                 ∎
    byUni : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]
    byUni {X} {Y} {f} {h} = begin 
      (id +₁ [ i₁ , h ]) 
      ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                 ≈⟨ ∘-resp-≈ʳ (trans ∘[] ([]-congʳ inject₁)) ⟩ 
      (id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f 
      , [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                        ≈⟨ ∘[] ⟩ 
      [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f) 
      , (id +₁ [ i₁ , h ]) ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
      [ ((id +₁ [ i₁ , h ]) ∘ (id +₁ i₁)) ∘ f 
      , ((id +₁ [ i₁ , h ]) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
      [ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
      , [ (id +₁ [ i₁ , h ]) ∘ ((id +₁ i₁) ∘ f) 
      , (id +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ]                    ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) 
                                                                      (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩
      [ (id +₁ i₁) ∘ f 
      , [ ((id +₁ [ i₁ , h ]) ∘ (id +₁ i₁)) ∘ f 
      , ((id +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ] ∘ h ]                    ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
      [ (id +₁ i₁) ∘ f 
      , [ ((id ∘ id) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
      , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ] ∘ h ]                            ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩
      [ (id +₁ i₁) ∘ f 
      , [ (id +₁ i₁) ∘ f 
      , i₂ ∘ ([ i₁ , h ] ∘ i₂) ] ∘ h ]                            ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
      [ (id +₁ i₁) ∘ f , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]        ≈˘⟨ []-congʳ inject₁ ⟩ 
      [ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ 
      , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                         ≈˘⟨ ∘[] ⟩ 
      [ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                    ∎
    right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (f # +₁ h)# ∘ i₂ ≈ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
    right {X} {Y} {f} {h} = begin 
      (f # +₁ h)# ∘ i₂                                     ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
      ([ id , id ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂ ≈⟨ pullʳ +₁∘i₂ ⟩ 
      [ id , id ∘ (((f #) +₁ h) #) ] ∘ i₂ ∘ h              ≈⟨ pullˡ inject₂ ⟩
      (id ∘ (((f #) +₁ h) #)) ∘ h                          ≈⟨ (identityˡ ⟩∘⟨refl) ⟩
      ((f #) +₁ h) # ∘ h                                   ≈˘⟨ #-Uniformity {f = ((f #) +₁ id) ∘ h} 
                                                                              {g = (f #) +₁ h} 
                                                                              {h = h} 
                                                                              (pullˡ (trans (+₁∘+₁) (+₁-cong₂ identityˡ identityʳ)))⟩
      (((f #) +₁ id) ∘ h) #                                ≈⟨ #-Compositionality ⟩ 
      (([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂)  ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} 
                                                                                        {g = [ (id +₁ i₁) ∘ f , i₂ ∘ h ]} 
                                                                                        {h = [ i₁ , h ]} 
                                                                                        byUni)⟩ 
      ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂    ≈⟨ pullʳ inject₂ ⟩ 
      [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h                    ≈˘⟨ inject₂  ⟩∘⟨refl ⟩ 
      ([ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h    ≈˘⟨ pushʳ inject₂  ⟩ 
      [ id , [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] 
      ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)                 ≈˘⟨ []-congˡ identityˡ ⟩∘⟨refl ⟩
      [ id , id ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ] 
      ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)                 ≈˘⟨ pushˡ #-Fixpoint ⟩ 
      [ (id +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂                   ∎


  Unguarded⇒Id-Guarded⇒Unguarded : ∀ (EA : Elgot-Algebra) {X : Obj} (f : X ⇒ Elgot-Algebra.A EA + X) → Elgot-Algebra._# EA f ≈ Elgot-Algebra._# (Id-Guarded⇒Unguarded (Unguarded⇒Id-Guarded EA)) f
  Unguarded⇒Id-Guarded⇒Unguarded EA {X} f = Equiv.refl

  Id-Guarded⇒Unguarded⇒Id-Guarded : ∀ (A : Obj) (EA : Guarded-Elgot-Algebra-on (Id-Algebra A)) {X : Obj} (f : X ⇒ A + X) → Guarded-Elgot-Algebra-on._# EA f ≈ Guarded-Elgot-Algebra-on._# (Unguarded⇒Id-Guarded (Id-Guarded⇒Unguarded EA)) f
  Id-Guarded⇒Unguarded⇒Id-Guarded A EA {X} f = Equiv.refl

  Elgot⇒Uniform : Elgot-Algebra → Uniform-Iteration-Algebra
  Elgot⇒Uniform EA = record 
    { A = A 
    ; algebra = record
      { _# = _# 
      ; #-Fixpoint = #-Fixpoint 
      ; #-Uniformity = #-Uniformity 
      ; #-resp-≈ = #-resp-≈ 
      } 
    }
    where open Elgot-Algebra EA
  
  Diamond-on⇒Elgot-on : ∀ A → Diamond-Elgot-Algebra-on A → Elgot-Algebra-on A
  Diamond-on⇒Elgot-on A DA = algebra
    where 
      open Elgot-Algebra (Id-Guarded⇒Unguarded (Diamond-on⇒Guarded-on A DA))