{-# OPTIONS --safe #-}

open import Categories.Category.Core
open import Categories.Category.Cocartesian
open import Categories.Category.Construction.EilenbergMoore using (Module)
open import Categories.Object.Terminal
open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Monad hiding (id)
open import Monad.Instance.Delay

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

module Algebra.Search.Properties {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) (DM : DelayM cocartesian) where
  open import Algebra.Search cocartesian DM
  open import Algebra.Elgot cocartesian
  open import Algebra.UniformIteration cocartesian
  open DelayM DM
  open D-Monad
  open D-Kleisli
  open Coit
  open P-Coit
  open Category C
  open M C
  open MR C
  open Equiv
  open HomReasoning
  open Cocartesian cocartesian renaming (+-unique to []-unique)

  Uniform⇒Search : Uniform-Iteration-Algebra → Search-Algebra
  Uniform⇒Search U = record 
    { A = A 
    ; search-algebra-on = record 
      { α = out # 
      ; identity₁ = begin 
        out # ∘ now                ≈⟨ pushˡ #-Fixpoint ⟩ 
        [ id , out # ] ∘ out ∘ now ≈⟨ refl⟩∘⟨ unitlaw ⟩ 
        [ id , out # ] ∘ i₁        ≈⟨ inject₁ ⟩ 
        id                         ∎ 
      ; identity₂ = begin 
        out # ∘ later                ≈⟨ pushˡ #-Fixpoint ⟩ 
        [ id , out # ] ∘ out ∘ later ≈⟨ refl⟩∘⟨ laterlaw ⟩ 
        [ id , out # ] ∘ i₂          ≈⟨ inject₂ ⟩ 
        out #                        ∎ 
      } 
    }
    where
    open Uniform-Iteration-Algebra U

  Search⇒Uniform : Search-Algebra → Uniform-Iteration-Algebra
  Search⇒Uniform S = record 
    { A = A 
    ; algebra = record
      { _# = λ {X} f → α ∘ coit f
      ; #-Fixpoint = λ {X} {f} → begin 
        α ∘ coit f                               ≈⟨ intro-center out⁻¹∘out ⟩ 
        α ∘ (out⁻¹ ∘ out) ∘ coit f               ≈⟨ (refl⟩∘⟨ ((sym +-g-η) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
        α ∘ ([ now , later ] ∘ out) ∘ coit f     ≈⟨ pullˡ (pullˡ ∘[]) ⟩ 
        ([ α ∘ now , α ∘ later ] ∘ out) ∘ coit f ≈⟨ ([]-cong₂ identity₁ identity₂ ⟩∘⟨refl ⟩∘⟨refl) ⟩ 
        ([ id , α ] ∘ out) ∘ coit f              ≈⟨ pullʳ (coit-commutes f) ⟩ 
        [ id , α ] ∘ (id +₁ coit f) ∘ f          ≈⟨ pullˡ []∘+₁ ⟩ 
        [ id ∘ id , α ∘ coit f ] ∘ f             ≈⟨ (([]-cong₂ identity² refl) ⟩∘⟨refl) ⟩ 
        [ id , α ∘ coit f ] ∘ f                  ∎ 
      ; #-Uniformity = λ {X} {Y} {f} {g} {h} eq → sym (pullʳ (sym (coit-unique f (coit g ∘ h) (begin 
        out ∘ coit g ∘ h               ≈⟨ pullˡ (coit-commutes g) ⟩ 
        ((id +₁ coit g) ∘ g) ∘ h       ≈⟨ pullʳ (sym eq) ⟩ 
        (id +₁ coit g) ∘ (id +₁ h) ∘ f ≈⟨ pullˡ +₁∘+₁ ⟩ 
        (id ∘ id +₁ coit g ∘ h) ∘ f    ≈⟨ ((+₁-cong₂ identity² refl) ⟩∘⟨refl) ⟩ 
        (id +₁ coit g ∘ h) ∘ f         ∎ ))))
      ; #-resp-≈ = λ {X} {f} {g} eq → refl⟩∘⟨ coit-resp-≈ eq
      }
    }
    where open Search-Algebra S

  Elgot⇒Search : Elgot-Algebra → Search-Algebra 
  Elgot⇒Search EA = Uniform⇒Search (Elgot⇒Uniform EA)

  Elgot⇒D-Algebra : Elgot-Algebra → Module monad
  Elgot⇒D-Algebra EA = record 
    { A = A 
    ; action = out # 
    ; commute = begin 
      out # ∘ D.F.₁ (out #)                                 ≈˘⟨ #-Uniformity (sym uni₁) ⟩ 
      ((out # +₁ id) ∘ out) #                               ≈⟨ #-Compositionality ⟩
      ([ (id +₁ i₁) ∘ out , i₂ ∘ i₂ ] ∘ [ i₁ , out ])# ∘ i₂ ≈˘⟨ pullˡ (sym (#-Uniformity uni₂)) ⟩
      out # ∘ [ id , D.μ.η _ ] ∘ i₂                         ≈⟨ refl⟩∘⟨ inject₂ ⟩
      out # ∘ D.μ.η _                                       ∎ 
    ; identity = begin 
      out # ∘ now                ≈⟨ pushˡ #-Fixpoint ⟩ 
      [ id , out # ] ∘ out ∘ now ≈⟨ refl⟩∘⟨ unitlaw ⟩ 
      [ id , out # ] ∘ i₁        ≈⟨ inject₁ ⟩ 
      id                         ∎ 
    }
    where
    open Elgot-Algebra EA
    uni₁ : out ∘ D.F.₁ (out #) ≈ (id +₁ D.F.₁ (out #)) ∘ (out # +₁ id) ∘ out
    uni₁ = begin 
      out ∘ D.F.₁ (out #)                         ≈⟨ D₁-commutes (out #) ⟩ 
      (out # +₁ D.F.₁ (out #)) ∘ out              ≈˘⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ) ⟩ 
      (id +₁ D.F.₁ (out #)) ∘ (out # +₁ id) ∘ out ∎ 
    uni₂ : (id +₁ [ id , D.μ.η _ ]) ∘ [ (id +₁ i₁) ∘ out , i₂ ∘ i₂ ] ∘ [ i₁ , out ] ≈ out ∘ [ id , D.μ.η _ ]
    uni₂ = begin 
      (id +₁ [ id , D.μ.η _ ]) ∘ [ (id +₁ i₁) ∘ out , i₂ ∘ i₂ ] ∘ [ i₁ , out ]                            ≈⟨ pullˡ ∘[] ⟩
      [ (id +₁ [ id , D.μ.η _ ]) ∘ (id +₁ i₁) ∘ out , (id +₁ [ id , D.μ.η _ ]) ∘ i₂ ∘ i₂ ] ∘ [ i₁ , out ] ≈⟨ ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) ((extendʳ inject₂) ○ ∘-resp-≈ʳ inject₂)) ⟩∘⟨refl ⟩ 
      [ (id +₁ id) ∘ out , i₂ ∘ D.μ.η _ ] ∘ [ i₁ , out ]                                                  ≈⟨ ∘[] ○ []-cong₂ inject₁ refl ⟩ 
      [ (id +₁ id) ∘ out , [ (id +₁ id) ∘ out , i₂ ∘ D.μ.η _ ] ∘ out ]                                    ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) (∘-resp-≈ˡ ([]-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl)) ⟩ 
      [ out , [ out , i₂ ∘ D.μ.η _ ] ∘ out ]                                                              ≈˘⟨ []-cong₂ identityʳ (extend-commutes id ○ ∘-resp-≈ˡ ([]-cong₂ identityʳ refl)) ⟩ 
      [ out ∘ id , out ∘ D.μ.η _ ]                                                                        ≈˘⟨ ∘[] ⟩ 
      out ∘ [ id , D.μ.η _ ]                                                                              ∎

  D-Algebra+Search⇒Elgot : ∀ (mod : Module monad) → IsSearchAlgebra (Module.action mod) → Elgot-Algebra-on (Module.A mod)
  D-Algebra+Search⇒Elgot mod search = Elgot-Algebra.algebra (Id-Guarded⇒Unguarded (record 
    { _# = _# 
    ; #-Fixpoint = λ {X} {f} → #-Fixpoint ○ (sym (∘-resp-≈ˡ ([]-congˡ identityˡ)))
    ; #-Uniformity = #-Uniformity
    ; #-Compositionality = #-Compositionality'
    ; #-resp-≈ = #-resp-≈
    }))
    where
    open Module mod using (A) renaming (action to α; commute to D-commute)
    open Uniform-Iteration-Algebra (Search⇒Uniform (IsSearchAlgebra⇒Search-Algebra α search)) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈)
    #-Compositionality' : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ X + Y}
      → (((f #) +₁ id) ∘ g)# ≈ ([ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , g ])# ∘ i₂
    #-Compositionality' {X} {Y} {f} {g} = begin 
      α ∘ coit ((α ∘ coit f +₁ id) ∘ g)                    ≈˘⟨ refl⟩∘⟨ (coit-resp-≈ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identityˡ))) ⟩ 
      α ∘ coit ((α +₁ id) ∘ (coit f +₁ id) ∘ g)            ≈˘⟨ refl⟩∘⟨ D₁-coit ((coit f +₁ id) ∘ g) α ⟩
      α ∘ D.F.₁ α ∘ coit ((coit f +₁ id) ∘ g)              ≈⟨ extendʳ D-commute ⟩ 
      α ∘ D.μ.η _ ∘ coit ((coit f +₁ id) ∘ g)              ≈˘⟨ refl⟩∘⟨ (extend-≈ out⁻¹∘out ⟩∘⟨refl) ⟩
      α ∘ extend (out⁻¹ ∘ out) ∘ coit ((coit f +₁ id) ∘ g) ≈˘⟨ refl⟩∘⟨ p-coit-to-coit ((coit f +₁ id) ∘ g) out ⟩
      α ∘ p-coit ((coit f +₁ id) ∘ g) out                  ≈⟨ refl⟩∘⟨ (p-coit-unique ((coit f +₁ id) ∘ g) out (coit h ∘ i₂) ident) ⟩ 
      α ∘ coit h ∘ i₂                                      ≈⟨ sym-assoc ⟩ 
      (α ∘ coit h) ∘ i₂                                    ∎
      where
      h = [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , g ]
      aux : coit h ∘ i₁ ≈ coit f
      aux = sym (coit-unique f (coit h ∘ i₁) (begin 
        out ∘ coit h ∘ i₁                                  ≈⟨ extendʳ (coit-commutes h) ⟩ 
        (id +₁ coit h) ∘ h ∘ i₁                            ≈⟨ refl⟩∘⟨ pullʳ inject₁ ⟩ 
        (id +₁ coit h) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩ 
        (id +₁ coit h) ∘ (id +₁ i₁) ∘ f                    ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩ 
        (id +₁ coit h ∘ i₁) ∘ f                            ∎))
      ident : out ∘ coit h ∘ i₂ ≈ [ id , i₂ ] ∘ (out +₁ (coit h ∘ i₂)) ∘ (coit f +₁ id) ∘ g
      ident = begin 
        out ∘ coit h ∘ i₂                                         ≈⟨ extendʳ (coit-commutes h) ⟩ 
        (id +₁ coit h) ∘ h ∘ i₂                                   ≈⟨ refl⟩∘⟨ (pullʳ inject₂) ⟩ 
        (id +₁ coit h) ∘ [ (id +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ g         ≈⟨ pullˡ (∘[] ○ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl)) (extendʳ inject₂)) ⟩ 
        [ (id +₁ coit h ∘ i₁) ∘ f , i₂ ∘ coit h ∘ i₂ ] ∘ g        ≈⟨ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ refl aux)) refl) ⟩∘⟨refl ⟩ 
        [ (id +₁ coit f) ∘ f , i₂ ∘ coit h ∘ i₂ ] ∘ g             ≈˘⟨ ([]-cong₂ (coit-commutes f) refl) ⟩∘⟨refl ⟩ 
        [ out ∘ coit f , i₂ ∘ coit h ∘ i₂ ] ∘ g                   ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ refl identityʳ) ⟩ 
        [ out , i₂ ∘ coit h ∘ i₂ ] ∘ (coit f +₁ id) ∘ g           ≈˘⟨ pullˡ ([]∘+₁ ○ []-cong₂ identityˡ refl) ⟩ 
        [ id , i₂ ] ∘ (out +₁ (coit h ∘ i₂)) ∘ (coit f +₁ id) ∘ g ∎