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.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.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

  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