open import Level
open import Categories.FreeObjects.Free
open import Categories.Functor.Core
open import Categories.Functor.Algebra
open import Categories.Functor.Coalgebra
open import Categories.Object.Terminal
open import Categories.Category.Core using (Category)
open import Categories.Category.Distributive using (Distributive)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cartesian using (Cartesian)
open import Categories.Category.BinaryProducts using (BinaryProducts)
open import Categories.Category.Construction.EilenbergMoore
open import Categories.Monad.Relative renaming (Monad to RMonad)

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

module Algebra.Elgot.Stable {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Distributive distributive
  open import Categories.Category.Distributive.Properties distributive
  open import Algebra.Elgot cocartesian
  open import Category.Construction.ElgotAlgebras cocartesian
  open import Categories.Morphism.Properties C

  open Category C
  open Cocartesian cocartesian
  open Cartesian cartesian
  open BinaryProducts products hiding (η)
  open import Algebra.Elgot.Free cocartesian
  open Equiv
  open HomReasoning
  open MR C
  open M C

  record IsStableFreeElgotAlgebraˡ {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
    open FreeObject freeElgot using (η) renaming (FX to FY)
    open Elgot-Algebra FY using (_#)

    field
      [_,_]♯ˡ : ∀ {X : Obj} (A : Elgot-Algebra) (f : Y × X ⇒ Elgot-Algebra.A A) → Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A A
      ♯ˡ-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ˡ ∘ (η ⁂ id)
      ♯ˡ-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ˡ ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B (([ B , f ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id))
      ♯ˡ-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : Y × X ⇒ Elgot-Algebra.A B) (g : Elgot-Algebra.A FY × X ⇒ Elgot-Algebra.A B)
        → f ≈ g ∘ (η ⁂ id)
        → ({Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (h # ⁂ id) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)))
        → g ≈ [ B , f ]♯ˡ

  record IsStableFreeElgotAlgebra {Y : Obj} (freeElgot : FreeElgotAlgebra Y) : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
    open FreeObject freeElgot using (η) renaming (FX to FY)
    open Elgot-Algebra FY using (_#)

    field
        [_,_]♯ : ∀ {X : Obj} (A : Elgot-Algebra) (f : X × Y ⇒ Elgot-Algebra.A A) → X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A A
        ♯-law : ∀ {X : Obj} {A : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A A) → f ≈ [ A , f ]♯ ∘ (id ⁂ η)
        ♯-preserving : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → [ B , f ]♯ ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B (([ B , f ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h))
        ♯-unique : ∀ {X : Obj} {B : Elgot-Algebra} (f : X × Y ⇒ Elgot-Algebra.A B) (g : X × Elgot-Algebra.A FY ⇒ Elgot-Algebra.A B)
          → f ≈ g ∘ (id ⁂ η)
          → (∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → g ∘ (id ⁂ h #) ≈ Elgot-Algebra._# B ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)))
          → g ≈ [ B , f ]♯

  isStable⇒isStableˡ : ∀ {Y} (freeElgot : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebra {Y} freeElgot → IsStableFreeElgotAlgebraˡ {Y} freeElgot

  IsStableFreeElgotAlgebraˡ.[_,_]♯ˡ (isStable⇒isStableˡ {Y} fe isStable) {X} A f = [ A , (f ∘ swap) ]♯ ∘ swap 
    where open IsStableFreeElgotAlgebra isStable

  IsStableFreeElgotAlgebraˡ.♯ˡ-law (isStable⇒isStableˡ {Y} fe isStable) {X} {A} f = begin 
    f ≈⟨ introʳ swap∘swap ⟩ 
    f ∘ swap ∘ swap ≈⟨ pullˡ (♯-law (f ∘ swap)) ⟩ 
    ([ A , f ∘ swap ]♯ ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ 
    [ A , (f ∘ swap) ]♯ ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩ 
    ([ A , (f ∘ swap) ]♯ ∘ swap) ∘ (η ⁂ id) ∎
    where
      open IsStableFreeElgotAlgebra isStable
      open FreeObject fe using (η) renaming (FX to FY)

  IsStableFreeElgotAlgebraˡ.♯ˡ-preserving (isStable⇒isStableˡ {Y} fe isStable) {X} {B} f {Z} h = begin 
    ([ B , (f ∘ swap) ]♯ ∘ swap) ∘ ((h #) ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ 
    [ B , (f ∘ swap) ]♯ ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (♯-preserving (f ∘ swap) h) ⟩ 
    (([ B , (f ∘ swap) ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ 
    ((([ B , (f ∘ swap) ]♯ ∘ swap) +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎
    where 
      open IsStableFreeElgotAlgebra isStable
      open FreeObject fe using (η) renaming (FX to FY)
      open Elgot-Algebra FY using (_#)
      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
      uni-helper : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ (([ B , f ∘ swap ]♯ coproducts.+₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap
      uni-helper = begin 
        (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullˡ +₁∘+₁ ⟩ 
        (id ∘ [ B , f ∘ swap ]♯ ∘ swap +₁ swap ∘ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
        ([ B , f ∘ swap ]♯ ∘ swap +₁ id ∘ swap) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
        (([ B , f ∘ swap ]♯ +₁ id) ∘ (swap +₁ swap)) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ⟩
        ([ B , f ∘ swap ]♯ +₁ id) ∘ (distributeˡ⁻¹ ∘ swap) ∘ (h ⁂ id) ≈⟨ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc ⟩ 
        (([ B , f ∘ swap ]♯ +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap ∎

  IsStableFreeElgotAlgebraˡ.♯ˡ-unique (isStable⇒isStableˡ {Y} fe isStable) {X} {B} f g g-law g-preserving = begin 
    g ≈⟨ introʳ swap∘swap ⟩ 
    g ∘ swap ∘ swap ≈⟨ pullˡ (♯-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩ 
    [ B , (f ∘ swap) ]♯ ∘ swap ∎
    where 
      open IsStableFreeElgotAlgebra isStable
      open FreeObject fe using (η) renaming (FX to FY)
      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
      open Elgot-Algebra FY using (_#)
      helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (id ⁂ η)
      helper₁ = begin 
        f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ 
        (g ∘ (η ⁂ id)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ 
        g ∘ swap ∘ (id ⁂ η) ≈⟨ sym-assoc ⟩ 
        (g ∘ swap) ∘ (id ⁂ η) ∎
      helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (id ⁂ h #) ≈ ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ
      helper₂ {Z} h = begin 
        (g ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ 
        g ∘ (h # ⁂ id) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ 
        ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ 
        ((g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∎
        where
          uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ ((g +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap
          uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc

  isStableˡ⇒isStable : ∀ {Y} (freeElgot : FreeElgotAlgebra Y) → IsStableFreeElgotAlgebraˡ {Y} freeElgot → IsStableFreeElgotAlgebra {Y} freeElgot

  IsStableFreeElgotAlgebra.[_,_]♯ (isStableˡ⇒isStable {Y} fe isStableˡ) {X} A f = [ A , f ∘ swap ]♯ˡ ∘ swap
    where open IsStableFreeElgotAlgebraˡ isStableˡ

  IsStableFreeElgotAlgebra.♯-law (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {A} f = begin 
    f ≈⟨ introʳ swap∘swap ⟩ 
    f ∘ swap ∘ swap ≈⟨ pullˡ (♯ˡ-law (f ∘ swap)) ⟩ 
    ([ A , f ∘ swap ]♯ˡ ∘ (η ⁂ id)) ∘ swap ≈⟨ (pullʳ (sym swap∘⁂)) ○ sym-assoc ⟩ 
    ([ A , (f ∘ swap) ]♯ˡ ∘ swap) ∘ (id ⁂ η) ∎
    where 
      open IsStableFreeElgotAlgebraˡ isStableˡ
      open FreeObject fe using (η) renaming (FX to FY)

  IsStableFreeElgotAlgebra.♯-preserving (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {B} f {Z} h = begin 
    ([ B , (f ∘ swap) ]♯ˡ ∘ swap) ∘ (id ⁂ h #) ≈⟨ pullʳ swap∘⁂ ⟩ 
    [ B , (f ∘ swap) ]♯ˡ ∘ ((h #) ⁂ id) ∘ swap ≈⟨ pullˡ (♯ˡ-preserving (f ∘ swap) h) ⟩ 
    (([ B , (f ∘ swap) ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∘ swap ≈˘⟨ #ᵇ-Uniformity by-uni ⟩ 
    (((([ B , (f ∘ swap) ]♯ˡ ∘ swap) +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ) ∎
    where 
      open IsStableFreeElgotAlgebraˡ isStableˡ
      open FreeObject fe using (η) renaming (FX to FY)
      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
      open Elgot-Algebra FY using (_#)
      by-uni : (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈ (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap
      by-uni = begin 
        (id +₁ swap) ∘ ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩ 
        (id ∘ [ B , f ∘ swap ]♯ˡ ∘ swap +₁ swap ∘ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩ 
        ([ B , f ∘ swap ]♯ˡ ∘ swap +₁ id ∘ swap) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩ 
        (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ (swap +₁ swap)) ∘ distributeˡ⁻¹ ∘ (id ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeʳ⁻¹∘swap)) ⟩
        ([ B , f ∘ swap ]♯ˡ +₁ id) ∘ (distributeʳ⁻¹ ∘ swap) ∘ (id ⁂ h) ≈⟨ refl⟩∘⟨ (pullʳ swap∘⁂) ⟩ 
        ([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ∘ swap ≈˘⟨ assoc ○ refl⟩∘⟨ assoc ⟩ 
        (([ B , f ∘ swap ]♯ˡ +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) ∘ swap ∎

  IsStableFreeElgotAlgebra.♯-unique (isStableˡ⇒isStable {Y} fe isStableˡ) {X} {B} f g g-law g-preserving = begin 
    g ≈⟨ introʳ swap∘swap ⟩ 
    g ∘ swap ∘ swap ≈⟨ pullˡ (♯ˡ-unique (f ∘ swap) (g ∘ swap) helper₁ helper₂) ⟩ 
    [ B , f ∘ swap ]♯ˡ ∘ swap ∎
    where 
      open IsStableFreeElgotAlgebraˡ isStableˡ
      open FreeObject fe using (η) renaming (FX to FY)
      open Elgot-Algebra B using () renaming (_# to _#ᵇ; #-Uniformity to #ᵇ-Uniformity)
      open Elgot-Algebra FY using (_#)
      helper₁ : f ∘ swap ≈ (g ∘ swap) ∘ (η ⁂ id)
      helper₁ = begin 
        f ∘ swap ≈⟨ g-law ⟩∘⟨refl ⟩ 
        (g ∘ (id ⁂ η)) ∘ swap ≈⟨ pullʳ (sym swap∘⁂) ⟩ 
        g ∘ swap ∘ (η ⁂ id) ≈⟨ sym-assoc ⟩ 
        (g ∘ swap) ∘ (η ⁂ id) ∎
      helper₂ : ∀ {Z : Obj} (h : Z ⇒ Elgot-Algebra.A FY + Z) → (g ∘ swap) ∘ (h # ⁂ id) ≈ ((g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ
      helper₂ {Z} h = begin 
        (g ∘ swap) ∘ (h # ⁂ id) ≈⟨ pullʳ swap∘⁂ ⟩ 
        g ∘ (id ⁂ h #) ∘ swap ≈⟨ pullˡ (g-preserving h) ⟩ 
        ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) #ᵇ ∘ swap ≈⟨ sym (#ᵇ-Uniformity uni-helper) ⟩ 
        ((g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id)) #ᵇ ∎
        where
          uni-helper : (id +₁ swap) ∘ (g ∘ swap +₁ id) ∘ distributeʳ⁻¹ ∘ (h ⁂ id) ≈ ((g +₁ id) ∘ distributeˡ⁻¹ ∘ (id ⁂ h)) ∘ swap
          uni-helper = pullˡ +₁∘+₁ ○ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ○ (sym +₁∘+₁) ⟩∘⟨refl ○ pullʳ (pullˡ (sym distributeˡ⁻¹∘swap)) ○ (refl⟩∘⟨ (pullʳ swap∘⁂ ○ sym-assoc)) ○ sym-assoc

  record StableFreeElgotAlgebra : Set (suc o ⊔ suc ℓ ⊔ suc e) where 
    field
      Y : Obj
      freeElgot : FreeElgotAlgebra Y
      isStableFreeElgotAlgebra : IsStableFreeElgotAlgebra freeElgot
    
    open IsStableFreeElgotAlgebra isStableFreeElgotAlgebra public