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.Object.Coproduct using (Coproduct)
open import Categories.Object.Exponential using (Exponential)
open import Categories.Category
open import Categories.Category.Distributive
open import Categories.Object.Exponential

import Categories.Morphism as M
import Categories.Morphism.Reasoning as MR
import Categories.Morphism.Properties as MP

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 import Category.Distributive.Helper distributive
  ccc : CartesianClosed C
  ccc = record { cartesian = cartesian ; exp = exp }
  open CartesianClosed ccc hiding (cartesian; exp)
  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))