open import Level
open import Categories.Category.Core
open import Categories.Category.Cocartesian

module Algebra.UniformIteration {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) where
  open Category C
  open Cocartesian cocartesian
  record Uniform-Iteration-Algebra-on (A : Obj) : Set (o ⊔ ℓ ⊔ e) where
    -- iteration operator
    field
      _# : ∀ {X} → (X ⇒ A + X) → (X ⇒ A)

    -- _# properties
    field
      #-Fixpoint : ∀ {X} {f : X ⇒ A + X }
        → f # ≈ [ id , f # ] ∘ f
      #-Uniformity : ∀ {X Y} {f : X ⇒ A + X} {g : Y ⇒ A + Y} {h : X ⇒ Y} 
        → (id +₁ h) ∘ f ≈ g ∘ h
        → f # ≈ g # ∘ h
      #-resp-≈ : ∀ {X} {f g : X ⇒ A + X} → f ≈ g → (f #) ≈ (g #)

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