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
open import Categories.Category.Cocartesian.Bundle
open import Categories.Category.Cartesian
open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra
open import Categories.Object.Terminal
open import Categories.Object.Product
open import Categories.Object.Exponential
open import Categories.Object.Coproduct
open import Categories.Category.BinaryProducts
open import Categories.Category
open import ElgotAlgebra
open import Distributive.Bundle
open import Distributive.Core

module ElgotAlgebras where

private
    variable
        o ℓ e : Level

module _ (D : DistributiveCategory o ℓ e) where
    open DistributiveCategory D renaming (U to C; id to idC)
    open Cocartesian cocartesian

    CC : CocartesianCategory o ℓ e
    CC = record
        { U = C
        ; cocartesian = cocartesian
        }

    --*
    -- 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 (cocartesian-)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 #)                                 ≈⟨ sym $ #-resp-≈ identityˡ ⟩ 
                            ((idC ∘ f) #)                         ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ 
                            (([ i₁ , i₂ ] ∘ f)#)                  ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ ([]-cong₂ identityʳ identityʳ)) ⟩ 
                            (([ i₁ ∘ idC , i₂ ∘ idC ] ∘ f)#)      ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ []∘+₁) ⟩ 
                            ((([ i₁ , i₂ ] ∘ (idC +₁ idC)) ∘ f)#) ≈⟨ #-resp-≈ assoc ⟩ 
                            (([ i₁ , i₂ ] ∘ (idC +₁ idC) ∘ f)#)   ≈⟨ #-resp-≈ (∘-resp-≈ˡ +-η) ⟩
                            ((idC ∘ (idC +₁ idC) ∘ f)#)           ≈⟨ #-resp-≈ identityˡ ⟩ 
                            ((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 #ᵃ)                     ≈⟨ assoc ⟩
                            (hᶠ ∘ hᵍ ∘ (f #ᵃ))                     ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩ 
                            (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ))          ≈⟨ preservesᶠ ⟩ 
                            (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ)   ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ 
                            ((((hᶠ +₁ idC) ∘ (hᵍ +₁ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ +₁∘+₁) ⟩ 
                            ((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ)  ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-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
            open HomReasoning
            open Equiv

    --*
    -- 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
            open Equiv

    -- if the carriers of the algebra form a product, so do the algebras
    A×B-Helper : ∀ {EA EB : Elgot-Algebra D} → Product C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra D
    A×B-Helper {EA} {EB} p = 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₂ sym-assoc sym-assoc ⟩
            ⟨ ([ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ (π₁ +₁ idC)) ∘ f , ([ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ (π₂ +₁ idC)) ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ˡ []∘+₁) (∘-resp-≈ˡ []∘+₁) ⟩
            ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈⟨ sym ∘-distribʳ-⟨⟩ ⟩
            (⟨ [ 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₂ identityˡ identityʳ ⟩
                    [ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ]                                                                 ≈⟨ sym ([]-cong₂ identityʳ project₁) ⟩
                    [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈⟨ sym ∘[] ⟩
                    π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎) 
                (begin 
                    π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ 
                    [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ]                                                     ≈⟨ []-cong₂ identityˡ identityʳ ⟩
                    [ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ]                                                                 ≈⟨ sym ([]-cong₂ identityʳ project₂) ⟩
                    [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈⟨ sym ∘[] ⟩
                    π₂ ∘ [ 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 
                        (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f   ≈⟨ sym-assoc ⟩ 
                        ((idC +₁ h) ∘ (π₁ +₁ idC)) ∘ f ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩
                        (idC ∘ π₁ +₁ h ∘ idC) ∘ f      ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
                        ((π₁ +₁ h) ∘ f)                ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
                        (((π₁ ∘ idC +₁ idC ∘ h)) ∘ f)  ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
                        ((π₁ +₁ idC) ∘ (idC +₁ h)) ∘ f ≈⟨ assoc ⟩
                        (π₁ +₁ idC) ∘ ((idC +₁ h) ∘ f) ≈⟨ ∘-resp-≈ʳ uni ⟩
                        (π₁ +₁ idC) ∘ g ∘ h            ≈⟨ sym-assoc ⟩
                        ((π₁ +₁ idC) ∘ g) ∘ h          ∎
                    )⟩
                (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h)                                  ≈⟨ sym (∘-resp-≈ˡ project₁) ⟩
                ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩
                π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎
            ) (
            begin 
                π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩         ≈⟨ project₂ ⟩ 
                ((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity (
                    begin 
                        (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f     ≈⟨ sym-assoc ⟩
                        (((idC +₁ h) ∘ (π₂ +₁ idC)) ∘ f) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩
                        ((idC ∘ π₂ +₁ h ∘ idC) ∘ f)      ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
                        ((π₂ +₁ h) ∘ f)                  ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
                        ((((π₂ ∘ idC +₁ idC ∘ h)) ∘ f))  ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
                        ((π₂ +₁ idC) ∘ ((idC +₁ h))) ∘ f ≈⟨ assoc ⟩
                        (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f   ≈⟨ ∘-resp-≈ʳ uni ⟩
                        (π₂ +₁ idC) ∘ g ∘ h              ≈⟨ sym-assoc ⟩
                        ((π₂ +₁ idC) ∘ g) ∘ h            ∎
                    )⟩
                ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈⟨ sym (∘-resp-≈ˡ project₂) ⟩
                ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩
                π₂ ∘ ⟨ ((π₁ +₁ 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-≈)
            open Product C p
            open HomReasoning
            open Equiv
            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-≈ +₁∘+₁ ⟩ 
                ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ)    ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩ 
                ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ)                                         ≈⟨ #ᵃ-Folding ⟩ 
                ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩ 
                ([ ((idC +₁ i₁) ∘ (π₁ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩ 
                ([ ((idC ∘ π₁ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵃ)                         ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩ 
                ([ ((π₁ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵃ)                                     ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩ 
                (([ (π₁ ∘ idC +₁ idC ∘ i₁) ∘ f ,  (i₂ ∘ idC) ∘ h ])#ᵃ)                 ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩ 
                (([ ((π₁ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₁ +₁ idC) ∘ i₂) ∘ h ])#ᵃ)     ≈⟨ #ᵃ-resp-≈ ([]-cong₂ assoc assoc) ⟩ 
                (([ (π₁ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₁ +₁ idC) ∘ i₂ ∘ h ])#ᵃ)         ≈⟨ sym (#ᵃ-resp-≈ ∘[]) ⟩ 
                ((π₁ +₁ 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-≈ +₁∘+₁ ⟩
                ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ)    ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩
                ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ)                                         ≈⟨ #ᵇ-Folding ⟩
                [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ                        ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩
                ([ ((idC +₁ i₁) ∘ (π₂ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵇ)                      ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩
                ([ ((idC ∘ π₂ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵇ)                         ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩
                ([ ((π₂ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵇ)                                     ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩
                (([ (π₂ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵇ)                  ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩
                (([ ((π₂ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₂ +₁ idC) ∘ i₂) ∘ h ])#ᵇ)     ≈⟨ #ᵇ-resp-≈ ([]-cong₂ assoc assoc) ⟩
                (([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ)         ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩
                ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ                         ∎

    Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra D) → Product C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Product Elgot-Algebras EA EB
    Product-Elgot-Algebras EA EB p = record
        { A×B = A×B-Helper {EA} {EB} p
        ; π₁ = 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 #ᵉ)                                                                              ≈⟨ ∘-distribʳ-⟨⟩ ⟩ 
                    ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩                                                                     ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
                    ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩                                                   ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²)))) ⟩
                    ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩           ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ +₁∘+₁)) (#ᵇ-resp-≈ (∘-resp-≈ˡ +₁∘+₁))) ⟩
                    ⟨ (((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵃ , (((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵇ ⟩ ≈⟨ (⟨⟩-cong₂ (#ᵃ-resp-≈ assoc) (#ᵇ-resp-≈ assoc)) ⟩
                    ⟨ ((π₁ +₁ 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} p) using () renaming (_# to _#ᵖ) 
            open Product C p
            open HomReasoning
            open Equiv
    

    -- if the carrier is cartesian, so is the category of algebras
    Cartesian-Elgot-Algebras : Cartesian C → Cartesian Elgot-Algebras
    Cartesian-Elgot-Algebras CaC = record { 
        terminal = Terminal-Elgot-Algebras terminal;
        products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB product }
        }
        where 
            open Cartesian CaC using (terminal; products)
            open BinaryProducts products using (product)
            open Equiv

    -- if the carriers of the algebra form a exponential, so do the algebras
    B^A-Helper : ∀ {EA EB : Elgot-Algebra D} → Exponential C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Elgot-Algebra D
    B^A-Helper {EA} {EB} e = record
        { A = B^A
        ; _# = λ {X} f → λg {!   !} {!   !}
        ; #-Fixpoint = {!   !}
        ; #-Uniformity = {!   !}
        ; #-Folding = {!   !}
        ; #-resp-≈ = {!   !}
        }
        where
            open Exponential e