open import Level renaming (suc to ℓ-suc)
open import Function using (_$_) renaming (id to idf; _∘_ to _∘ᶠ_)
open import Data.Product using (_,_) renaming (_×_ to _∧_)

open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Object.Product
open import Categories.Object.Coproduct
open import Categories.Category

private
    variable
        o ℓ e : Level


module _ (C𝒞 : CocartesianCategory o ℓ e) where
    open CocartesianCategory C𝒞 renaming (U to 𝒞; id to idC)
    
    --*
    -- F-guarded Elgot Algebra
    --*
    module _ {F : Endofunctor 𝒞} (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 #)

    --*
    -- (unguarded) Elgot-Algebra
    --*
    module _ where
        record Elgot-Algebra : Set (o ⊔ ℓ ⊔ e) where
            -- Object
            field
                A : Obj
            
            -- 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} (
                    begin 
                    ((idC +₁ h) ∘ ((f #) +₁ idC) ∘ h)    ≈⟨ sym-assoc ⟩
                    (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h)  ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ 
                    ((((idC ∘ (f #)) +₁ (h ∘ idC))) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ 
                    ((((f #) +₁ h)) ∘ h)                 ∎)
                ⟩ 
                ((f # +₁ h)# ∘ h) ≈⟨ sym inject₂ ⟩
                (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂))                                     ≈⟨ ∘-resp-≈ˡ (sym $ []∘+₁) ⟩
                (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂)                                  ≈⟨ (sym $ ∘-resp-≈ˡ (#-Fixpoint {f = (f # +₁ h) })) ⟩
                (f # +₁ h)# ∘ i₂                                                               ≈⟨ ∘-resp-≈ˡ #-Folding ⟩
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂)                                          ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩
                ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ assoc ⟩
                [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈⟨ ∘-resp-≈ʳ inject₂ ⟩ 
                [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h)                            ≈⟨ sym-assoc ⟩ 
                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h)                          ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h)                                           ≈⟨ ∘-resp-≈ʳ $ sym (inject₂ {f = i₁} {g = h}) ⟩ 
                [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂)                             ≈⟨ sym-assoc ⟩ 
                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂)                           ≈⟨ sym (∘-resp-≈ˡ (#-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 ]                                                                 ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                                 ≈⟨ ∘-resp-≈ʳ ([]-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ʳ (sym (inject₁)) ⟩ 
                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                         ≈⟨ sym ∘[] ⟩ 
                        [ (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₂ #

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

    private
        -- identity functor on 𝒞
        Id : Functor 𝒞 𝒞
        Id = idF {C = 𝒞}

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

    -- 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} → begin 
                f # ≈⟨ #-Fixpoint ⟩ 
                [ idC , f # ] ∘ f       ≈⟨ sym $ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ 
                [ idC , idC ∘ f # ] ∘ f ∎
        ; #-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
        { _# = _#
        ; #-Fixpoint = λ {X} {f} → begin 
                f # ≈⟨ #-Fixpoint ⟩ 
                [ idC , idC ∘ f # ] ∘ f ≈⟨ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ 
                [ idC , f # ] ∘ f       ∎
        ; #-Uniformity = #-Uniformity
        ; #-Folding = λ {X} {Y} {f} {h} → begin 
            ((f #) +₁ h) #                                                                ≈⟨ sym +-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₁                                         ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
                (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁) ≈⟨ assoc ⟩ 
                ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (((f #) +₁ h) ∘ i₁)) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₁ ⟩
                ([ idC , ((f #) +₁ h) # ] ∘ (i₁ ∘ (f #)))                ≈⟨ sym-assoc ⟩
                (([ idC , ((f #) +₁ h) # ] ∘ i₁) ∘ (f #))                ≈⟨ ∘-resp-≈ˡ inject₁ ⟩
                idC ∘ (f #)                                              ≈⟨ identityˡ ⟩
                (f #)                                                    ≈⟨ #-Uniformity {f = f} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁) ⟩
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁)                    ∎
            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₂)                               ≈⟨ assoc ⟩ 
                ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h) ∘ i₂)                                 ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₂ ⟩ 
                ([ idC , ((f #) +₁ h) # ] ∘ (i₂ ∘ h))                                                  ≈⟨ sym-assoc ⟩ 
                ([ idC , ((f #) +₁ h) # ] ∘ i₂) ∘ h                                                    ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
                ((f #) +₁ h) # ∘ h                                                                     ≈⟨ sym (#-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} (
                    begin 
                        (idC +₁ h) ∘ ((f #) +₁ idC) ∘ h     ≈⟨ sym-assoc ⟩ 
                        (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ 
                        (((idC ∘ (f #)) +₁ (h ∘ idC)) ∘ h)  ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ 
                        (f # +₁ h) ∘ h                      ∎)
                    )⟩ 
                ((((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 ]} (
                    begin 
                        (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                                                                 ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                                 ≈⟨ ∘-resp-≈ʳ ([]-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ʳ (sym (inject₁)) ⟩ 
                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                         ≈⟨ sym ∘[] ⟩ 
                        [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                                                                                        ∎)
                    )⟩ 
                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂)                                   ≈⟨ assoc ⟩ 
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂))                                   ≈⟨ (∘-resp-≈ʳ $ inject₂) ⟩ 
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h)                                                   ≈⟨ sym $ ∘-resp-≈ˡ inject₂ ⟩ 
                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h)                                  ≈⟨ assoc ⟩ 
                ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂ ∘ h)                                    ≈⟨ sym (∘-resp-≈ ([]-congˡ identityˡ) inject₂) ⟩ 
                ([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)) ≈⟨ sym-assoc ⟩ 
                (([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂) ≈⟨ ∘-resp-≈ˡ (sym #-Fixpoint) ⟩ 
                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂)                                                  ∎

    -- unguarded elgot-algebras are just Id-guarded Elgot-Algebras
    Unguarded↔Id-Guarded : ((ea : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A ea))) ∧ (∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra)
    Unguarded↔Id-Guarded = Unguarded→Id-Guarded , Id-Guarded→Unguarded