Free Elgot algebras

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

  open Category C
  open Cocartesian cocartesian
  open Equiv
  open HomReasoning
  open MR C
  open M C

A free elgot algebra is a free object in the category of Elgot algebras.

  elgotForgetfulF : Functor Elgot-Algebras C
  elgotForgetfulF = record
    { F₀ = λ X → Elgot-Algebra.A X
    ; F₁ = λ f → Elgot-Algebra-Morphism.h f
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = λ x → x
    }

  -- typedef
  FreeElgotAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
  FreeElgotAlgebra X = FreeObject {C = C} {D = Elgot-Algebras} elgotForgetfulF X