open import Level

open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Functor using (Functor) renaming (id to idF)
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Product using (Product)
open import Categories.Object.Coproduct using (Coproduct)
open import Categories.Object.Exponential using (Exponential)
open import Categories.Category
open import ElgotAlgebra
open import Categories.Category.Distributive
open import Categories.Category.Extensive.Bundle
open import Categories.Category.Extensive
import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR

module ElgotAlgebras 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 BinaryProducts products
  open M C
  open MR C
  open HomReasoning
  open Equiv

  --*
  -- let's define the category of elgot-algebras
  --*

  -- iteration preversing morphism between two elgot-algebras
  module _ (E₁ E₂ : Elgot-Algebra D) where
    open Elgot-Algebra E₁ renaming (_# to _#₁)
    open Elgot-Algebra E₂ renaming (_# to _#₂; A to B)
    record Elgot-Algebra-Morphism : Set (o ⊔ ℓ ⊔ e) where
      field
        h : A ⇒ B
        preserves : ∀ {X} {f : X ⇒ A + X} → h ∘ (f #₁) ≈ ((h +₁ idC) ∘ f)#₂

  -- the category of elgot algebras for a given category
  Elgot-Algebras : Category (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e) e
  Elgot-Algebras = record
    { Obj       = Elgot-Algebra D
    ; _⇒_       = Elgot-Algebra-Morphism
    ; _≈_       = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
    ; id        = λ {EB} → let open Elgot-Algebra EB in 
    record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin
      idC ∘ f #            ≈⟨ identityˡ ⟩ 
      f #                  ≈⟨ #-resp-≈ (introˡ (coproduct.unique id-comm-sym id-comm-sym)) ⟩
      ((idC +₁ idC) ∘ f) # ∎ }
    ; _∘_       = λ {EA} {EB} {EC} f g → let 
      open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
      open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
      open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ)
      open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B)
      open Elgot-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈)
      in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin 
        (hᶠ ∘ hᵍ) ∘ (f #ᵃ)                     ≈⟨ pullʳ preservesᵍ ⟩
        (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ))          ≈⟨ preservesᶠ ⟩ 
        (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ)   ≈⟨ #ᶜ-resp-≈ (pullˡ (trans +₁∘+₁ (+₁-cong₂ refl (identity²)))) ⟩ 
        ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ              ∎ }
    ; identityˡ = identityˡ
    ; identityʳ = identityʳ
    ; identity² = identity²
    ; assoc     = assoc
    ; sym-assoc = sym-assoc
    ; equiv     = record
      { refl  = refl
      ; sym   = sym
      ; trans = trans
      }
    ; ∘-resp-≈  = ∘-resp-≈
    }
    where open Elgot-Algebra-Morphism

  --*
  -- products and exponentials of elgot-algebras
  --*

  -- if the carrier contains a terminal, so does elgot-algebras
  Terminal-Elgot-Algebras : Terminal C → Terminal Elgot-Algebras
  Terminal-Elgot-Algebras T = record 
    { ⊤ = record
      { A = ⊤
      ; _# = λ x → !
      ; #-Fixpoint = λ {_ f} → !-unique ([ idC , ! ] ∘ f)
      ; #-Uniformity = λ {_ _ _ _ h} _ → !-unique (! ∘ h)
      ; #-Folding = refl
      ; #-resp-≈ = λ _ → refl
      } 
    ; ⊤-is-terminal = record 
      { ! = λ {A} → record { h = ! ; preserves = λ {X} {f} → sym (!-unique (! ∘ (A Elgot-Algebra.#) f))   } 
      ; !-unique = λ {A} f → !-unique (Elgot-Algebra-Morphism.h f) 
      } 
    }
    where 
    open Terminal T

  -- if the carriers of the algebra form a product, so do the algebras
  A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Elgot-Algebra D
  A×B-Helper {EA} {EB}  = record
    { A = A × B
    ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
    ; #-Fixpoint = λ {X} {f} → begin
      ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
      ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
      ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈˘⟨ ⟨⟩∘ ⟩
      (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (unique′ 
        (begin 
          π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ 
          [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
          [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
          π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎) 
        (begin 
          π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ 
          [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
          [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
          π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎)
      )⟩
      ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
    ; #-Uniformity = λ {X Y f g h} uni → unique′ 
      (begin 
        π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
          (((π₁ +₁ idC) ∘ f)#ᵃ)                            ≈⟨ #ᵃ-Uniformity 
            (begin 
            -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
              (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f                     ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩ 
              (π₁ ∘ idC +₁ idC ∘ h) ∘ f                        ≈˘⟨ pullˡ +₁∘+₁ ⟩
              (π₁ +₁ idC) ∘ (idC +₁ h) ∘ f                     ≈⟨ pushʳ uni ⟩
              ((π₁ +₁ idC) ∘ g) ∘ h                            ∎)⟩
      (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h)                                  ≈˘⟨ pullˡ project₁ ⟩
        π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎) 
      (begin 
        π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ 
        ((π₂ +₁ idC) ∘ f)#ᵇ                                ≈⟨ #ᵇ-Uniformity 
          (begin 
            (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f   ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
            ((π₂ ∘ idC +₁ idC ∘ h) ∘ f)    ≈˘⟨ pullˡ +₁∘+₁ ⟩
            (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
            ((π₂ +₁ idC) ∘ g) ∘ h          ∎)⟩
        ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h                                    ≈˘⟨ pullˡ project₂ ⟩
        π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎)
    ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
    ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
    }
    where 
    open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
    open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
    +₁-id-swap : ∀ {X Y C} {f : X ⇒ (A × B) + X} {h : Y ⇒ X + Y} (π : A × B ⇒ C) → [ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] ≈ (π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]
    +₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (idC +₁ i₁) ∘ ((π +₁ idC) ∘ f) , i₂ ∘ h ] )                      ≈⟨ ([]-congʳ sym-assoc) ⟩ 
      ([ ((idC +₁ i₁) ∘ (π +₁ idC)) ∘ f , i₂ ∘ h ] )                      ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩ 
      (([ (π ∘ idC +₁ idC ∘ i₁) ∘ f ,  (i₂ ∘ idC) ∘ h ]))                 ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩ 
      (([ (π +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π +₁ idC) ∘ i₂ ∘ h ]))          ≈˘⟨ ∘[] ⟩ 
      ((π +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])                         ∎
    foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
    foldingˡ {X} {Y} {f} {h} = begin 
      ((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩ 
      ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ)                                         ≈⟨ #ᵃ-Folding ⟩ 
      ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
      ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ                         ∎
    foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
    foldingʳ {X} {Y} {f} {h} = begin
      ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
      ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ)                                         ≈⟨ #ᵇ-Folding ⟩
      [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ                        ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
      ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ                         ∎

  Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product Elgot-Algebras EA EB
  Product-Elgot-Algebras EA EB = record
    { A×B = A×B-Helper {EA} {EB}
    ; π₁ = record { h = π₁ ; preserves = λ {X} {f} → project₁ }
    ; π₂ = record { h = π₂ ; preserves = λ {X} {f} → project₂ }
    ; ⟨_,_⟩ = λ {E} f g → let 
      open Elgot-Algebra-Morphism f renaming (h to f′; preserves to preservesᶠ)
      open Elgot-Algebra-Morphism g renaming (h to g′; preserves to preservesᵍ)
      open Elgot-Algebra E renaming (_# to _#ᵉ) in record { h = ⟨ f′ , g′ ⟩ ; preserves = λ {X} {h} → 
      begin 
        ⟨ f′ , g′ ⟩ ∘ (h #ᵉ)                                                                              ≈⟨ ⟨⟩∘ ⟩ 
        ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩                                                                     ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
        ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩                                                   ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩
        ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩           ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩
        ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩     ∎ }
    ; project₁ = project₁
    ; project₂ = project₂
    ; unique = unique
    }
    where
    open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
    open Elgot-Algebra EB using () renaming (A to B; _# to _#ᵇ; #-Fixpoint to #ᵇ-Fixpoint; #-Uniformity to #ᵇ-Uniformity; #-Folding to #ᵇ-Folding; #-resp-≈ to #ᵇ-resp-≈)
    open Elgot-Algebra (A×B-Helper {EA} {EB}) using () renaming (_# to _#ᵖ) 


  -- if the carrier is cartesian, so is the category of algebras
  Cartesian-Elgot-Algebras : Cartesian Elgot-Algebras
  Cartesian-Elgot-Algebras = record 
    { terminal = Terminal-Elgot-Algebras terminal
    ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
    }

  -- if the carriers of the algebra form a exponential, so do the algebras
  B^A-Helper : ∀ {EA : Elgot-Algebra D} {X : Obj} → Exponential C X (Elgot-Algebra.A EA) → Elgot-Algebra D
  B^A-Helper {EA} {X} exp = record
    { A = A^X
    ; _# = λ {Z} f → λg product (((((eval +₁ idC) ∘ (Categories.Object.Product.repack C product product' +₁ idC)) ∘ dstl) ∘ (f ⁂ idC)) #ᵃ)
    ; #-Fixpoint = λ {X} {f} → {!   !}
    ; #-Uniformity = {!   !}
    ; #-Folding = {!   !}
    ; #-resp-≈ = {!   !}
    }
    where
    open Exponential exp renaming (B^A to A^X; product to product')
    open Elgot-Algebra EA using (A) renaming (_# to _#ᵃ; #-Fixpoint to #ᵃ-Fixpoint; #-Uniformity to #ᵃ-Uniformity; #-Folding to #ᵃ-Folding; #-resp-≈ to #ᵃ-resp-≈)
    dstr = λ {X Y Z} → IsIso.inv (isIsoˡ {X} {Y} {Z})
    dstl = λ {X Y Z} → IsIso.inv (isIsoʳ {X} {Y} {Z})