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
open import Distributive.Core
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
open import Extensive.Bundle
open import Extensive.Core

private
    variable
        o ℓ e : Level


module _ (D : ExtensiveDistributiveCategory o ℓ e) where
    open ExtensiveDistributiveCategory D renaming (U to C; id to idC)
    open Cocartesian cocartesian
    open Cartesian cartesian
    
    --*
    -- F-guarded Elgot Algebra
    --*
    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 #)

    --*
    -- (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 C C
        Id = idF {C = 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