Exponentials of Elgot Algebras

module Category.Construction.ElgotAlgebras.Exponentials {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (exp : ∀ {A B} → Exponential C A B) where
  open Category C
  open HomReasoning
  open M C
  open MR C
  open MP C
  open Equiv
  open Distributive distributive
  open import Categories.Category.Distributive.Properties distributive
  ccc : CartesianClosed C
  ccc = record { cartesian = cartesian ; exp = exp }
  open CartesianClosed ccc hiding (cartesian; exp)
  open Cocartesian cocartesian
  open Cartesian cartesian
  open BinaryProducts products renaming (unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′)
  open import Algebra.Elgot cocartesian
  open import Category.Construction.ElgotAlgebras cocartesian
  open import Category.Construction.ElgotAlgebras.Products cocartesian cartesian
  open Elgot-Algebra using (algebra) renaming (A to ∣_∣)
  open Elgot-Algebra-on using (#-Fixpoint; #-Uniformity; #-Folding; #-resp-≈) renaming (_# to [_,_]#)
  
  Exponential-Elgot-Algebra : ∀ {E : Elgot-Algebra} {X : Obj} → Elgot-Algebra

  ∣ Exponential-Elgot-Algebra {E} {X} ∣ = ∣ E ∣ ^ X

  [ algebra (Exponential-Elgot-Algebra {E} {X} ) , f ]# = λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#

  algebra (Exponential-Elgot-Algebra {E} {X}) .#-Fixpoint {Y} {f} = sym (λ-unique′ (begin 
    eval′ ∘ (([ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ f) ⁂ id)                                ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²) ⟩ 
    eval′ ∘ ([ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ⁂ id) ∘ (f ⁂ id)                           ≈⟨ refl⟩∘⟨ pushˡ (⟨⟩-unique proj₁ proj₂) ⟩ 
    eval′ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id)           ≈⟨ pullˡ ∘[] ⟩ 
    [ eval′ ∘ id , eval′ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈⟨ ([]-cong₂ identityʳ β′) ⟩∘⟨refl ⟩ 
    [ eval′ , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ distributeʳ⁻¹ ∘ (f ⁂ id)                          ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ identityʳ) ⟩ 
    [ id , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)             ≈˘⟨ #-Fixpoint (algebra E) ⟩ 
    [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#                                                                 ∎))
    where
    proj₁ : π₁ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈ [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ π₁
    proj₁ = begin 
      π₁ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹        ≈⟨ pullˡ ∘[] ⟩ 
      [ π₁ ∘ id , π₁ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ id-comm project₁) ⟩∘⟨refl ⟩ 
      [ id ∘ π₁ , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ∘ π₁ ] ∘ distributeʳ⁻¹          ≈˘⟨ pullˡ []∘+₁ ⟩ 
      [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ (π₁ +₁ π₁) ∘ distributeʳ⁻¹       ≈⟨ refl⟩∘⟨ distributeʳ⁻¹-π₁ ⟩ 
      [ id , λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ] ∘ π₁                               ∎
    proj₂ : π₂ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹ ≈ id ∘ π₂
    proj₂ = begin 
      π₂ ∘ [ id , (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id ] ∘ distributeʳ⁻¹        ≈⟨ pullˡ ∘[] ⟩ 
      [ π₂ ∘ id , π₂ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#) ⁂ id) ] ∘ distributeʳ⁻¹ ≈⟨ ([]-cong₂ identityʳ (project₂ ○ identityˡ)) ⟩∘⟨refl ⟩ 
      [ π₂ , π₂ ] ∘ distributeʳ⁻¹                                                                              ≈⟨ distributeʳ⁻¹-π₂ ○ sym identityˡ ⟩ 
      id ∘ π₂                                                                                                  ∎

  algebra (Exponential-Elgot-Algebra {E} {X}) .#-Uniformity {B} {D} {f} {g} {h} eq = sym (λ-unique′ (begin 
    eval′ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ∘ h) ⁂ id)      ≈˘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identityʳ) ⟩ 
    eval′ ∘ (λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ⁂ id) ∘ (h ⁂ id) ≈⟨ pullˡ β′ ⟩ 
    [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)]# ∘ (h ⁂ id)                   ≈˘⟨ #-Uniformity (algebra E) by-uni ⟩ 
    [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]#                             ∎))
    where
    by-uni : (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ≈ ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id)
    by-uni = begin 
      (id +₁ (h ⁂ id)) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)   ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
      (eval′ +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)                ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityʳ identityˡ) ⟩ 
      (eval′ +₁ id) ∘ (id +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)   ≈⟨ refl⟩∘⟨ pullˡ ((+₁-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl ○ distributeʳ⁻¹-natural id id h) ⟩
      (eval′ +₁ id) ∘ (distributeʳ⁻¹ ∘ ((id +₁ h) ⁂ id)) ∘ (f ⁂ id) ≈⟨ refl⟩∘⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ eq identity²) ⟩ 
      (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ∘ h ⁂ id)                  ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ 
      ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ∘ (h ⁂ id)         ∎

  algebra (Exponential-Elgot-Algebra {E} {X}) .#-Folding {B} {D} {f} {h} = λ-cong (begin 
    [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ h) ⁂ id) ]#        ≈⟨ #-resp-≈ (algebra E) (refl⟩∘⟨ (sym (distributeʳ⁻¹-natural id (λg ((E Elgot-Algebra.#) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)))) h))) ⟩ 
    [ algebra E , (eval′ +₁ id) ∘ ((λg [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# ⁂ id) +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ]# ≈⟨ #-resp-≈ (algebra E) (pullˡ (+₁∘+₁ ○ +₁-cong₂ β′ identityˡ)) ⟩
    [ algebra E , ([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ (h ⁂ id)) ∘ distributeʳ⁻¹ ]#                           ≈⟨ #-Uniformity (algebra E) by-uni₁ ⟩
    [ algebra E , [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)]# +₁ distributeʳ⁻¹ ∘ (h ⁂ id) ]# ∘ distributeʳ⁻¹              ≈⟨ (#-Folding (algebra E)) ⟩∘⟨refl ⟩
    [ algebra E , [ ((id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id)) , (i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ] ]# ∘ distributeʳ⁻¹     ≈˘⟨ #-Uniformity (algebra E) by-uni₂ ⟩
    [ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ]#                                                ∎)
    where
    by-uni₁ : (id +₁ distributeʳ⁻¹) ∘ ([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ h ⁂ id) ∘ distributeʳ⁻¹ ≈ (([ algebra E , (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) ]# +₁ distributeʳ⁻¹ ∘ (h ⁂ id))) ∘ distributeʳ⁻¹
    by-uni₁ = pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl)
    by-uni₂ : (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id) ≈ [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹
    by-uni₂ = Iso⇒Epi (IsIso.iso isIsoʳ) ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ([ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) (begin 
      ((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ distributeʳ                                                                ≈⟨ ∘[] ⟩ 
      [ (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₁ ⁂ id)) 
      , (((id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ([ (id +₁ i₁) ∘ f , i₂ ∘ h ] ⁂ id)) ∘ (i₂ ⁂ id)) ]                                                            ≈⟨ []-cong₂ (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₁ identity²)))) (pullʳ (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ inject₂ identity²)))) ⟩ 
      [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁) ∘ f) ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((i₂ ∘ h) ⁂ id) ]             ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ refl identity²)) ⟩ 
      [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((id +₁ i₁)) ⁂ id) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (i₂ ⁂ id) ∘ (h ⁂ id) ] ≈⟨ []-cong₂ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (sym (distributeʳ⁻¹-natural id id i₁))) (refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeʳ⁻¹-i₂) ⟩ 
      [ (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id +₁ distributeʳ⁻¹) ∘ (eval′ +₁ id) ∘ i₂ ∘ (h ⁂ id) ]                     ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘+₁) ⟩ 
      [ (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ ((id ⁂ id +₁ i₁ ⁂ id) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (id ∘ eval′ +₁ distributeʳ⁻¹ ∘ id) ∘ i₂ ∘ (h ⁂ id) ]                           ≈⟨ []-cong₂ (pullˡ (pullˡ +₁∘+₁)) (pullˡ +₁∘i₂) ⟩ 
      [ ((((id ∘ eval′) ∘ (id ⁂ id)) +₁ ((distributeʳ⁻¹ ∘ id) ∘ (i₁ ⁂ id))) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , (i₂ ∘ (distributeʳ⁻¹ ∘ id)) ∘ (h ⁂ id) ]                              ≈⟨ []-cong₂ (((+₁-cong₂ (identityˡ ⟩∘⟨refl) (identityʳ ⟩∘⟨refl ○ distributeʳ⁻¹-i₁)) ⟩∘⟨refl) ⟩∘⟨refl) (pullʳ (pullʳ identityˡ)) ⟩ 
      [ (((eval′ ∘ (id ⁂ id)) +₁ i₁) ∘ distributeʳ⁻¹) ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ]                                                                              ≈⟨ []-cong₂ (assoc ○ (+₁-cong₂ (elimʳ (⟨⟩-unique id-comm id-comm)) refl) ⟩∘⟨refl) refl ⟩ 
      [ (eval′ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ]                                                                                              ≈˘⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) refl ⟩ 
      [ (id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ]                                                                                 ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoʳ) ⟩ 
      ([ ( id +₁ i₁) ∘ (eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (f ⁂ id) , i₂ ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ] ∘ distributeʳ⁻¹) ∘ distributeʳ                                                ∎)

  algebra (Exponential-Elgot-Algebra {E} {X}) .#-resp-≈ {Y} {f} {g} eq = λ-cong (#-resp-≈ (algebra E) (refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ eq refl))