open import Level
open import Categories.Category.Core
open import Categories.Functor.Algebra
open import Categories.Category.Cocartesian
open import Monad.Instance.Delay using (DelayM)

-- A *D-Algebra* `(A, α : D₀ A ⇒ A)` is called a *search-algebra* if it satisfies
-- - α now ≈ id
-- - α ▷ ≈ α

module Algebra.Search {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) (D : DelayM cocartesian) where
  open Category C
  open Cocartesian cocartesian
  open DelayM D
  open D-Monad

  record IsSearchAlgebra {A : Obj} (α : F-Algebra-on D.F A) : Set (ℓ ⊔ e) where
    field
      identity₁ : α ∘ now ≈ id
      identity₂ : α ∘ later ≈ α 

  record Search-Algebra-on (A : Obj) : Set (ℓ ⊔ e) where
    field
      α : F-Algebra-on D.F A

    field
      identity₁ : α ∘ now ≈ id
      identity₂ : α ∘ later ≈ α 

  record Search-Algebra : Set (o ⊔ ℓ ⊔ e) where
    field
      A : Obj
      search-algebra-on : Search-Algebra-on A
    open Search-Algebra-on search-algebra-on public

  IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on D.F A) → IsSearchAlgebra α → Search-Algebra
  IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } }
    where open IsSearchAlgebra is

  Search-Algebra-on⇒IsSearchAlgebra : ∀ {A} → (search : Search-Algebra-on A) → IsSearchAlgebra (Search-Algebra-on.α search)
  Search-Algebra-on⇒IsSearchAlgebra {A} search = record { identity₁ = identity₁ ; identity₂ = identity₂ }
    where open Search-Algebra-on search