open import Level

open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Category
open import Categories.Category.Cartesian
open import Categories.Category.BinaryProducts
open import Categories.Category.Cocartesian
open import Categories.Category.Extensive.Bundle
open import Categories.Category.Extensive
import Categories.Morphism.Reasoning as MR

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

  --*
  -- 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
  --*
  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} 
                                                                          (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₂ #

  --*
  -- 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
    { _# = _#
    ; #-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₂                    ∎