module ElgotAlgebra where

private
  variable
    o ℓ e : Level


module _ (D : ExtensiveDistributiveCategory o ℓ e) where
  open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
  open Cocartesian (Extensive.cocartesian extensive)
  open Cartesian (ExtensiveDistributiveCategory.cartesian D)
  open MR C

  module _ {F : Endofunctor C} (FA : F-Algebra F) where
    record Guarded-Elgot-Algebra : 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 # ≈ [ idC , α ∘ F₁ (f #) ] ∘ f
        #-Uniformity : ∀ {X Y} {f : X ⇒ A + F₀ X} {g : Y ⇒ A + F₀ Y} {h : X ⇒ Y} 
          → (idC +₁ F₁ h) ∘ f ≈ g ∘ h
          → f # ≈ g # ∘ h
        #-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
          → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
        #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} 
          → f ≈ g 
          → (f #) ≈ (g #)

  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 # ≈ [ idC , f # ] ∘ f
      #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} 
        → (idC +₁ h) ∘ f ≈ g ∘ h
        → f # ≈ g # ∘ h
      #-Folding : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
        → ((f #) +₁ h)# ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #
      #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)

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

    -- every elgot-algebra comes with a divergence constant
    !ₑ : ⊥ ⇒ A
    !ₑ = i₂ #
  record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
    field
      A : Obj
      algebra : Elgot-Algebra-on A
    open Elgot-Algebra-on algebra public

  --*
  -- Here follows the proof of equivalence for unguarded and Id-guarded Elgot-Algebras
  --*

  private
    -- identity algebra
    Id-Algebra : Obj → F-Algebra (idF {C = C})
    Id-Algebra A = record
      { A = A
      ; α = idC
      }
     where open Functor (idF {C = C})

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

  -- constructing an unguarded Elgot-Algebra from an Id-Guarded one 
  Id-Guarded→Unguarded : ∀ {A : Obj} → Guarded-Elgot-Algebra (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 ⟩ 
      [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ 
      ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #)                                              ∎
      ; #-resp-≈ = #-resp-≈
      }
    }
    where 
    open Guarded-Elgot-Algebra gea
    open HomReasoning
    open Equiv
    left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
    left {X} {Y} {f} {h} = begin  
      (f # +₁ h)# ∘ i₁                                       ≈⟨ #-Fixpoint ⟩∘⟨refl ⟩ 
      ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩ 
      [ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (i₁ ∘ f #)          ≈⟨ cancelˡ inject₁ ⟩
      (f #)                                                  ≈⟨ #-Uniformity {f = f} 
                                                                             {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} 
                                                                             {h = i₁} 
                                                                             (sym inject₁)⟩
      ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁)                  ∎
    byUni : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]
    byUni {X} {Y} {f} {h} = begin 
      (idC +₁ [ i₁ , h ]) 
      ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                  ≈⟨ ∘-resp-≈ʳ (trans ∘[] ([]-congʳ inject₁)) ⟩ 
      (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f 
      , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                         ≈⟨ ∘[] ⟩ 
      [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) 
      , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
      [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f 
      , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
      [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
      , [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) 
      , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ] ∘ h ]                     ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) 
                                                                      (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩
      [ (idC +₁ i₁) ∘ f 
      , [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f 
      , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ] ∘ h ]                     ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
      [ (idC +₁ i₁) ∘ f 
      , [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f 
      , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ] ∘ h ]                              ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩
      [ (idC +₁ i₁) ∘ f 
      , [ (idC +₁ i₁) ∘ f 
      , i₂ ∘ ([ i₁ , h ] ∘ i₂) ] ∘ h ]                              ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
      [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]        ≈˘⟨ []-congʳ inject₁ ⟩ 
      [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ 
      , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                          ≈˘⟨ ∘[] ⟩ 
      [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                     ∎
    right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
      → (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
    right {X} {Y} {f} {h} = begin 
      (f # +₁ h)# ∘ i₂                                       ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
      ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂ ≈⟨ pullʳ +₁∘i₂ ⟩ 
      [ idC , idC ∘ (((f #) +₁ h) #) ] ∘ i₂ ∘ h              ≈⟨ pullˡ inject₂ ⟩
      (idC ∘ (((f #) +₁ h) #)) ∘ h                           ≈⟨ (identityˡ ⟩∘⟨refl) ⟩
      ((f #) +₁ h) # ∘ h                                     ≈˘⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} 
                                                                              {g = (f #) +₁ h} 
                                                                              {h = h} 
                                                                              (pullˡ (trans (+₁∘+₁) (+₁-cong₂ identityˡ identityʳ)))⟩
      (((f #) +₁ idC) ∘ h) #                                 ≈⟨ #-Compositionality ⟩ 
      (([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂)   ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} 
                                                                                        {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} 
                                                                                        {h = [ i₁ , h ]} 
                                                                                        byUni)⟩ 
      ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂     ≈⟨ pullʳ inject₂ ⟩ 
      [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h                     ≈˘⟨ inject₂  ⟩∘⟨refl ⟩ 
      ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h    ≈˘⟨ pushʳ inject₂  ⟩ 
      [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] 
      ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)                  ≈˘⟨ []-congˡ identityˡ ⟩∘⟨refl ⟩
      [ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] 
      ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)                  ≈˘⟨ pushˡ #-Fixpoint ⟩ 
      [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂                    ∎