The Category of Elgot Algebras on C is Cartesian if C is Cartesian

module Category.Construction.ElgotAlgebras.Products {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) (cartesian : Cartesian C) where
  open Category C
  open Equiv
  open HomReasoning
  open MR C
  open import Category.Construction.ElgotAlgebras cocartesian
  open Cartesian cartesian
  open Cocartesian cocartesian
  open import Algebra.Elgot cocartesian
  open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)

  -- if the carrier contains a terminal, so does elgot-algebras
  Terminal-Elgot-Algebras : Terminal Elgot-Algebras
  Terminal-Elgot-Algebras = record 
    { ⊤ = record
      { A = ⊤
      ; algebra = record
        { _# = λ x → !
        ; #-Fixpoint = λ {_ f} → !-unique ([ id , ! ] ∘ 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 terminal

  -- the product of the carrier of two elgot algebras is again an elgot algebra
  Product-Elgot-Algebra : ∀ {EA EB : Elgot-Algebra} → Elgot-Algebra
  Product-Elgot-Algebra {EA} {EB}  = record
    { A = A × B
    ; algebra = record
      { _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
      ; #-Fixpoint = λ {X} {f} → begin
        ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
        ⟨ [ id , ((π₁ +₁ id) ∘ f)#ᵃ ] ∘ ((π₁ +₁ id) ∘ f) , [ id , ((π₂ +₁ id) ∘ f)#ᵇ ] ∘ ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ (pullˡ []∘+₁) (pullˡ []∘+₁) ⟩
        ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] ∘ f , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ∘ f ⟩           ≈˘⟨ ⟨⟩∘ ⟩
        (⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (⟨⟩-unique′ 
          (begin 
            π₁ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₁ ⟩ 
            [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₁)) ⟩
            [ π₁ ∘ id , π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
            π₁ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ]                                 ∎) 
          (begin 
            π₂ ∘ ⟨ [ id ∘ π₁ , ((π₁ +₁ id) ∘ f)#ᵃ ∘ id ] , [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ] ⟩ ≈⟨ project₂ ⟩ 
            [ id ∘ π₂ , ((π₂ +₁ id) ∘ f)#ᵇ ∘ id ]                                                     ≈⟨ []-cong₂ id-comm-sym (trans identityʳ (sym project₂)) ⟩
            [ π₂ ∘ id , π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ]                            ≈˘⟨ ∘[] ⟩
            π₂ ∘ [ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ]                                 ∎)
        )⟩
        ([ id , ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
      ; #-Uniformity = λ {X Y f g h} uni → ⟨⟩-unique′ 
        (begin 
          π₁ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
            (((π₁ +₁ id) ∘ f)#ᵃ)                            ≈⟨ #ᵃ-Uniformity 
              (begin 
              -- TODO factor these out or adjust +₁ swap... maybe call it +₁-id-comm
                (id +₁ h) ∘ (π₁ +₁ id) ∘ f                     ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm)) ⟩ 
                (π₁ ∘ id +₁ id ∘ h) ∘ f                        ≈˘⟨ pullˡ +₁∘+₁ ⟩
                (π₁ +₁ id) ∘ (id +₁ h) ∘ f                     ≈⟨ pushʳ uni ⟩
                ((π₁ +₁ id) ∘ g) ∘ h                            ∎)⟩
        (((π₁ +₁ id) ∘ g)#ᵃ ∘ h)                                  ≈˘⟨ pullˡ project₁ ⟩
          π₁ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ g)#ᵇ ⟩ ∘ h     ∎) 
        (begin 
          π₂ ∘ ⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ 
          ((π₂ +₁ id) ∘ f)#ᵇ                                ≈⟨ #ᵇ-Uniformity 
            (begin 
              (id +₁ h) ∘ (π₂ +₁ id) ∘ f   ≈⟨ pullˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))⟩
              ((π₂ ∘ id +₁ id ∘ h) ∘ f)    ≈˘⟨ pullˡ +₁∘+₁ ⟩
              (π₂ +₁ id) ∘ ((id +₁ h)) ∘ f ≈⟨ pushʳ uni ⟩
              ((π₂ +₁ id) ∘ g) ∘ h          ∎)⟩
          ((π₂ +₁ id) ∘ g)#ᵇ ∘ h                                    ≈˘⟨ pullˡ project₂ ⟩
          π₂ ∘ ⟨ ((π₁ +₁ id) ∘ g)#ᵃ , ((π₂ +₁ id) ∘ 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) → [ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] ≈ (π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ]
    +₁-id-swap {X} {Y} {C} {f} {h} π = begin ([ (id +₁ i₁) ∘ ((π +₁ id) ∘ f) , i₂ ∘ h ] )                      ≈⟨ ([]-congʳ sym-assoc) ⟩ 
      ([ ((id +₁ i₁) ∘ (π +₁ id)) ∘ f , i₂ ∘ h ] )                      ≈⟨ []-cong₂ (∘-resp-≈ˡ (trans +₁∘+₁ (+₁-cong₂ id-comm-sym id-comm))) (∘-resp-≈ˡ (sym identityʳ)) ⟩ 
      (([ (π ∘ id +₁ id ∘ i₁) ∘ f ,  (i₂ ∘ id) ∘ h ]))                 ≈˘⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩ 
      (([ (π +₁ id) ∘ (id +₁ i₁) ∘ f , (π +₁ id) ∘ i₂ ∘ h ]))          ≈˘⟨ ∘[] ⟩ 
      ((π +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])                         ∎
    foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
    foldingˡ {X} {Y} {f} {h} = begin 
      ((π₁ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₁ identityˡ)) ⟩ 
      ((((π₁ +₁ id) ∘ f)#ᵃ +₁ h)#ᵃ)                                         ≈⟨ #ᵃ-Folding ⟩ 
      ([ (id +₁ i₁) ∘ ((π₁ +₁ id) ∘ f) , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ (+₁-id-swap π₁)⟩
      ((π₁ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ                         ∎
    foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
    foldingʳ {X} {Y} {f} {h} = begin
      ((π₂ +₁ id) ∘ (⟨ ((π₁ +₁ id) ∘ f)#ᵃ , ((π₂ +₁ id) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ (trans +₁∘+₁ (+₁-cong₂ project₂ identityˡ)) ⟩
      ((((π₂ +₁ id) ∘ f)#ᵇ +₁ h)#ᵇ)                                         ≈⟨ #ᵇ-Folding ⟩
      [ (id +₁ i₁) ∘ ((π₂ +₁ id) ∘ f) , i₂ ∘ h ] #ᵇ                        ≈⟨ #ᵇ-resp-≈ (+₁-id-swap π₂) ⟩
      ((π₂ +₁ id) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ                         ∎

  Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Product Elgot-Algebras EA EB
  Product-Elgot-Algebras EA EB = record
    { A×B = Product-Elgot-Algebra {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′ +₁ id) ∘ h) #ᵃ , ((g′ +₁ id) ∘ h) #ᵇ ⟩                                                   ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²))) ⟩
        ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ id ∘ id) ∘ h) #ᵇ ⟩           ≈˘⟨ ⟨⟩-cong₂ (#ᵃ-resp-≈ (pullˡ +₁∘+₁)) (#ᵇ-resp-≈ (pullˡ +₁∘+₁)) ⟩
        ⟨ ((π₁ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ h) #ᵃ , ((π₂ +₁ id) ∘ (⟨ f′ , g′ ⟩ +₁ id) ∘ 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 (Product-Elgot-Algebra {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
    ; products = record { product = λ {EA EB} → Product-Elgot-Algebras EA EB }
    }