open import Level
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.CartesianClosed using (CartesianClosed)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Object.Terminal using (Terminal)
open import Categories.Object.Product using (Product)
open import Categories.Category.Core

import Categories.Morphism.Reasoning as MR

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 }
    }